< 1268438417 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :plash is better than you. < 1268438424 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Or something :P < 1268438604 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yay, just got HOL Light installed (under cygwin...) and proved something with it < 1268438643 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Someone should make Plash for Windows < 1268438977 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: No. < 1268439196 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268439843 0 :augur!~augur@pool-96-231-169-236.washdc.fios.verizon.net JOIN :#esoteric < 1268439921 0 :cpressey!unknown@unknown.invalid PART #esoteric :? < 1268440221 0 :MigoMipo!~4f6606ed@gateway/web/freenode/x-omtwelumnkhfohrw JOIN :#esoteric < 1268440557 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268440576 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268440620 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268440658 0 :FireFly!unknown@unknown.invalid QUIT :Write error: Broken pipe < 1268440829 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1268441860 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :wow < 1268442265 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :wiw < 1268442280 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :waw < 1268442581 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :wuw < 1268442608 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :wyw < 1268442690 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :wew < 1268442706 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :wfw < 1268442708 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :c-c-c- < 1268442717 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :COMBO BREAKER? < 1268442730 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :HAI GAIS < 1268442735 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :You could have continued using another semivowel, you know. < 1268442738 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Like "yay". < 1268442753 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :waw, wew, wiw, wow, wuw, wyw, yay, yey, yiy, yoy, yuy, yyy... < 1268442772 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :After that, proceed to the stuff that's almost a vowel. rar, rer, rir, ror, rur, ryr. < 1268442787 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Then other stuff that's almost a vowel: lal, lel, lil, lol, lul, lyl. < 1268442802 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :And then some nasals: nan, nen, nin, non, nun, nyn, mam, mem, mim, mom, mum, mym. < 1268444010 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268444043 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :mer < 1268444044 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :rem < 1268444068 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Wow. http://to./ < 1268444075 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It's a URL shortener. < 1268444232 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :how is this even possible < 1268444245 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :to is a TLD < 1268444252 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :For some country < 1268444261 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Some country clever enough to make the greatest URL shortener ever. < 1268444277 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Also, http://to/bleh works the same if your OS doesn't suck. < 1268444303 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :but why the dot at the end < 1268444358 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I've recently been reminded that that's always been the correct canonicalization, since the beginning of DNS (this is why BIND wants your hostnames to end in a .), not having a . is just a convenience. < 1268444536 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :why i cannot visit pl. or com. then? < 1268444608 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :com. does work, although it forwards to www.com. < 1268444616 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pl. also works < 1268444638 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oh, sorry, my confusion, lemme restate: < 1268444645 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :bah < 1268444651 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :i see it does noe < 1268444654 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :com and pl don't have A addresses, they have no host. www.com. does work, as does www.pl. < 1268444684 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :com. doesn't work for the same reason that com doesn't work, because the gigantulous company that controls the com TLD doesn't have any address there. < 1268444688 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Same with pl < 1268444830 0 :nooga!unknown@unknown.invalid PRIVMSG #esoteric :wonder who controls it < 1268445897 0 :MigoMipo!unknown@unknown.invalid QUIT :Quit: Page closed < 1268446052 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :In zone files, domain names ending in . are absolute and domain names not ending in . are relative. < 1268446105 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So if your domain name is foo.com., adding an A record for blah.foo.com. will make http://blah.foo.com/ go somewhere, and adding an A record for blah.foo.com will make http://blah.foo.com.foo.com/ go somewhere. < 1268446162 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268446457 0 :nooga_!~nooga@sc82.internetdsl.tpnet.pl JOIN :#esoteric < 1268446656 0 :nooga!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268448947 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268448971 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268449007 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268450136 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268450189 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268450220 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268450257 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268450291 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268450474 0 :kwertii!~kwertii@ResNet-35-132.resnet.ucsb.edu JOIN :#esoteric < 1268451039 0 :werdan7!unknown@unknown.invalid QUIT :Ping timeout: 615 seconds < 1268451541 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268452350 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :burp < 1268452388 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: i see < 1268452402 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :code red! quarantine broken! < 1268452460 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :wha.... < 1268452462 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION dons a gas mask. < 1268452463 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268452469 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wraps nooga_ in plastic. < 1268452485 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :mmffgffgf < 1268452494 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION pokes breathing holes in the plastic. < 1268452501 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :hhhhhhh < 1268452507 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION pokes speaking holes in the plastic. < 1268452517 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268452529 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION pokes speaking articulately holes in the plastic. < 1268452532 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :that would actually make the plactic wrap pointles < 1268452538 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Indeed. < 1268452545 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wraps the holes in plastic. < 1268452546 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :There! < 1268452569 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :mmfgm. < 1268452596 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Hey, now. The holes still exist, so you can still breathe and speak and speak articulately through them. < 1268452614 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :But they're also wrapped in plastic so no contaminants can get out. < 1268452616 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Genius, eh? < 1268453034 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268453058 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :wait a second < 1268453176 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :isn't france in the same time zone with warsaw? < 1268453182 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :i mean paris < 1268453215 0 :nooga_!unknown@unknown.invalid PRIVMSG #esoteric :night coding huh? < 1268453329 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268454797 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268454823 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION notes that alise hasn't been around for a few days < 1268455588 0 :Libster!~Libster@pool-173-73-27-43.washdc.fios.verizon.net JOIN :#esoteric < 1268455590 0 :Libster!unknown@unknown.invalid PART #esoteric :? < 1268457468 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr2.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1268457937 0 :nooga_!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1268458345 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1268458559 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268458580 0 :FireFly!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268459489 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268459965 0 :coppro!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268460108 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268460746 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268461742 0 :MigoMipo!~4f6606ed@gateway/web/freenode/x-rjlhtwksgxferuvt JOIN :#esoteric < 1268466178 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268466370 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268467199 0 :clog!unknown@unknown.invalid QUIT :ended < 1268467200 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1268467294 0 :kwertii!unknown@unknown.invalid QUIT :Quit: bye < 1268468283 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268468520 0 :cheater2!~cheater@ip-80-226-230-32.vodafone-net.de JOIN :#esoteric < 1268469378 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268469607 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268472762 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268474231 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1268475673 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268478762 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1268478906 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268479493 0 :sebbu!unknown@unknown.invalid QUIT :Ping timeout: 256 seconds < 1268480177 0 :sebbu!~sebbu@ADijon-152-1-14-101.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1268480272 0 :fax!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1268480612 0 :tombom!tombom@wikipedia/Tombomp JOIN :#esoteric < 1268481980 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268483776 0 :cheater!unknown@unknown.invalid QUIT :Read error: Operation timed out < 1268483800 0 :cheater!~cheater@62.176.155.187 JOIN :#esoteric < 1268484058 0 :adam_d!~Adam@cpc2-acto6-0-0-cust48.brnt.cable.ntl.com JOIN :#esoteric < 1268484841 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1268485254 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1268486928 0 :lifthrasiir!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268487762 0 :MigoMipo!unknown@unknown.invalid QUIT :Quit: Page closed < 1268487784 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268488166 0 :lifthrasiir!8eA6PQte@haje12.kaist.ac.kr JOIN :#esoteric < 1268488311 0 :Phantom_Hoover!~chatzilla@cpc3-sgyl21-0-0-cust116.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268488346 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :If I have a raw Qemu disc image, how do I format an ext3 filesystem on it? < 1268488514 0 :lifthrasiir!unknown@unknown.invalid QUIT :Quit: leaving < 1268488527 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Well? < 1268488533 0 :lifthrasiir!GEaiGlw0@haje12.kaist.ac.kr JOIN :#esoteric < 1268488913 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ill < 1268489032 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268489182 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268489410 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268489484 0 :cheater2!~cheater@ip-80-226-21-16.vodafone-net.de JOIN :#esoteric < 1268490645 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Ping timeout: 256 seconds < 1268490709 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268491140 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Just mkfs.ext3 on it. < 1268491191 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :It might need the -F flag if it refuses to operate on a normal file, though I seem to recall it asking about it instead. < 1268491199 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :(Yes, I noticed he is gone already.) < 1268491800 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :What's the environment variable restriction in cfunge's sandbox mode useful for? < 1268491840 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :alise and/or ehird, when either of you show up: the intelligence squared debate on the catholic church as a force for good was simply amazing < 1268492377 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268492647 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :theres this thing called Intelligence Squared < 1268492665 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :they held a debate last year on whether or not the catholic hcurch was a force for good in the world < 1268492684 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :and they subsequently had a vote of the people who were present for the debate < 1268492702 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :pre-debate, the numbers were like 1000 no, 700 yes, 300 dont know < 1268492706 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :after it was like 1750 no, 200 yes, 50 dont know < 1268492925 0 :alise!~95fee059@gateway/web/freenode/x-lvxgikuciiqtiysh JOIN :#esoteric < 1268492952 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :#alise, please. I do not want this to be logged. < 1268493029 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :augur < 1268493031 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :daahafh < 1268493388 0 :alise_!~95fee059@gateway/web/freenode/x-egguysmgimtuqmqt JOIN :#esoteric < 1268493650 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268493980 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268494013 0 :alise!~95fee059@gateway/web/freenode/x-uykmcysttrftzukr JOIN :#esoteric < 1268494016 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :06:21:54 I wonder how small one can make a decent forth compiler in C < 1268494018 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.ioccc.org/1992/buzzard.2.design < 1268494077 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Compiler < 1268494139 0 :alise_!~95feda57@gateway/web/freenode/x-hrleiyrnmlrizhhb JOIN :#esoteric < 1268494288 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268494338 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :o.o; < 1268494684 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268494825 0 :alise!~95fed94f@gateway/web/freenode/x-dmnmbbezhbbexwjc JOIN :#esoteric < 1268495095 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1268495344 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268495730 0 :alise!~95fee1bd@gateway/web/freenode/x-fvgedxpwirwtqahy JOIN :#esoteric < 1268495770 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION writes a program to generate true constructivist statements. < 1268495770 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Endlessly < 1268495773 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*Endlessly. < 1268495789 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268495797 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Why not? < 1268495812 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's just a case of having a bunch of axioms and then substituting things for the variables in them. Endlessly. < 1268496202 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268496297 0 :fungot!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268496354 0 :alise!~95fee1bd@gateway/web/freenode/x-ieiwfwoquyoibxyu JOIN :#esoteric < 1268496873 0 :alise_!~95fed957@gateway/web/freenode/x-vqkqkunagmfvlpqv JOIN :#esoteric < 1268496884 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268496905 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: plz relink < 1268496905 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :in msg < 1268496926 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268497015 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Please? < 1268497033 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1268497045 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Por mi? < 1268497072 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Why not? < 1268497079 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :because nothing was said < 1268497095 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :-_-' < 1268497096 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :There was -- in #alise2. < 1268497102 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :At the beginning. < 1268497110 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(In /msg only, please. I do not want it leaking) < 1268497147 0 :fungot!~fungot@momus.zem.fi JOIN :#esoteric < 1268497154 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:31 -!- alise [~95fee059@gateway/web/freenode/x-uykmcysttrftzukr] has quit [Ping timeout: 252 seconds] < 1268497158 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:31 < alise_> test < 1268497160 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:31 < fax> test < 1268497161 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :FFS. < 1268497164 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I mean what I told you at the start. < 1268497165 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268497170 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Hello? < 1268497171 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :In */msg only. Please.* < 1268497173 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you want me to show you what you told me? < 1268497190 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268497208 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Yes. In /msg, in a private pastie. Please? < 1268497221 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why < 1268497239 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So I can show it to someone else... < 1268497241 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Because this client doesn't log... < 1268497272 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*... < 1268497313 0 :zzo38!~zzo38@h24-207-48-53.dlt.dccnet.com JOIN :#esoteric < 1268497340 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :I thought about Conway's Life cellular automaton but I have idea for a variant, called KnightLife < 1268497343 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: In case your question is still relevant, just /sbin/mkfs.ext3 on it; at least my copy will ask about being sure to operate on non-block-device, but will do it after confirmation. < 1268497375 0 :sebbu!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268497390 0 :sebbu!~sebbu@ADijon-152-1-14-101.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1268497422 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Fizzie: thanks. < 1268497453 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :all (0 -> all (0 -> 1)); all all all ((0 -> (1 -> 2)) -> ((0 -> 1) -> (0 -> 2))); all all ((~0 -> ~1) -> (1 -> 0)) < 1268497497 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Turns out I am a bit too lazy even to implement modus ponens. :) < 1268497662 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268497843 0 :alise!~95fed95b@gateway/web/freenode/x-fjylwgioskzbwcys JOIN :#esoteric < 1268498028 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268498049 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ffff I hate trivial programming bookkeeping < 1268498064 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I hate how I don't make much sense < 1268498071 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :even when I try really hard to < 1268498110 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :like consider < 1268498113 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :subst :: [(Integer,Statement)] -> Statement -> Statement < 1268498114 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi alise < 1268498118 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I do bookkeeping in the first argument but you also specify what to subst in there < 1268498128 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so when I come across a universal quantification < 1268498154 0 :alise_!~95fed95b@gateway/web/freenode/x-sjtxrewpryjjtiby JOIN :#esoteric < 1268498157 0 :Asztal!~asztal@host86-155-78-33.range86-155.btcentralplus.com JOIN :#esoteric < 1268498162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :FUCK < 1268498164 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :THIS < 1268498166 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :FUCKING < 1268498167 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :CONNECTION < 1268498169 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :until it's fixed i'm not talking < 1268498172 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :zzo38: so, what does KnightLife do? < 1268498262 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :It wouldn't be Life with knightships added, would it? < 1268498280 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :That would be cute. < 1268498296 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sdgjdfigjfdsoigx < 1268498301 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :rpghghrounprghounyphrguorpgh < 1268498311 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :phonographphonographphonograph < 1268498385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :safkaspofksad < 1268498385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :asfd < 1268498385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :asl < 1268498385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :das < 1268498385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dasd < 1268498387 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :a\sdl < 1268498389 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :a < 1268498390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :f < 1268498390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sfdskf < 1268498390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[sdf < 1268498402 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268498508 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: I thought it is obvious, isn't it? If not, I will explain < 1268498558 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Obvious from the name? < 1268498573 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :all (42 -> all (42 -> 1)) SAME FUCKING PROBLEM >_< < 1268498575 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I hate coding < 1268498576 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :hmm interesting < 1268498584 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Maybe it's a little bit obvious, but it's not very obvious. < 1268498590 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise: I hate programming too! < 1268498594 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :theres a subset of non-CF languages that have linear parse time < 1268498594 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Yes, a little bit. < 1268498596 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :hm hm! < 1268498614 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :and their conveniently representable in compact regex-like notation! < 1268498615 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Basically the 8 surrounding cells are the knight's move cells instead of the king's move cells < 1268498616 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :hm hm! < 1268498618 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :faxoh but I love programming < 1268498618 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :proper programming < 1268498624 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :not this fuking bookkeeping shit < 1268498625 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :with five bbillion variables < 1268498629 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :also fuck you chrome < 1268498633 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :show me the input field < 1268498636 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Now it's obvious, isn't it? < 1268498650 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :ACTION bookkeeps alise_'s variables < 1268498652 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :;o ;o ;o < 1268498668 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :WOOT < 1268498673 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268498699 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Yep, now it's obvious. < 1268498718 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268498726 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Same number of neighbors, but connected differently. Hmm. < 1268498784 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :asdfghj < 1268498821 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :pafdounafpoonufadpoundfapounadpfuondfpa < 1268498828 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :seriously what is it with shitty languages that can't match patterns and keep vaariables easily < 1268498843 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i should be able to like.. modulo out that stuff to a separate block and write the rest uberpurely < 1268498846 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :"Pattern matching is hard!" < 1268498860 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: not that kind of pattern matching < 1268498870 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the kind of pattern matching that involves a recursive function to determine the OK-ness of a pattern < 1268498880 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and then dispatching on the structure you infer in it < 1268498917 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq < 1268498922 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :This function is 99% fucking fluff. < 1268498943 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Now write modus ponens :: Statement -> Statement -> (Maybe) Statement. :-) < 1268499010 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :test < 1268499022 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :test < 1268499038 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :What is fax? < 1268499070 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :人間。 < 1268499070 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You cannot ask... what is fax. < 1268499071 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It is not a question. < 1268499073 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Instead, you mist ask.. < 1268499080 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Why did I typo "mist" for "must"? < 1268499108 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Then you will be enlightened. < 1268499108 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Who is fax? < 1268499117 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :alise_: so what is this language, and why must you use it? < 1268499138 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :BUT WHO IS PHAX?! < 1268499166 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: This is ... Haskell ... < 1268499178 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :fax is the bastard child of Miss Piggy and Kermit the Frog. < 1268499187 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :THIS < 1268499190 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :IS < 1268499192 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :HASKELL!!!!!!!!! < 1268499193 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ファクス君が此処に居る人です。 < 1268499208 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :saoidjdoifjsdojdsf < 1268499212 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I'm I'm understanding you correctly, I'm slightly surprised that you're calling Haskell a shitty language that can't match patterns and keep variables easily. < 1268499214 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :THIS - IS - AN OUTDATED - MEEEEEEEEME < 1268499214 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION bastard < 1268499215 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I wish someone actually took u my challenge to write modusponens :P < 1268499216 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(fax is a person who is hear) < 1268499216 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :s/I'm/If/ < 1268499219 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*up < 1268499226 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :stop speaking japanese. < 1268499228 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: :) < 1268499229 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :s/hear/here/ < 1268499231 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: because I don't mean the trivial sense that haskell does < 1268499235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I mean generalised book keeping < 1268499239 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/868022.txt?key=mqvjqn84rgv75aalq9arq < 1268499244 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :2/3 parameters are bookkeeping < 1268499246 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :augur: 日本語を勉強する始めて。 < 1268499252 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the majoritry of the code. book keeping < 1268499254 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(start studying Japanese) < 1268499259 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if you try and code modus ponens inferrence using that, < 1268499265 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you get EVEN MORE book keeping! yay < 1268499358 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I think I'm turning Portuguese I think I'm turning Portuguese I really think so < 1268499405 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So just what is subst supposed to do? < 1268499425 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Substitute. < 1268499450 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If the language excelled at eliminating pointless crap like that it'd be obvious from the definition. < 1268499455 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Substitute what for what into what? < 1268499471 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Substitute for a given De Bruijn index into a logical statement. < 1268499475 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :programming languages don't exist < 1268499486 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :THERE IS ONLY ZUUL < 1268499492 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :fax has spoken. < 1268499525 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*XUL < 1268499532 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :*XML < 1268499535 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(The XUL namespace file is one called there.is.only.xul; it says that. :)) < 1268499622 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Okay, I think I see what this is all about. < 1268499622 0 :zzo38!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268499788 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268499801 0 :alise!~95fed95b@gateway/web/freenode/x-wrypznxukeqkofpv JOIN :#esoteric < 1268499822 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION installs xchat to avoid the shitty webchat client < 1268499905 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: If you do decide to be my slave, the expectation of mp is that `mp (Var n :-> q) p'` produces q with p substituted for Var n (note that if you hit an All, all existing variables are shifted one place, and 0 becomes the newly-quantified variable); `mp (Not p :-> q) (Not p')` does the same but with the obvious, and `mp ((p :-> r) :-> q) (p' :-> r')` check that p/p' and r/r' match and then does the same as the others. < 1268499920 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Actually, I'm just saying that so it's clearer what I have to do. < 1268500144 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ss < 1268500181 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise shut up < 1268500188 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :have you read I am not a number, I am a free variable < 1268500204 0 :alise_!~alise@genld-216-046.t-mobile.co.uk JOIN :#esoteric < 1268500264 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I know how De Bruijn indexes work, fax. < 1268500270 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I chose a bit of a shitty representation though. < 1268500275 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I know how your mom works < 1268500277 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"fax" < 1268500282 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268500283 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Who is fax < 1268500293 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I did not mean that. < 1268500301 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What do you mean, "'fax' what"? < 1268500308 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise shut up have you read it?? < 1268500322 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :How can I do both simultaneously? < 1268500328 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :JUST!!!! DO!!!!! < 1268500354 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Can someone with more kernel knowledge than me tell me if this is feasible: http://esoteric.voxelperfect.net/forum/kareha.pl/1266506523/1 < 1268500410 0 :indu!~indu@117.192.150.14 JOIN :#esoteric < 1268500430 0 :indu!unknown@unknown.invalid PART #esoteric :? < 1268500481 0 :alise__!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268500492 0 :alise__!unknown@unknown.invalid QUIT :Client Quit < 1268500536 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268500564 0 :MarcoAchur1!~usuario@200.71.243.5 JOIN :#esoteric < 1268500584 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :This is a gun: =>. And this is 5 episodes of Endless Eight. < 1268500656 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268500842 0 :alise!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268500881 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268500885 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :mIRC users: how the fuck do you set the default font for all subdinwws? < 1268500891 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*subwindows < 1268500918 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :got it < 1268500974 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Why the fuck would you use mIRC? < 1268500978 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Sorry for the language < 1268501003 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :a lot of idiots hate mIRC for seemingly no reason other than idiots use it. On Windows I have been unable to find a better client (because all others suck). < 1268501084 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268501109 0 :alise_!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268501122 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :...and then it inexplicably crashed < 1268501129 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, Silverex? < 1268501139 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No, mIRC. Or maybe I quit it... < 1268501143 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Windows is confusing. < 1268501183 0 :alise_!unknown@unknown.invalid QUIT :Client Quit < 1268501187 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I meant, what's wrong with Silverex? < 1268501190 0 :alise!unknown@unknown.invalid QUIT : < 1268501217 0 :alise!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268501227 0 :alise_!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268501234 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Figured out why. < 1268501242 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It was minimising to tray; bad idea w/ Win7. Didn't actually crash. < 1268501246 0 :alise!unknown@unknown.invalid QUIT :Client Quit < 1268501251 0 :alise_!unknown@unknown.invalid NICK :alise < 1268501261 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So now my only question is how to make subwindows maximised by default. < 1268501302 0 :alise!unknown@unknown.invalid QUIT :Client Quit < 1268501332 0 :alise!~alise@genld-216-213.t-mobile.co.uk JOIN :#esoteric < 1268501375 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Ftop. < 1268501449 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hopefully a permanent client should make my IRC more reliable. < 1268501457 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Is there anything better than Pidgin yet for Windows IMing? < 1268501465 0 :MarcoAchur1!unknown@unknown.invalid PART #esoteric :? < 1268501496 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :nekwhat's the apb < 1268501590 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268501592 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Are you drunk? < 1268501803 0 :adam_d!~Adam@cpc2-acto6-0-0-cust48.brnt.cable.ntl.com JOIN :#esoteric < 1268501840 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I recently tried switching to Digsby < 1268501848 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oerjan said something about superstrict languages where (\x. f x) evaluates f. < 1268501852 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That's interesting. < 1268501855 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268501867 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Yet to form a solid opinion on whether it's better. So far, still hoping that its Facebook Chat support is better than Pidgins < 1268501877 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Digsby is spyware, iirc. < 1268501881 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Or at least obnoxiously social. < 1268501903 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Which one? I mind the former, the latter can be disabled as far as I've seen < 1268501927 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I don't know. < 1268501952 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x). < 1268501959 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So even the lambda-expression of Y would diverge. < 1268501966 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Is it TC, I wonder? < 1268501973 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(\x. x x) is OK < 1268502008 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268502341 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yay, I implemented it and Y does indeed diverge. < 1268502517 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268502526 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :using divergence to check if your code works < 1268502547 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quite. < 1268502664 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise, hm.. which language? < 1268502677 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :lambda calculus? < 1268503033 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268503037 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Superstrict lambda calculus. < 1268503050 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Where, in (\x.E), you evaluate E as far as you can without relying on x's value. < 1268503060 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So (\x. f x) evaluates f before it's even applied. < 1268503135 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*Main> eval (App succL zeroL) < 1268503136 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\a. \b. (a ((*** Exception: Prelude.(!!): index too large < 1268503140 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Dammit. < 1268503142 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :The verifier should have caught that... < 1268503154 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: That's pretty damned crazy right there. < 1268503196 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Ugh, I have some sort of horrible bug. < 1268503202 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(You could argue the entire thing is a horrible bug.) < 1268503306 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :At some point I used Xircon for Windows-irc, but the development of that died at 1.0b4, I think. It had a TCL scripting engine, that was at least nicer than mirc-scripting. But that was years ago; not sure what people use nowadays. < 1268503450 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I have no idea why this isn't working XD < 1268503467 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION tries booleans instead as a test < 1268503604 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I have serious variable issues. < 1268503759 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ah... < 1268503766 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Lam ((Var 1 :$ Lam (Lam (Var 1))) :$ Var 1) < 1268503770 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm not demoting my variables sufficiently < 1268504050 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise shut up!!!!!!!! < 1268504085 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :read the (first few pages of the) paper < 1268504109 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268504121 0 :alise_!~alise@genld-216-207.t-mobile.co.uk JOIN :#esoteric < 1268504183 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION ported the "official" Lazy K interpreter to use Boehm GC... < 1268504198 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Quite an accomplishment. < 1268504210 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The reference counting scheme it used leaked memory. < 1268504215 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :So I fixed it. < 1268504228 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I've also made the thing compile on modern C++ compilers. :P < 1268504240 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :It used reference counting? < 1268504242 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Lollercopters < 1268504244 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268504257 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It leaked a metric fuckton of memory. And the author had no idea why. < 1268504263 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :WHat's wrong with reference counting? < 1268504276 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Leaks memory with cyclic datastructures. < 1268504282 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So... the issue is that when I apply a lambda, and it results in a lambda, I need to decrement the Vars in it. < 1268504288 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Ah < 1268504292 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Bleh. < 1268504297 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Not interesting enough. < 1268504305 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Also, is somewhat overhead-heavy if done naively. < 1268504330 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okay im here < 1268504395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It would be interesting to have a language where all expressions result in infinite structures. < 1268504404 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Then reference counting would be /useless/ :) < 1268504442 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Most of the work in making the interpreter GC'd was removing the reference counting and the inefficient pool allocator. < 1268504468 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Adding the GC-ness was... "class Expr : public gc {" < 1268504633 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :`calc 1 metric fuckton in US fucktons < 1268504642 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :`calc 1000000000000000000000000000000000000000000000000 < 1268504645 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :twitterbits.com/wp-content/plugins/as-pdf/generate.php?post=11 - [21]Similar < 1268504646 0 :HackEgo!unknown@unknown.invalid PRIVMSG #esoteric :yodellingllama.com/?p=1183 - [16]Cached - [17]Similar < 1268504741 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Y'know, I'm starting to think that metric fucktons aren't even a real unit! < 1268504856 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hahah. < 1268504908 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :http://sprunge.us/OLIF It's a Lazy K interpreter that doesn't leak memory! < 1268504931 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Is it a bird? Is it a plain? No... < 1268504935 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(This is Jeopardy, right?) < 1268504942 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*plane >_< < 1268505029 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(note: still more complicated than it should be. C++: because iostreams suck so much we write our own stream class for everything) < 1268505085 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268505258 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders whether he's invented the Church, Mogensen-Scott or an entire, unnamed other encoding. < 1268505266 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(The latter is unlikely.) < 1268505331 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Mogensen-Scott is best < 1268505335 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268505364 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :How do you encode Nil | Cons ? List in Mogensen-Scott? I have: < 1268505368 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Nil = \f g x. f x < 1268505368 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Cons = \head tail f g x. tail f g (g head x) < 1268505370 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Z | S Nat: < 1268505370 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Z = \f g x. f x < 1268505370 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :S = \nat f g x. nat f g (g x) < 1268505371 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A ? | B ?: < 1268505372 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A = \val f g x. f val x < 1268505372 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :B = \val f g x. g val x < 1268505389 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Are there any people acquainted with the Linux kernel here? < 1268505390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and finally, A | B: < 1268505390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A = \f g x. f x < 1268505390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :B = \f g x. g x < 1268505417 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So for a given constructor C, you take n functions where there are n constructors, and each function is of the type (... -> x) for the same x for all of them and ... being the arguments to the constructor. < 1268505432 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If there is no recursion in the type, then you simply call the appropriate function. < 1268505433 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise weird < 1268505452 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Otherwise, you invoke your substructure with the same functions, but with the value being substituted for what you'd normally do without the recursion. < 1268505476 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I may have the function types wrong; forgot about the \x. bit. < 1268505476 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I think it's the most natural encoding. < 1268505480 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Case analysis is built-in as the distinct functions. < 1268505491 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Decomposition of the value also is built-in to each function's argument. < 1268505502 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And it transforms type recursion into value recursion. < 1268505523 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So the relevant function gets the /already decomposed, according to your will/ substructure as its argument. < 1268505561 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: and you know what? < 1268505564 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> :t cons (1::Integer) (cons 2 nil) < 1268505564 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons (1::Integer) (cons 2 nil) < 1268505564 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : :: (t21 -> t2) -> (Integer -> t21 -> t21) -> t21 -> t2 < 1268505568 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It encodes types as their fold. < 1268505571 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think their left fold. < 1268505576 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Maybe right-fold would be more elegant. < 1268505628 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So succ would be \nat f g x. g (nat f g x) < 1268505643 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cons would be \hd tl f g x. g head (tail f g x) < 1268505648 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: is that morgonson? < 1268505670 0 :sebbu2!~sebbu@ADijon-152-1-37-180.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1268505670 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1268505678 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What is morgonson then? < 1268505735 0 :sebbu!unknown@unknown.invalid QUIT :Ping timeout: 245 seconds < 1268505735 0 :sebbu2!unknown@unknown.invalid NICK :sebbu < 1268505944 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION tries to transform a tree into it < 1268506003 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Leaf = \val f g x. f val x < 1268506004 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Branch = \left right f g x. left f g (g (right f g x) x) < 1268506004 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or < 1268506004 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Branch = \left right f g x. g (left f g x) (right f g x) < 1268506004 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think < 1268506015 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think the latter is better. < 1268506020 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise did you see my post that uses lambda calculus < 1268506030 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No; link. < 1268506044 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :on the blog < 1268506066 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION attempts to google to find it again < 1268506152 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268506173 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :church numerals are like this but with f=id < 1268506175 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which is equivalent < 1268506190 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and church numerals are A/B without the extra x (equivalent under n) < 1268506218 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :actually < 1268506222 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :false = \g x. x < 1268506226 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :true = \g x. g x < 1268506230 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so false = \a b. b < 1268506233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :true = \a. a < 1268506236 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268506255 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wait i can't have f = id < 1268506257 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A = \val f g x. f val x < 1268506257 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :B = \val f g x. g val x < 1268506306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> :t branch < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :branch < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : :: (t -> (t2 -> t3 -> t4) -> t1 -> t2) < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : -> (t -> (t2 -> t3 -> t4) -> t1 -> t3) < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : -> t < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : -> (t2 -> t3 -> t4) < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : -> t1 < 1268506307 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : -> t4 < 1268506308 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obviously < 1268506605 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm it should be f x val < 1268506609 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :not f val x < 1268506666 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Cons = \head tail f g x. g (tail f g x) head < 1268506670 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Er, no, that's not really right. < 1268506900 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I thought of a really nice property of musing Mu for recursive datatypes. < 1268506934 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :musings on Mu -- sounds like a blog post < 1268507029 0 :olsner_!~salparot@c83-252-161-133.bredband.comhem.se JOIN :#esoteric < 1268507052 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: hehe < 1268507099 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I often have the issue that I have two types, e.g. expression and pattern, where pattern is like expression but with one extra constructor like Free String < 1268507102 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so I have to do < 1268507104 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Core = ... < 1268507112 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(oh and expression has some extra thing too) < 1268507116 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Expr = Core Core | ... < 1268507120 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Pat = Core Core | ... < 1268507121 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :except < 1268507124 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what if Core is recursive? < 1268507132 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Core self = ... < 1268507142 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Expr = Core (Core Expr) | ... < 1268507147 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Pat = Core (Core Pat) | ... < 1268507149 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but < 1268507151 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if Core was defined with mu < 1268507156 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then it'd be Mu F < 1268507162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so we'd just do F (Mu Expr) instead! < 1268507183 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so Mu actually lets you easily express recursion-substitution of data types < 1268507324 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think we need some way to extract the F from a Mu F < 1268507356 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wait, that's easy < 1268507358 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :extract (Mu F) = F < 1268507362 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268507366 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that requires pattern matching on Mu :P < 1268507379 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Are you just talking to yourself? < 1268507406 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :He's talking to whoever is listening. < 1268507414 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, fax would ideally respond. < 1268507429 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :What is it you're talking about? < 1268507433 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I missed the start. < 1268507496 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Using Mu-recursive types to encode recursion-substitution of data types. < 1268507537 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1268507611 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :heh () becomes id in my encoding < 1268507650 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :How does that work? < 1268507697 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/868169.txt?key=mmgxkfgi4bnnt1ix3u3jqg < 1268507725 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Haskell? < 1268507737 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268507738 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, for the data types (with ? for polymorphism) < 1268507745 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The expressions, lambda-calculus < 1268507752 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The format is data Foo = ..., in my representation is ... < 1268507793 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So a constructor C for a type T with N constructors, C takes N functions of the arity of the corresponding constructor, plus one (of the same type for every function, but polymorphic), and returning something of the same type for every function (but polymorphic). < 1268507808 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268507817 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oh, and a value of the type of the first argument of each function. < 1268507825 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If the data type is not recursive, then the corresponding function is simply called with the value given, plus the constituents of the constructor. < 1268507826 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :*quails* < 1268507840 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If it is recursive the value given is substituted for the value of calling the substructure with the same functions, and the value. < 1268507850 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(This is repeated for each recursive element, as different arguments to the function.) < 1268507858 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Thus: < 1268507860 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Leaf = \val f g x. f val x < 1268507861 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Branch = \left right f g x. g (left f g x) (right f g x) < 1268507875 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I was away having dinner < 1268507903 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: That is NOT ALLOWED. < 1268507908 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :;( < 1268507912 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I didn't know < 1268507924 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Real Programmers eat the dust in the air. < 1268507926 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268507935 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: well READ WHAT I SAID :| < 1268507938 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi oerjan! < 1268507940 0 :MizardX-!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268507943 0 :MizardX-!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268507945 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hi fax < 1268507949 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise encoding data into lambda calculus is boring though < 1268507952 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :also alise_ < 1268507961 0 :MizardX-!~MizardX@81-237-250-33-no147.tbcn.telia.com JOIN :#esoteric < 1268507963 0 :MizardX-!unknown@unknown.invalid QUIT :Changing host < 1268507963 0 :MizardX-!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268507974 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey < 1268507983 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so where does calulus happen? < 1268507993 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :real numbers, finite numbers, data < 1268507995 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what else ? < 1268508010 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Calculus :: * -> BranchOfMathematics < 1268508018 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: What is there that is not data? < 1268508018 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :um < 1268508020 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Wait, there's and implementation of real numbers on the lambda calculus now? < 1268508023 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Function calculus perhaps? < 1268508024 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't mean lambda calculus < 1268508028 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :s/and/an/ < 1268508034 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I mean like "derivatives" and "integrals" < 1268508038 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: The computable reals are expressible in just about any language. < 1268508045 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :on data I mean specifiically: d for data < 1268508046 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well-typed at compile time in dependent languages. < 1268508054 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :please just understand what I mean :| < 1268508071 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :f : PosRational -> Rational is a computable real number iff for all positive rationals e1, e2, abs (f e1 - f e2) < e1 + e2 < 1268508090 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah, for computable reals you don't even need recursion < 1268508093 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268508096 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"recursion" < 1268508104 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :+general < 1268508130 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah if you can do rationals and semi-recursive functions < 1268508132 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then you can do computable reals < 1268508133 0 :MizardX!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1268508140 0 :MizardX-!unknown@unknown.invalid NICK :MizardX < 1268508144 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you could even model them in brainfuck if you came up with a function representation < 1268508156 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I should implement some reals, but I'd need quotient field..... < 1268508164 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and I have implemented it but not proved it a field yet < 1268508201 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*<= < 1268508203 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :not < < 1268508204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I always make that mistake < 1268508233 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise ill tell you the defintion from my bok < 1268508340 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :bok < 1268508379 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, < 1268508396 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :really what you need is a cauchy sequence that's all :P < 1268508443 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Serious analysis begins with the real numbers. A /real number/ is a sequence (x_n)_(n>=1) of rational numbers that is /regular/, in the sense that forall m >= 1, forall n >= 1, |x_m - x_n| <= m^-1 + n^-1 < 1268508495 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :The standard equality on the class R of real numbers is defined so that (x_n) =_R (y_n) if and only if forall n >= 1, |x_n - y_n| <= 2n^-1 < 1268508497 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah but if you have an infinite sequence... well that's a function < 1268508513 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and it's nicer to use if you have the indices be Q+s < 1268508526 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :This relation is clearly reflexive and transitive; its transitivity is a consequence of 6.1 < 1268508530 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :also equality on the computable reals doesn't always terminate if they're nonequal which sucks < 1268508535 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :imo, using === is better < 1268508543 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then you just have to prove they're equal or not :)))) < 1268508557 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah equality is not decidible on R, that's a classical statement < 1268508570 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that =_R I gave above is a proposition < 1268508588 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268508592 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268508601 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise want to show you something really cool I saw today < 1268508604 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i know it's well known < 1268508607 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but it does so suck < 1268508615 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what sucks?? < 1268508627 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise_: um if they're nonequal obviously it terminates, it's the equal case that is problematic < 1268508627 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, read this http://coq.inria.fr/stdlib/Coq.Reals.Rlogic.html < 1268508628 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :a NINJA??? < 1268508640 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o_o lol < 1268508823 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: er right < 1268508848 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :09:39:12 Hmm... (\f. (\x. f (x x)) (\x. f (x x)) would evaluate (x x). < 1268508848 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :09:39:19 So even the lambda-expression of Y would diverge. < 1268508863 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"transClause :: ..." ;; Mr, now Mrs Clause < 1268508865 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well but that expression is unusable in a (just) strict language anyway < 1268508914 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem not_not_archimedean : < 1268508919 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : forall r : R, ~ (forall n : nat, (INR n <= r)%R). < 1268508919 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Not not not not not. < 1268508924 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: of course < 1268508929 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :having lambda-expressions diverge is hilarious < 1268509090 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :10:17:56 Sgeo: Leaks memory with cyclic datastructures. < 1268509107 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i don't think lazy-K has cyclic datastructures, but i haven't investigated it < 1268509115 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise did you read it??? < 1268509140 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :because it doesn't have Y as a primitive < 1268509152 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: yrd < 1268509157 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :?? < 1268509157 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*yes < 1268509165 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :now what 'sucks'? < 1268509197 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although on the other hand _that_ might perhaps cause memory leaks with recursion that an efficient Y wouldn't give < 1268509222 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: non-propositional equality on reals < 1268509224 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ffs < 1268509240 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the consequence of decidible equality < 1268509260 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :think about classical logic as contained inside constructive.. < 1268509265 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or perhaps that just causes a lot of duplicate evaluation. < 1268509298 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: what are you trying to say < 1268509319 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is assuming lazy-K isn't so cleverly implemented as to detect essential uses of Y < 1268509326 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :im just talking :| < 1268509427 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: :-) okay < 1268509443 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you think im stupid!! < 1268509445 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ill show you < 1268509449 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: also i'm beginning to think pattern matching in function heads is overrated in dependent langs... < 1268509457 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh?? < 1268509485 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I don't think you're stupid ffs :) < 1268509486 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and < 1268509487 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :bI don't think a denpendent language needs to support pattern matching < 1268509496 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I mean as a syntactic thing < 1268509498 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it should be able to add pattern matching < 1268509505 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because often pattern matching has drastic effects on the structure of the other arguments < 1268509516 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so a possibly-nested case expression makes this much clearer < 1268509529 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and often the analysis is more complex than just does-this-constructor-match < 1268509531 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well you can try programming with nested cases in Coq < 1268509536 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and function-head matching doesn't really aid that < 1268509555 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :at one point I just gave up an implemented (an ad-hoc bug* ridden version of) dependent pattern matching < 1268509577 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(* not actually able to produce wrong results.. but sometimes might not produce any result) < 1268509635 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well i mean i like dependent pattern matching < 1268509646 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but I'm specifically criticising < 1268509649 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :f (X ...) = ... < 1268509651 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :f (Y ...) = ... < 1268509670 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah but you know case < 1268509673 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you can't just write < 1268509688 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :f x = case x of X ... -> ... ; Y ... -> ... < 1268509691 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :if it's dependent < 1268509697 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you have to say something about the types < 1268509697 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm. < 1268509702 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I don't see why < 1268509706 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268509717 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well.................... you do in Coq, is this a fundamental thing though? < 1268509727 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what do you mean say something about the types btw? < 1268509730 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ISTR augustss writing about it being essential < 1268509733 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well I blogged about it < 1268509773 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: that Talk: Befunge message you responded to is spam (try googling it) < 1268509780 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268509785 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :sheesh < 1268509791 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :he just does that on purpose < 1268509796 0 :augur!~augur@pool-96-231-169-236.washdc.fios.verizon.net JOIN :#esoteric < 1268509834 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: um that Ping timeout thing isn't is server generated? < 1268509849 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :he pulls the plug out 265 seconds before someone talks to him < 1268509994 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I should have a specialisation of id called ff < 1268509994 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so I can have < 1268510002 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :tt : ? < 1268510002 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ff : ? < 1268510006 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hope that sent right < 1268510010 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :¬??? < 1268510015 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268510018 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :top/bot < 1268510019 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that ? must have been a 'T' < 1268510019 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :from tt/ff < 1268510024 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268510028 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :TT : ~T < 1268510029 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268510031 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268510031 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268510034 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :tt : T < 1268510036 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ff : ~_|_ < 1268510036 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :looks like Omegamega < 1268510042 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm indeed user quit messages are prefaced with Quit: < 1268510072 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(the format changed when they switched ircd) < 1268510088 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :toProp : (b : Bool) -> Sigma (P : Prop) (cond [b => P, not b => ~P]) < 1268510089 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :toProp b := < 1268510100 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : cond [b => T sigma tt, not b => _|_ sigma ff] < 1268510122 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wondering if i should use case analysis instead of cond < 1268510146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah it looks nicer < 1268510159 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I should have ?: with a nicer name :) < 1268510201 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268510219 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : Phantom_Hoover: that Talk: Befunge message you responded to is spam (try googling it) < 1268510256 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: ^ < 1268510346 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Oh. < 1268510354 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Very weird spam. < 1268510386 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: i don't know why they're doing it, but it's fairly common. look out for messages that have no hint the poster knows what the wiki is about. < 1268510390 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :after a while you get a sense as to what's spam and what isn't < 1268510403 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: does the page need deleting? or is there legit content on it too? < 1268510419 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: i already removed that section, there are lots of legit ones < 1268510428 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1268510472 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i have an excellent spam 'n phish o mometer < 1268510473 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :spam and fish < 1268510475 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I should probably start selling fungot licenses to spammers; it's more entertaining than the usual gibberish I see in my inbox. (Though they might not be going for the entertainment value there.) < 1268510475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1268510475 0 :fungot!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: i was born in a barn?". i assume you'll mostly just want " how did you get my privmsgs? < 1268510491 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Born in a Barn. fungot. The autobiography. < 1268510492 0 :fungot!unknown@unknown.invalid PRIVMSG #esoteric :alise_: distributive property for example i wrote program as an ast? i believe the right way < 1268510509 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: they have started trying to formulate messages that look like they _could_ be legit, but google shows when they're spammed all over the place < 1268510552 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/place/web/ < 1268510631 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ehird < 1268510635 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise < 1268510644 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: that spam is mostly pointless anyway, if they aren't spamming URLs or anything like that < 1268510693 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I have a feeling I need a real system... < 1268510696 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I keep using "refl" to substitute for any a === :-) < 1268510700 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*a === b < 1268510708 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: yeah i don't understand why they're doing it either. maybe to test our spam response intelligence? < 1268510714 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise I don't understand < 1268510730 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you cant use refl unless a and b are convertible < 1268510735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: don't understand what, my refl thing? < 1268510737 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268510739 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: I heard an explanation that sounds plausible: the bots are trying to spam their URLs in an URL field, and although MediaWiki doesn't have one the bots don't know that < 1268510742 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well exactly < 1268510749 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :however, in that case I don't see how they'd be getting past the CAPTCHA < 1268510749 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ah < 1268510752 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :toProp b === T sigma tt? well obviously, it's true! < 1268510765 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that's extentional equality!!!!! < 1268510770 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :spambots generally need some knowledge of how an individual CAPTCHA works before breaking it < 1268510775 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Proof: refl! < 1268510787 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hrfm < 1268510795 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: does our wiki have a special captcha? < 1268510810 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, it's MediaWiki's default captcha < 1268510819 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and a very easily broken one, at that < 1268510821 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i don't recall seeing it < 1268510825 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so? :P < 1268510831 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, wait < 1268510839 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :btw how is apartness defined? < 1268510842 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: which means the spammers probably know all about it since a long time ago < 1268510853 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the CAPTCHA rules are that they come up on attempts to register accounts, and edits by anons that add URLs < 1268510859 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I thought of having as an argument to the constructor a proposition for which P x but not P y < 1268510860 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :thinking about it: this spam isn't actually adding URLs < 1268510865 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so it doesn't need to go past the CAPTCHA at all < 1268510886 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: heh. also this last spam showed some indication they knew it was a _wiki_, even if not what the wiki was about < 1268510898 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(it talked about creating articles) < 1268510975 0 :mano0o0!~Administr@41.129.28.153 JOIN :#esoteric < 1268510976 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or maybe that's common terminology for other things than wikis too < 1268510989 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the spam just came up on my feed of all edits to Esolang < 1268510992 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :nothing gets past the admins! < 1268510998 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :just, sometimes other people get there first < 1268511011 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and that particular comment would make sense on a blog, too < 1268511015 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although it would mean something else < 1268511022 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: oh? what then? < 1268511037 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :an article would have to posted by a blog owner wouldn't it < 1268511043 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*to be < 1268511055 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: it means, can someone find me more articles on this subject? < 1268511096 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm not quite, but i see it could be... < 1268511097 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I will show you apartness < 1268511107 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise I should just write this whole chapter into Coq :P < 1268511113 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it sounds like one blogger asking another how they find ideas < 1268511120 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1268511211 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x # y if x > y or y > x < 1268511228 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: just look at this pile of shit: http://pastie.org/868241.txt?key=unp3wmm109dzwe6ssnkw < 1268511234 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :properties: x = y /\ x # y -> 0 = 1 < 1268511238 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I just cheated through the whole fucking proof by sprinkling refl everywhere! :-P < 1268511243 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i wonder if the wiki enabled captchas after i joined (2006) < 1268511245 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so apartness is only defined if you have an ordering? < 1268511248 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I had < 1268511252 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x = y /\ y # z -> x # z (??? weird one) < 1268511257 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x # y -> y # z < 1268511259 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x # y -> y # x *** < 1268511266 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x # y -> x # z \/ z # y < 1268511314 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data Apart : {A:Set} -> (x:A) -> (y:A) -> Prop where lfer : {P : A->Prop} -> ((P x /\ ~P y) \/ (P y /\ ~P x)) -> Apart x y < 1268511339 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: it's relatively recent, I had a discussion with Graue about it < 1268511363 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise what's teh point in making that data? < 1268511367 0 :olsner_!unknown@unknown.invalid QUIT :Quit: olsner_ < 1268511368 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why not just do it as a function definition < 1268511379 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh wait I completely neglected my obligation in toBool to supply P | ~P < 1268511379 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that's why the proof was so easy... < 1268511520 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what data < 1268511524 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and because < 1268511526 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :20:14 < alise_> data Apart : {A:Set} -> (x:A) -> (y:A) -> Prop where lfer : {P : A->Prop} -> ((P x /\ ~P y) \/ (P y /\ ~P x)) -> Apart x y < 1268511528 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :toProp : (b : Bool) ? S (P : Prop) (cond b ? P; else ? P) < 1268511529 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh you mean apart < 1268511536 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because === is defined as data sooo < 1268511543 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :my um / < 1268511543 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268511550 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what's the name of like .. a strategyr < 1268511552 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well here's a definition < 1268511554 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523: rings a bell < 1268511557 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :except that it's ad-hoc guidlines < 1268511571 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :rule of thumb < 1268511589 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: heuristic? < 1268511594 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes! < 1268511613 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :my hooristikc is to define the fewest data possible, but the strongest ones < 1268511614 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apart : {A:Set} -> A -> A -> Prop < 1268511621 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :like if two data are similar, you can probably abstract it out < 1268511633 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apart x y = exists {P : A->Prop}. (P x /\ ~P y) \/ (P y /\ ~P x) < 1268511633 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or something < 1268511636 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the real reason to define a data type is because you want the strength of its induction principle < 1268511644 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :at least that's my (current) view/understanding < 1268511664 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: it looks really weird whenever anyone uses the word "data" correctly < 1268511665 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well done < 1268511679 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/868253.txt?key=nb3ny4djjrabif9xilvalq honestly toBool.toProp===id should just be "obvious" < 1268511689 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :toBool.toProp===id b := obvious < 1268511740 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obvious : {P : Prop} -> cond isObvious P -> P; else -> T < 1268511763 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :tautology "P" -> P ? < 1268511806 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268511811 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :is " quoting? < 1268511835 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so tautology : (q : Quoted Prop) -> unquote q? < 1268511875 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so what's the type containing Prop and Set in your opinion? Set_1? < 1268512035 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x < 1268512035 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :scary type. < 1268512040 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :whoa there mirc < 1268512042 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what are you doing < 1268512063 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :s : {A : Set1} ? {B : Set1} ? {P : A ? B} ? (x:A) ? P x ? S (x:A). P x < 1268512063 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268512084 0 :werdan7!unknown@unknown.invalid QUIT :Ping timeout: 619 seconds < 1268512132 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268512162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :_sigma_ : {A : Set_1} -> {B : Set_1} -> {P : A -> B} -> (x:A) -> P x -> Sigma (x:A). P x < 1268512162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :anyway < 1268512210 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise in Coq it's Type (Type[1]) < 1268512217 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but I don't really have an opinion on this :P < 1268512229 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so Set : Type, Prop : Type? < 1268512255 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I kinda hate having separate Sets and Props < 1268512260 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because you lose so much isomorphism and neatness < 1268512284 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :umf < 1268512288 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't knnow what yu mean < 1268512299 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :please, please, PLEASE, when saying you don't know what i mean QUOTE the bit < 1268512301 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :otherwise I can't answer < 1268512305 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :20:30 < alise_> because you lose so much isomorphism and neatness < 1268512319 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :for instance < 1268512332 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A \/ B = Either A B < 1268512336 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A /\ B = A * B < 1268512349 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :P \/ ~P then just inspecting left/right to find out which it is < 1268512363 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :forall <-> function < 1268512370 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :exists <-> dependent tuple < 1268512374 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and so on, so forth < 1268512513 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268512528 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wait < 1268512537 0 :Phantom_Hoover!~chatzilla@cpc3-sgyl21-0-0-cust116.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268512552 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :proofs are different than types < 1268512559 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the reason is proof irrelevance < 1268512564 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i know! < 1268512575 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so why would you want to get rid of proofs?? < 1268512577 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but if you ignore proof irrelevance like agda, everything is so much prettier and curry-howardish :( < 1268512587 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION doesn't find it prettier < 1268512596 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268512608 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :agda has combined proof/set... and suffers for it, but the isomorphisms are just so appealing < 1268512608 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 for instance < 1268512608 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 A \/ B = Either A B < 1268512608 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 A /\ B = A * B < 1268512608 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 P \/ ~P then just inspecting left/right to find out which it is < 1268512609 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 forall <-> function < 1268512609 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 exists <-> dependent tuple < 1268512610 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 and so on, so forth < 1268512614 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :maybe if we used quotients!!!! < 1268512621 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :to make a 'proof' set < 1268512633 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well it's not prettier per se < 1268512634 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I suppose that's what epigram does < 1268512636 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but the isomorphisms are elegant < 1268512638 0 :werdan7!~w7@freenode/staff/wikimedia.werdan7 JOIN :#esoteric < 1268512642 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if you don't value isomorphisms - < 1268512643 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what isomorphisms? < 1268512647 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then why do we persue curry howard? < 1268512647 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :are you talking about curry-howard < 1268512649 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :for FUCK's sake < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 for instance < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 A \/ B = Either A B < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:31 A /\ B = A * B < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 P \/ ~P then just inspecting left/right to find out which it is < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 forall <-> function < 1268512650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 exists <-> dependent tuple < 1268512651 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :20:32 and so on, so forth < 1268512662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :THOSE isomorphisms < 1268512664 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :stop pasting that, I can't see what you are saying inbetween all this pastes < 1268512684 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :maybe the idea is to read the paste < 1268512684 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :instead of asking for its contents < 1268512793 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :those are (among the) appealing isomorphism s < 1268512795 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*isomorphisms < 1268512822 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't get it < 1268512883 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what part do you not get < 1268512919 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data _/\_ : (A:*) -> (B:*) -> * where both : A -> B -> A /\ B < 1268512923 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :look similar to the definition of a tuple to you? < 1268512932 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::S < 1268512958 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What, it doesn't? < 1268512963 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :curry-howard is that typed lambda calculus corresponds to natural deduction ? < 1268512977 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What I was /trying/ to do is use *analogy*. < 1268512997 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Curry-Howard: Types in the lambda calculus correspond to statements in intuitionistic logic. W < 1268513004 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Curry-Howard: Types in the lambda calculus correspond to statements in intuitionistic logic. We love this, and pursue it: it's why we make dependent languages. < 1268513013 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :is that a quote? < 1268513014 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So if you do not appreciate the isomorphisms I listed, why then Curry-Howard? < 1268513018 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1268513027 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okay let me get this straight < 1268513042 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1268513044 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no I don't get it < 1268513064 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What part? < 1268513065 0 :comex!unknown@unknown.invalid PRIVMSG #esoteric :can't you use v and ^ instead? :p < 1268513071 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm asking #haskell < 1268513074 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :comex: Yeah, it's not like v is like a variable name. < 1268513082 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: ugh, you make no sense at all < 1268513095 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*is a variable name < 1268513111 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this is my question: < 1268513112 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what does 'Curry–Howard correspondence' have to do with dependent types? < 1268513127 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Ugh! That is IRRELEVANT to my point. < 1268513134 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Dependent languages make /good proof systems/. < 1268513135 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wow < 1268513140 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why is it irrelevant < 1268513152 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Because/ of Curry-Howard. < 1268513154 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*Because < 1268513155 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*BECAUSE < 1268513197 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So we, in making our languages, support the isomorphism; recognise it as good. If you do not recognise isomorphisms as a reason for the unification of two general concepts, as in the examples I showed, why then do you recognise Curry-Howard as a good thing? < 1268513243 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure what Curry-Howard is exactly < 1268513273 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it seems kinda vauge, like a principle more than a formal statement < 1268513286 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Duh. < 1268513287 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Of course it is. < 1268513312 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you needn't be so caustic < 1268513319 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: http://lifehacker.com/5336382/digsby-joins-the-dark-side-uses-your-pc-to-make-money, http://www.downloadsquad.com/2008/11/24/new-digsby-installer-loaded-with-bloat-and-adverts/, http://www.downloadsquad.com/2009/08/14/digsby-responds-to-claims-of-shady-money-making-tactics/ < 1268513405 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Survived the first two points raised by LH < 1268513422 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So? < 1268513425 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Do you want to support such a company? < 1268513530 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Hm. What alternatives are there, then? < 1268513544 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Pidgin's been sucking for me for some reason, Digsby's company is shady < 1268513545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Uh, Pidgin? < 1268513549 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It sucks but what can you do. < 1268513559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Miranda IM is popular with the anal-retentive tweakers. < 1268513570 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A few hours and it's exactly as good as Pidgin but with more alpha-translucency. < 1268513592 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::/ < 1268513592 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION doesn't like tweaking stuff < 1268513596 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Huh; Russ Cox wrote Code Search. < 1268513600 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise just give up on me after bitching < 1268513615 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I just didn't notice what you said < 1268513620 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :There are other people than you and they talk... < 1268513631 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I give up on people after I see a conversation going in circles, only. < 1268513742 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :brb < 1268513747 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :people shouldn't repeat themselves if they don't like going in cirlecs.. < 1268513759 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Can Miranda IM be made to support Facebook Chat? < 1268513774 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Apparently yes < 1268513812 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I remember using Miranda IM once when I couldn't get Pidgin working, and I remember HATING it < 1268513815 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838] < 1268513831 0 :Phantom_Hoover!~chatzilla@cpc3-sgyl21-0-0-cust116.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268513862 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Bloody QEMU... < 1268513878 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION weeps < 1268513884 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Why? < 1268513978 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :*bangs head against keyboard* < 1268513982 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :What's wrong with Qemu? < 1268514036 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :I'm trying to run a Linux kernel with -hda as a virtual disc, but it won't mount for some reason. < 1268514138 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :If I run "qemu -m 32 -hda ./vm.img -kernel ~/.../bzImage -append "root=/dev/hda"" the console prints some stuff about not being able to mount < 1268514139 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :. < 1268514163 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Is hda a virtual disk or a filesystem? That is, is it partitioned? < 1268514181 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :You mean vm.img? < 1268514187 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yeah < 1268514198 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :It's a raw image with an ext3 filesystem on it. < 1268514211 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well, yuh, that should work, assuming the kernel has IDE support. < 1268514254 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :It doesn't work with the kernel in /boot either, so I assume the fault isn't with the kernel. < 1268514286 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh what happened... < 1268514299 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :By mistake I left clicked a tab with ctrl held down in firefox < 1268514308 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it changed the tab title to begin with "(*)" < 1268514316 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :repeating the click removes it < 1268514319 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fully reproducible < 1268514336 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but it seems to have no effect in behaviour < 1268514352 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :anyone know if it is supposed to just do that, or do something else as well? < 1268514374 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I mean, if it is just to mark a tab, or it changes something wrt. how the tab behaves < 1268514435 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it could be from tab mix plus I suppose < 1268514514 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838] < 1268514757 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise? < 1268515049 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm it does indeed seem to be related to tab mix plus < 1268515094 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268515150 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Should ChanServ really be giving me a dead link? < 1268515198 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :yes. < 1268515209 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :But it's dead! < 1268515496 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :It's bleeding demised! It's passed on! It's no more! It has ceased to be! It's expired and gone to meet its maker! < 1268515626 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :It's just resting. < 1268515639 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :back < 1268515645 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise_: not you < 1268515648 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Oh, you were right. < 1268515662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :we backed up the frappr, so bah < 1268515690 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Where is this backup? < 1268515705 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :on our hard drives < 1268515712 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster has it, so do I on my other machine < 1268515763 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Oh, does anyone now the reason for my Qemu problems? < 1268515771 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Apparently Digsby stopped bundling spyware, so I'll try it. < 1268515778 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: #qemu? < 1268515791 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise alise alise alise < 1268515822 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Tried that. It doesn't let me say anything. < 1268515894 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Identify your nickname. < 1268515897 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: What? < 1268515901 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :...How? < 1268515908 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :nickserv < 1268515918 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :...How? < 1268515929 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Just Fucking Google It < 1268515935 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :;( < 1268515946 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ghost sucker: /msg nickserv help < 1268515953 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :don't google anything < 1268515958 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :google is for idiots and queers < 1268516003 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :real defensed proposition you got there < 1268516007 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you included all that evidence and reasoning < 1268516084 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION uses a screwdriver to fix alise_'s joke detector < 1268516128 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise < 1268516132 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I have to tell you this < 1268516138 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Coq is a proof assistant based on dependent type theory developed at < 1268516138 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :INRIA [CDT08]. By default, it uses constructive logic via the Curry-Howard < 1268516138 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :isomorphism. This isomorphism associates propositions with types and proofs of < 1268516141 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :propositions with programs of the associated type. This makes Coq a functional < 1268516145 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :programming language as well as a deduction system. The identification of a pro- < 1268516148 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :gramming language with a deduction system allows Coq to reason about programs < 1268516151 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and allows Coq to use computation to prove theorems. < 1268516159 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: well fax legit hates wikipedia, so... < 1268516291 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :alise_: so what you are saying is that fax incorporates poe's law all by himself? < 1268516390 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1268516405 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Oerjan: There seems to be some vandalism on the wiki. < 1268516424 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :to the esomobile! < 1268516446 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise -- are you really pissed off at me < 1268516464 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1268516475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If I was, I would be FUCKING SHOUTING YOU RETARD <-- like that. < 1268516488 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION uses the screwdriver to fix fax's joke detector as well. < 1268516488 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"Allow Digsby to use idle CPU time for grid computing." Uh, no? < 1268516489 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okay < 1268516507 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan ? < 1268516530 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Manage all your IM, email and social < 1268516530 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :network accounts with one login < 1268516533 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: assuming you are referring to the Lazy Evaluation article? < 1268516537 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Suspicious. Do I have to give them my password? < 1268516540 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's clearly a joke < 1268516544 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lazy evaluation?? no < 1268516555 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :wait waht < 1268516571 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Me? < 1268516572 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION beats himself for confusing fax and Phantom_Hoover ===\__/ < 1268516579 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :OH! < 1268516582 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Why do I need a Digsby account? < 1268516583 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We wanted to make it easier to use Digsby at multiple locations. Your Digsby account is used to synchronize preferences such as what skin to use and whether to show popups or not. When you sit down at another computer and log in to Digsby, the experience is completely seamless. < 1268516583 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*OW! < 1268516586 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So: They store my password. < 1268516596 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :reversibly < 1268516603 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Obviously. < 1268516604 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: mind you your joke detector probably needs adjustment too < 1268516616 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::/ < 1268516622 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I TAKE OFFENSE TO THIS < 1268516626 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*Phantom_Hoover: assuming you are referring to the Lazy Evaluation article? < 1268516645 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: Digsby used to bundle adware, now by default (1) uses a browser plugin to get cashbacks when you shop online (installer setting) (2) uses your idle CPU for grid computing (3) changes your homepage to a Digsby-branded Google Search. It also stores your IM passwords. < 1268516649 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: I think I have said enough. < 1268516666 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION gives his info anyway because dammit pidgin is /really/ badf < 1268516666 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*bad < 1268516675 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268516702 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: maybe you could write your own? < 1268516713 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, even telnet is usable for IRC, but only if you don't do anything else < 1268516715 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o_o < 1268516722 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Write Windows software? Are you kidding? < 1268516737 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: I'd suggest not actually using the Windows API, that would be ridiculous < 1268516737 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*/me uses the screwdriver to fix Phantom_Hoover's joke detector as well. < 1268516748 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but can't you write portable software, and then run it on Windows? < 1268516760 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wanted to talk about dependent types/constructive math with ehird but seems not to be happening < 1268516778 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but I'd rather just get an internet connection that doesn't suck and use it to install Ubuntu. < 1268516779 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Or buy a Mac. < 1268516817 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: you can!! < 1268516821 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I love talking about those things < 1268516834 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Ooh, Digsby lets you sort contact by total size of logs. < 1268516836 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :That's interesting. < 1268516976 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :does anyone hear know what the common "now you have two problems" quip against regex means? < 1268517021 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what it means?? < 1268517030 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it means that writing regex is a bitch < 1268517035 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and doesn't make things easier < 1268517053 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ais523 is so eso-adjusted that he thinks regexes are easy :D < 1268517072 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: because regexps are brittle and often have scary performance < 1268517074 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :regex makes things easier if it's appropriate for the problem < 1268517082 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :ais523: The original quote is about sed, not regex. < 1268517086 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's a quip, it doesn't have to be actually true. < 1268517086 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :just, don't use it to parse XML or stupid things like that < 1268517096 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: recognised; Deewiant: ah, interesting < 1268517122 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :The UNIX-HATERS Handbook mentions it. < 1268517131 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :<3 unix haters handbook! < 1268517172 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :is there a windows-haters handbook? < 1268517206 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Not to my knowledge. < 1268517213 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, http://esolangs.org/wiki/Lazy_evaluation, now that's /clever/ vandalism < 1268517225 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :much better than the typical "recursion" joke < 1268517241 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268517246 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I'd leave that there < 1268517251 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm planning to < 1268517255 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Since there wasn't any content to start with < 1268517300 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also fun: Google have made a mostly PCRE-compatible regular expression engine < 1268517348 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :expanding the acronym makes your head spin < 1268517365 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268517387 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Firefox can't find the server at www.esolangs.org. :/ < 1268517391 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Yes, it's the typical "fast but can't do everything" implementation using a Thompson NFA < 1268517399 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ... why? < 1268517408 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://esoteric.voxelperfect.net/wiki/Lazy_evaluation < 1268517408 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: better worst-case performance < 1268517428 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so they can let people write arbitrary regexen and evaluate them without worrying about someone sending them an algorithmic complexity bomb < 1268517430 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Except that worst-case performance of PCRE is almost a non-issue, the worst case never comes up ... < 1268517434 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Ahhh < 1268517437 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Arbitrary regex < 1268517438 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Most properly-maintained things use the slow algos < 1268517443 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :User-created malicious regex. < 1268517444 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Gotcha. < 1268517541 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268517545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Russ Cox wrote it < 1268517550 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Only now do I get the lazy evaluation page. < 1268517551 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the same author of the famous article about it < 1268517559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(and the author of Google Code Search which uses it) < 1268517761 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Russ Cox??? < 1268517946 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268517965 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise_ < 1268517966 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :PM me < 1268518053 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: can't you PM alise? < 1268518060 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1268518065 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :she doesn't want to talk to me < 1268518095 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :there is something wrong with this reasoning... < 1268518099 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Mayhaps that's because you mistook him for a woman :P < 1268518116 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hey, I've been careful for ages to avoid pronouns for alise, it's more fun that way < 1268518131 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, third-person pronouns at least < 1268518134 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Actually, she is the correct pronoun. < 1268518139 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :imagine if "I" and "you" were gendered! < 1268518143 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It in fact matches reality more than he. < 1268518146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Most people mistake me for a girl. < 1268518168 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ounapfhounfakp < 1268518175 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Hotels: "Miss (mother's surname because I'm never asked for mine)". Taxis: "[Blah blah destination] ladies?" < 1268518189 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :People, to my mother: "Blah blah blah your daughter" < 1268518192 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So on, so forth. < 1268518198 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I'll talk if you say something to me. < 1268518198 0 :Phantom_Hoover!unknown@unknown.invalid PRIVMSG #esoteric :Weird. < 1268518202 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1268518239 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268518249 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Phantom_Hoover: Long hair + ULTRA-SOFT PERSONALITY YO < 1268518260 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :+ young so no GRATUITOUS BODILY HAIR AND ADAM'S APPLE = Female! < 1268518268 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :wait until you hit puberty :( < 1268518302 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Hey, I have. It's just taking its sweet, sweet time :P < 1268518348 0 :Phantom_Hoover!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.8/20100214235838] < 1268518598 0 :mano0o0!unknown@unknown.invalid PART #esoteric :? < 1268518606 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :;( < 1268518621 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Your girliness was pretty conclusively proven by that one video, you know. < 1268518646 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :video ? < 1268518667 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I showed my female genitals! (not really) < 1268518671 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :gross < 1268518771 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1268518827 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :|: < 1268518837 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I wish someone would talk to me about deptypes < 1268518857 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: did you see my talk about Confloddle in the log? < 1268518896 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :deptypes are so depressing. it's in the name, really. < 1268518906 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION didn't see ais523's talk < 1268518909 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :-_-- < 1268518919 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it's a new esolang I'm thinking about < 1268518929 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :tarpit, as usual; I like tarpits that work differently from other tarpits < 1268518936 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: So SAY SOMETHING! < 1268518939 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :tits < 1268518967 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the only data type is the list (also function literals, but functions can't be manipulated in any way, just run, and there are no closures) < 1268518975 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Okay, how about this: Make a paraconsistent deptyped language. < 1268518985 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and there are only two operators/commands, cons and foldl < 1268518991 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't know what paraconsistent it but it sounds stupid < 1268519001 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cunning tarpal syndrome < 1268519003 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'd explain but I've forgotten how to spell a word < 1268519005 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And google isn't loading < 1268519006 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sec < 1268519020 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :That is, p and ~p are allowed to coexist (dialetheia). You could do this by weakening _|_ -> forall a, a. < 1268519025 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I think this leads to a TC lang with 5 characters re<>: without cheating (the same way that BF is 8 ,.<>+-[] without cheating, although of course BF can be cut down) < 1268519072 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Nested folding on infinite lists seems trivially TC to me. < 1268519077 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: idea -- eliminate > < 1268519080 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :< lasts til end of program? < 1268519086 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, <> delimit a function < 1268519092 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No <> is foldr < 1268519097 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :<> is foldl < 1268519100 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :er right < 1268519102 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and what's inside them is the function you fold on < 1268519104 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :With infinite lists maybe this is acceptable, just having < last until EOF < 1268519109 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Try it. < 1268519112 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, there's only one infinite list < 1268519130 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :necessary because you can't return an infinite list in finite time < 1268519149 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :< until EOF isn't obviously sub-TC, though < 1268519183 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://en.wikipedia.org/wiki/Paraconsistent_logic < 1268519183 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :go for it < 1268519191 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Exactly. < 1268519198 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Wait, how do you combine r and e? < 1268519204 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh, is re cons r e? < 1268519212 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, it's reverse-polish < 1268519215 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :re is a syntax error < 1268519219 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :re: is cons r e < 1268519229 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh, I didn't see : < 1268519255 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and is foldl `cons` [] < 1268519257 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in other words, list reverse < 1268519261 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :" < 1268519288 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Can this be written without >? < 1268519294 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :not obviously < 1268519297 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Perhaps by accumulating something into the result then folding on that. < 1268519338 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: So you want me to talk, then you dismiss and ignore me? < 1268519343 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268519346 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I think you have to grab the results of a calculation at the start of the next iteration of the main loop < 1268519350 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I didn't want to interrupt ais < 1268519359 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :we can interleave :) < 1268519362 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or use /msg < 1268519364 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: this is IRC, if you can't have two conversations at the same time you aren't concentrating enough < 1268519374 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ooh, nice < 1268519379 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but it has to be part of the main fold < 1268519385 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268519397 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if we're having trouble just expressing first element of a list, this is either sub-tc or brilliantly TC < 1268519402 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and you have Confloddle's general issue with initialising < 1268519423 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the real problem here, is that insisting on using < but not > means that you can't get the return value from <> immediately < 1268519430 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you only get it in r on the next iteration of the loop < 1268519439 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268519447 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://en.wikipedia.org/wiki/Paraconsistent_logic#Relation_to_other_logics dual-intuitionistic logic may be a good place to steal things from < 1268519452 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but it has to be a proper language not just a logic < 1268519456 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okay < 1268519464 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: so basically we need < 1268519480 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if we're done then , so why not for the main loop too? < 1268519758 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268519758 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so what does Xr: do < 1268519770 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :just that < 1268519770 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what list does it result in, using X as a var < 1268519789 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :[X | r] (prolog syntax) < 1268519801 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what is r < 1268519810 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :r is the result of the last iteration of the current <> < 1268519813 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ffff < 1268519815 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :just this program < 1268519816 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :on its own < 1268519816 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Xr: < 1268519821 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what result does it yield? < 1268519845 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, the main loop doesn't leave a result at all, but the value of r on each iteration goes [X] [X X] [X X X] and so on < 1268519871 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :so if you can imagine you're using Proud or some other uncomputable lang to implement this, the return value is an infinite list of Xs < 1268519876 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but in a TC system, you never get that far < 1268519921 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh, you could < 1268519926 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :consider haskell < 1268519929 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, you could optimise that case < 1268519931 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fix (1:) = [1,1,1,1,1,1,... < 1268519941 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, ooh, lazy evaluation? < 1268519942 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ok, so r is {}? < 1268519949 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :at the start < 1268519952 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :r is initially a null list, yes < 1268519954 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :for any <> < 1268519957 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so the whole program is a fold, right < 1268519958 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so < 1268519959 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :er: < 1268519965 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what result does that yield < 1268519969 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :e and r are both {} < 1268519971 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so it should be {{}} < 1268519977 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so you should get {{{}}, {{}}, ... < 1268519978 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :right/ < 1268519978 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, the entire program's implicitly in a <> < 1268519981 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*right? < 1268519987 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh, good point < 1268519989 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so you get... < 1268519994 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :outside <> e and r have no meaning, but you can't be outside a <> < 1268519995 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :{ {{}, {}, {}, {}, ...} } < 1268519996 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think < 1268520003 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, because the return value is the final value of r < 1268520020 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :there isn't a "final" one, but if there was, it would be [ [] [] [] [] [] ... ] < 1268520132 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so > < 1268520158 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yes, I see that < 1268520164 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I bet we can use the main fold as storage for inner ones < 1268520168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm... cons ought to be prefix < 1268520168 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in fact, that's obviously the only way to do practical non-> programs < 1268520171 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and so do I < 1268520172 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so we can do :xy<... < 1268520176 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268520177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::x<... < 1268520183 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I agree that prefix is much better than postfix in non-> programs < 1268520190 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :postfix would be better for non-< programs < 1268520196 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :also, just make it foldr and I think you can do laziness trivially < 1268520200 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and hey, a small syntax change doesn't matter if you're trying to tarpit something more < 1268520208 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, foldr is really laziness-hostile < 1268520214 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :because it starts with the last element of a list < 1268520220 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and to determine that, you have to force it < 1268520249 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268520250 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :OTOH, foldl doesn't work too well either, because you have to force it to determine the final value of r < 1268520331 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 < 1268520339 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: that is not what foldr is... < 1268520358 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, I see < 1268520365 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr f x [e1,e2,e3,...] = f e1 (f e2 (f e3 x)) < 1268520369 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it works on infinite lists < 1268520373 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :unlike foldl < 1268520377 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :a lazy foldr, to determine the final r, you determine the final e and the penultimate r < 1268520382 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and the second can be left lazy < 1268520386 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :consider foldr (:) [] [1..] < 1268520391 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :-> (:) 1 ((:) 1 ... < 1268520396 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :-> [1,1,1,...] < 1268520399 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, I get it now < 1268520418 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :is cons and foldr TC, though? < 1268520422 0 :Phantom_Hoover!~chatzilla@cpc4-sgyl29-2-0-cust108.sgyl.cable.virginmedia.com JOIN :#esoteric < 1268520434 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :how do you, say, get the last element of a list? or the second? < 1268520439 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :getting the second seems easier < 1268520468 0 :Phantom_Hoover!unknown@unknown.invalid PART #esoteric :? < 1268520469 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> take 10 $ foldr (\n xs -> n : map succ xs) [] [1..] < 1268520470 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[1,3,5,7,9,11,13,15,17,19] < 1268520477 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: btw foldr = foldl, they're implementable in terms of each other (lazily) < 1268520485 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :also, last element of a list with foldr... < 1268520495 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :not purely each other, surely, you need to mess with at least some other primitives? < 1268520502 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and if there's something confloddle is short of, it's primitives < 1268520521 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :first is < 1268520524 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: nope < 1268520525 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well < 1268520527 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :with cons and stuff < 1268520529 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :anyway < 1268520531 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :first elem is < 1268520536 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the "stuff" is the problem < 1268520541 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :first is , anyway, with foldr < 1268520545 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm... let's make it >e< < 1268520546 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr' (\x _ -> x) [1,2,3] < 1268520550 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*foldr1 < 1268520552 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :different notation so it's clear that we're doing something different < 1268520553 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(not that that exists, but) < 1268520557 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wait yes it does < 1268520563 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :although it's a -> a -> a ofc < 1268520566 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which is upsettingly restricting < 1268520578 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but that doesn't concern you since yours is dynamically typed < 1268520578 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :foldr1 does exist in Haskell < 1268520579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but < 1268520586 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :don't you want an initial value? < 1268520596 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :confloddle's is (foldl []) though < 1268520602 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :last element is < 1268520605 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr1 (\x y -> y) < 1268520611 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(isn't that easy?) < 1268520619 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise_, did I mention that I'm considering making a Scheme? < 1268520620 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that's cheating < 1268520624 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no it is not < 1268520625 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :foldr1 special-cases the last eleemnt < 1268520630 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :???? < 1268520635 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh you are right < 1268520679 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :btw reverse is < 1268520684 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr (\x y -> y ++ [x]) < 1268520698 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :you can do head on that < 1268520713 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sp < 1268520713 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so < 1268520727 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr [] (\x _ -> x) . foldr [] (\x y -> y ++ [x]) < 1268520746 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that fails to type but whatever :) < 1268520750 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the [] should be after < 1268520777 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> (foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) []) [[1,2],[3,4]] < 1268520777 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[3,4] < 1268520808 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I agree with that definition, but ++ looks hard to do in a foldr-version of confloddle (conflodder?) < 1268521510 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I did ++ < 1268521513 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :folr (\xs ys -> foldr (:) ys xs) [] < 1268521515 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*foldr < 1268521540 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't see how that works < 1268521545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :how would you write that in conflodder? assuming > exists < 1268521547 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :because the whole thing seems to only take one argument < 1268521556 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[list1,list2] < 1268521572 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i.e. list1list2[]:: < 1268521586 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and it's hard to do easily, because there's no way to have a second arg to foldr of anything but [] < 1268521604 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :in confloddle you can get around that by putting every element into a singleton list, and messing around with cons and last < 1268521607 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: try and make a logic-computation isomorphism for http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 < 1268521613 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so where statements in that are types; give them semantic values < 1268521623 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: So do that < 1268521686 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :as in, instead of [a b c] you have [[a] [b] [c]], then foldl x y z is the same as foldl (\r -> x (last (cons y r))) [] z < 1268521696 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I think, I may have got the arguments the wrong way round < 1268521712 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so do that :) < 1268521719 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you have circularitiy problems trying that trick with foldr, though, as you'd have to implement last first < 1268521735 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and the same trick doesn't work with first, unfortunately < 1268521751 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdfview_1&handle=euclid.ndjfl/1039886520 < 1268521751 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :erm < 1268521760 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ugh < 1268521762 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pdf doesn't allow copying < 1268521779 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: basically there's a dual-intuitionistic set theory that has russell's paradox but is consistent < 1268521785 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Hey, I implemented last. < 1268521795 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :thsat's cscrewad < 1268521798 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(foldr (\x _ -> x) [] . foldr (\x y -> y ++ [x]) []) < 1268521806 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: please learn to type :| < 1268521808 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :anyway do it! < 1268521810 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, but that's implemented in terms of ++ < 1268521817 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it will be fucking awesome to have computational dual-intuitionistic < 1268521823 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: ah :-D < 1268521825 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :What does it mean for something to have Russell's paradox but be consistent... < 1268521834 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: it means it allows p & ~p < 1268521839 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :which is what paraconsistent logics do < 1268521842 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Oh. < 1268521865 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dual-intuitionistic logic is intuitionistic logic's goatee-sporting, paraconsistent twin < 1268521865 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the major issue with foldr is finding just some way to do a foldr1 or a foldr with non-[] second arg or last or ++ or, well, anything < 1268521884 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION defines fold f = foldr f [] to keep himself honest < 1268521890 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I wonder if intuitionistic logic and paraconsistent logic are isomorphic somehow. < 1268521894 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: maybe you should have a better last thing than [] < 1268521901 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Paraconsistent logic is a class of logics. < 1268521909 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I can't think of anything obvious; maybe I should go at it Wolfram-style and just generate loads of Conflodder programs to see if any do last < 1268521915 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Intuitionistic logic's "opposite", dual-intuitionistic, is paraconsistent. < 1268521922 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :ACTION nods. < 1268521986 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So, does the Web have any proof databases that accept all and only valid proofs? < 1268521994 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Using an automatic proof verifier, of course. < 1268522000 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :metamath < 1268522024 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: < 1268522025 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268522025 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Prelude> fold (\xs ys -> fold (\xs' ys' -> (xs' : ys') ++ ys) xs) [[1,2],[3,4]] < 1268522026 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[1,2,3,4,3,4] < 1268522030 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Can I simply submit a proof to Metamath and see it appear? < 1268522032 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it's incorrect and depends on ++ but I think I'm honing in on a solution < 1268522035 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'll ask #haskell < 1268522036 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: no. < 1268522039 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax wants that < 1268522070 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I also want that. < 1268522083 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :If fax is a programmer, maybe we can collaborate on getting that. < 1268522130 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax hates programming < 1268522133 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's a project of mine though < 1268522137 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Metastruct < 1268522173 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :It's a project of yours? Neat. < 1268522205 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes. No work done yet, but... < 1268522208 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :What programming language are you using, and what proof system are you using? < 1268522212 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :My own, my own. < 1268522222 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Same here. It's a project of mine with no work done. :P < 1268522233 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :#haskell seems a non-obvious place to ask for easolangs < 1268522235 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well. The proof system (dependent language) will be written in Haskell and so will be the website, but... < 1268522235 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Except mine's called Kallipolis, written in Haskell, using Agda. < 1268522242 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Why not write it in Agda? < 1268522254 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Hmm. < 1268522261 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Agda doesn't have proof irrelevance < 1268522263 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :sucks to be you < 1268522270 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Proof irrelevance? < 1268522271 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: somewhat offtopic: "I object to this attempt to initiate an Emergency. Per rule 31 of the previous ruleset, the change to the gamestate that prevents us from making arbitrary rule changes is cancelled retroactively, and we're still in the BGora Era." < 1268522277 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :does that even work? < 1268522292 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Google it. < 1268522312 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: wat. < 1268522318 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm... idea < 1268522327 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Google's not giving much useful. < 1268522399 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :23:18 alise_: can you write reverse with foldl, then do a left fold (which is a right fold on the original), and then reverse again if you produced a list? < 1268522399 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :23:18 as in can you flip the arguments to cons? < 1268522403 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: in confludder < 1268522418 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :So what's proof irrelevance? < 1268522425 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: that's how you do foldr in terms of foldl < 1268522429 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Didn't I tell you to google it? < 1268522432 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :rather than vice versa < 1268522445 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :alise_: yes, and I did Google it, and I came away with no impression of what it is. < 1268522527 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Hmm, is it the equality of all proofs of a statement? < 1268522534 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Yes. < 1268522536 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Agda doesn't even have equality testing. < 1268522539 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes it does. < 1268522544 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :See the standard library. < 1268522561 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Really? Huh. < 1268522570 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :data _===_ : {A:Set} -> (x:A) -> A -> Set where refl : x === x < 1268522584 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Use Coq or something else with proof irrelevance. < 1268522593 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :At least until they add it. < 1268522641 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Why is proof irrelevance so important? < 1268522674 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :because it simplifies a lot of stuff. < 1268522872 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :23:26 > let xs ++ ys = let f = foldl (flip (:)) in f (f [] xs) (f [] ys) in "abc " ++ "alise_" < 1268522873 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :23:26 "alise_ cba" < 1268522891 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :foldr fial < 1268522892 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*fail < 1268522994 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: for instance proof irrelevance makes equality nicer < 1268523107 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :Maybe you can write a spec for your stuff and I can write it. < 1268523123 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I can do both because I hate collaborating :P < 1268523129 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268523228 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :someone paste me the unicode mathematical [[ ]] chars :( < 1268523233 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :MATHEMATICAL LEFT WHITE BRACKET or something < 1268523356 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :⟦⟧ < 1268523367 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :took a while to find < 1268523374 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :thanks :P < 1268523378 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and it's MATHEMATICAL LEFT WHITE SQUARE BRACKET, etc, you were almost right < 1268523783 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We use G ? ?, to denote that if we reject all formulas of G, we have to reject the formula ?. < 1268523788 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ufg < 1268523789 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ugh < 1268523798 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :X -| Y < 1268523803 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :X < 1268523804 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Y < 1268523826 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.2290&rep=rep1&type=pdf < 1268523841 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :!haskell let x ++ y = foldr (:) y x in [1,2,3] ++ [4,5,6] < 1268523855 0 :EgoBot!unknown@unknown.invalid PRIVMSG #esoteric :[1,2,3,4,5,6] < 1268523909 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: no < 1268523913 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fold f = foldr f [] < 1268523927 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :grmbl < 1268524018 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm you cannot put _either_ x or y after that for any f and get x ++ y, because [] will be wrong < 1268524180 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm that [[1,2],[3,4]] thing... < 1268524193 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :which would be concat not ++, but... < 1268524210 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh wait < 1268524241 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well i'm not sure it is possibl < 1268524243 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*e < 1268524284 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268524357 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :What postscript viewer should I use for Windows? < 1268524365 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :gsview is nice except that it sucks, horribly.