> 1531959411 591295 PRIVMSG #esoteric :14[[07Stupid14]]4 M10 02https://esolangs.org/w/index.php?diff=56850&oldid=56558 5* 03Oerjan 5* (-27) 10rm nonexistent category
> 1531959438 889577 PRIVMSG #esoteric :14[[07Stop14]]4 M10 02https://esolangs.org/w/index.php?diff=56851&oldid=56564 5* 03Oerjan 5* (-27) 10rm nonexistent category
> 1531959572 261896 PRIVMSG #esoteric :14[[07EsoScript14]]4 M10 02https://esolangs.org/w/index.php?diff=56852&oldid=56822 5* 03Oerjan 5* (-4) 10fix category
> 1531959590 435781 PRIVMSG #esoteric :14[[07Bit Stupid14]]4 M10 02https://esolangs.org/w/index.php?diff=56853&oldid=56562 5* 03Oerjan 5* (-27) 10rm nonexistent category
> 1531959629 841911 PRIVMSG #esoteric :14[[07Array Changer14]]4 M10 02https://esolangs.org/w/index.php?diff=56854&oldid=56244 5* 03Oerjan 5* (-27) 10fix categories
< 1531960571 658491 :imode!~imode@unaffiliated/imode JOIN :#esoteric
< 1531962829 391523 :oerjan!oerjan@hagbart.nvg.ntnu.no QUIT :Quit: Nite
< 1531963145 579799 :XorSwap!~XorSwap@wnpgmb016qw-ppp-103-253.dynamic.bellmts.net JOIN :#esoteric
< 1531963385 400386 :pikhq!~pikhq@c-73-181-126-9.hsd1.co.comcast.net QUIT :Ping timeout: 240 seconds
< 1531965016 667873 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531965267 663995 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 240 seconds
< 1531965633 625941 :Sgeo__!~Sgeo@ool-18b98dd9.dyn.optonline.net QUIT :Quit: Leaving
< 1531965672 670569 :Sgeo!~Sgeo@ool-18b98dd9.dyn.optonline.net JOIN :#esoteric
< 1531965968 819969 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Ping timeout: 255 seconds
< 1531967660 665569 :pikhq!~pikhq@c-73-181-126-9.hsd1.co.comcast.net JOIN :#esoteric
> 1531968009 554078 PRIVMSG #esoteric :14[[07User:A14]]4 10 02https://esolangs.org/w/index.php?diff=56855&oldid=56847 5* 03A 5* (-69) 10
< 1531968207 680234 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531968477 687440 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 240 seconds
> 1531968567 582681 PRIVMSG #esoteric :14[[07Telegram14]]4 10 02https://esolangs.org/w/index.php?diff=56856&oldid=26665 5* 03A 5* (+578) 10Unsure...
> 1531968604 695951 PRIVMSG #esoteric :14[[07Telegram14]]4 10 02https://esolangs.org/w/index.php?diff=56857&oldid=56856 5* 03A 5* (+7) 10Aw man...too messy!
> 1531968803 510083 PRIVMSG #esoteric :14[[07User:A14]]4 10 02https://esolangs.org/w/index.php?diff=56858&oldid=56855 5* 03A 5* (+15) 10
> 1531969504 918390 PRIVMSG #esoteric :14[[07Talk:Logic14]]4 N10 02https://esolangs.org/w/index.php?oldid=56859 5* 03A 5* (+162) 10Created page with "==Actually more shorter CAT program==  I-|    &-O  1-| That is a lot shorter. I think the CAT program in the page is user-unfriendly.--[[User:A]]11:04 19 Jul.2018"
> 1531969555 868422 PRIVMSG #esoteric :14[[07Talk:Logic14]]4 10 02https://esolangs.org/w/index.php?diff=56860&oldid=56859 5* 03A 5* (-5) 10Bad grammar.
< 1531971256 742191 :rdococ!rdococ@cheapiesystems.com QUIT :Changing host
< 1531971256 802222 :rdococ!rdococ@unaffiliated/rdococ JOIN :#esoteric
< 1531974571 748018 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531974875 711101 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 276 seconds
< 1531977469 493628 :XorSwap!~XorSwap@wnpgmb016qw-ppp-103-253.dynamic.bellmts.net QUIT :Ping timeout: 244 seconds
< 1531977529 147673 :MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net JOIN :#esoteric
< 1531977810 329274 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531978065 298222 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 245 seconds
> 1531978207 669240 PRIVMSG #esoteric :14[[07Shorten your Brainfuck code14]]4 M10 02https://esolangs.org/w/index.php?diff=56861&oldid=56721 5* 03A 5* (+59) 10
< 1531978232 162258 :lynn_!sid154965@gateway/web/irccloud.com/x-bchkvpjlrzapffgz JOIN :#esoteric
< 1531978271 29354 :lynn!sid154965@gateway/web/irccloud.com/x-rtmaqvnphnrjfapq QUIT :Ping timeout: 276 seconds
< 1531978274 458399 :lynn_!sid154965@gateway/web/irccloud.com/x-bchkvpjlrzapffgz NICK :lynn
< 1531978404 174673 :lynn!sid154965@gateway/web/irccloud.com/x-bchkvpjlrzapffgz NICK :Guest55067
< 1531980112 858976 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric
< 1531981256 684128 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531981527 666980 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 240 seconds
< 1531981563 716700 :moei!~moei@softbank221078042071.bbtec.net JOIN :#esoteric
< 1531984232 777608 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531984490 771321 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 255 seconds
< 1531984591 644355 :aloril_!~aloril@80.246.146.6 QUIT :Ping timeout: 268 seconds
< 1531984646 10937 :aloril_!~aloril@80.246.146.6 JOIN :#esoteric
< 1531985043 700769 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1531986372 469136 :AnotherTest!~turingcom@natx-145.kulnet.kuleuven.be JOIN :#esoteric
< 1531986395 435497 :APic!apic@apic.name QUIT :Ping timeout: 240 seconds
< 1531989523 8507 :FreeFull!~freefull@defocus/sausage-lover QUIT :Quit: Rebooting
< 1531989595 679298 :FreeFull!~freefull@defocus/sausage-lover JOIN :#esoteric
< 1531990940 720107 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric
< 1531991372 791593 :imode!~imode@unaffiliated/imode QUIT :Ping timeout: 276 seconds
< 1531993008 629853 :SopaXT!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric
< 1531993027 225630 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Disconnected by services
< 1531993029 324161 :SopaXT!~SopaXorzT@unaffiliated/sopaxorztaker NICK :SopaXorzTaker
< 1531993126 493361 :SopaXT!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric
< 1531993713 501176 :SopaXT!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Ping timeout: 244 seconds
> 1531995210 541214 PRIVMSG #esoteric :14[[07Far14]]4 10 02https://esolangs.org/w/index.php?diff=56862&oldid=56530 5* 03GibsonGeorge 5* (+60) 10
< 1531998380 88926 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Remote host closed the connection
< 1531998412 696456 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric
< 1531998806 78292 :lldd_!~atrapado@unaffiliated/atrapado JOIN :#esoteric
< 1531999992 950163 :APic!apic@apic.name JOIN :#esoteric
< 1532002916 804625 :moei!~moei@softbank221078042071.bbtec.net QUIT :Ping timeout: 276 seconds
> 1532005568 312701 PRIVMSG #esoteric :14[[07Surtic14]]4 M10 02https://esolangs.org/w/index.php?diff=56863&oldid=56624 5* 03Digital Hunter 5* (+41) 10/* S */
< 1532006640 192110 :fungot!~fungot@momus.zem.fi QUIT :Ping timeout: 256 seconds
< 1532006656 680147 :fungot!~fungot@momus.zem.fi JOIN :#esoteric
< 1532010173 526293 :aloril_!~aloril@80.246.146.6 QUIT :Remote host closed the connection
< 1532011043 676187 :aloril!~aloril@80.246.146.6 JOIN :#esoteric
< 1532011224 508575 :oerjan!oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric
< 1532012081 160095 :aloril!~aloril@80.246.146.6 QUIT :Remote host closed the connection
< 1532012432 649456 :aloril!~aloril@80.246.146.6 JOIN :#esoteric
< 1532014421 581247 :AnotherTest!~turingcom@natx-145.kulnet.kuleuven.be QUIT :Ping timeout: 244 seconds
< 1532014471 566364 :XorSwap!~XorSwap@wpa-4-1743.cc.umanitoba.ca JOIN :#esoteric
< 1532014699 681789 :PinealGlandOptic!~PinealGla@82.144.205.57 JOIN :#esoteric
< 1532015698 270493 :PinealGlandOptic!~PinealGla@82.144.205.57 QUIT :Quit: leaving
< 1532015743 366020 :yurichev!~yurichev@82.144.205.57 JOIN :#esoteric
< 1532016574 834451 :oerjan!oerjan@hagbart.nvg.ntnu.no QUIT :Quit: Later
< 1532017242 481322 :XorSwap!~XorSwap@wpa-4-1743.cc.umanitoba.ca QUIT :Ping timeout: 244 seconds
< 1532017395 361228 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric
< 1532017981 712510 :AnotherTest!~turingcom@d51A46C74.access.telenet.be JOIN :#esoteric
< 1532018206 384143 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Quit: Leaving
< 1532020050 350557 :XorSwap!~XorSwap@wpa-4-1743.cc.umanitoba.ca JOIN :#esoteric
< 1532020595 447365 :deltab!~deltab@ds6266.dedicated.turbodns.co.uk QUIT :Ping timeout: 256 seconds
< 1532021649 163289 :erkin!~erkin@unaffiliated/erkin QUIT :Quit: Ouch! Got SIGIRL, dying...
< 1532022641 794516 :deltab!~deltab@ds6266.dedicated.turbodns.co.uk JOIN :#esoteric
< 1532023016 749474 :LKoen!~LKoen@vbo91-6-78-245-243-132.fbx.proxad.net JOIN :#esoteric
< 1532023328 666065 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric
< 1532023479 787153 :imode!~imode@unaffiliated/imode JOIN :#esoteric
> 1532023926 431381 PRIVMSG #esoteric :14[[07User:TuxCrafting14]]4 10 02https://esolangs.org/w/index.php?diff=56864&oldid=48916 5* 03TuxCrafting 5* (+27) 10
< 1532023927 466725 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric
< 1532024090 670981 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net QUIT :Ping timeout: 256 seconds
< 1532024139 378795 :XorSwap!~XorSwap@wpa-4-1743.cc.umanitoba.ca QUIT :Ping timeout: 260 seconds
< 1532024525 26805 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net JOIN :#esoteric
< 1532024683 614148 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net QUIT :Read error: Connection reset by peer
< 1532024752 896111 :erkin!~erkin@unaffiliated/erkin QUIT :Quit: Ouch! Got SIGIRL, dying...
< 1532024921 606799 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net JOIN :#esoteric
< 1532024959 342604 :erkin!~erkin@unaffiliated/erkin JOIN :#esoteric
< 1532025027 646142 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net PRIVMSG #esoteric :Why lemons?
< 1532025050 216011 :myname!~myname@ks300980.kimsufi.com PRIVMSG #esoteric :those lemon whores!
< 1532025113 579479 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net PRIVMSG #esoteric :yes they arid but?
< 1532025351 38335 :Lean1!~lean@14.red-83-37-124.dynamicip.rima-tde.net PART :#esoteric
< 1532028006 785759 :S_Gautam!uid286066@gateway/web/irccloud.com/x-fbfwekuqlvpqqnjf QUIT :Quit: Connection closed for inactivity
< 1532028036 928857 :yurichev!~yurichev@82.144.205.57 QUIT :Quit: leaving
< 1532028231 965755 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`olist 1128
< 1532028232 639116 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :olist 1128: shachaf oerjan Sgeo FireFly boily nortti b_jonas
< 1532028620 407168 :nchambers!nchambers@learnprogramming/staff/nchambers NICK :uplime
> 1532029183 829195 PRIVMSG #esoteric :14[[07User:DMC14]]4 M10 02https://esolangs.org/w/index.php?diff=56865&oldid=56784 5* 03DMC 5* (-78) 10
< 1532030114 177126 :lldd_!~atrapado@unaffiliated/atrapado QUIT :Quit: Leaving
< 1532030984 792791 :atslash!~atslash@static.231.107.9.5.clients.your-server.de QUIT :Ping timeout: 255 seconds
< 1532031023 617441 :MDead!~MDude@c-73-187-225-46.hsd1.pa.comcast.net JOIN :#esoteric
< 1532031085 721979 :moei!~moei@softbank221078042071.bbtec.net JOIN :#esoteric
< 1532031104 408136 :MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net QUIT :Ping timeout: 260 seconds
< 1532031108 80812 :MDead!~MDude@c-73-187-225-46.hsd1.pa.comcast.net NICK :MDude
< 1532031222 505435 :atslash!~atslash@static.231.107.9.5.clients.your-server.de JOIN :#esoteric
< 1532032149 869668 :MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net QUIT :Ping timeout: 264 seconds
< 1532034181 336859 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric
< 1532034267 716861 :ais523!~ais523@unaffiliated/ais523 QUIT :Remote host closed the connection
< 1532034280 926228 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric
< 1532034547 451682 :erkin!~erkin@unaffiliated/erkin QUIT :Quit: Ouch! Got SIGIRL, dying...
< 1532034565 432589 :LKoen!~LKoen@vbo91-6-78-245-243-132.fbx.proxad.net QUIT :Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”
< 1532034615 381932 :tromp!~tromp@ip-217-103-3-94.ip.prioritytelecom.net JOIN :#esoteric
< 1532035099 627088 :subleq!~gavin@207.173.246.52 JOIN :#esoteric
< 1532035125 165392 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :Are there any formal languages that do not always halt, but have a decideable halting problem?
< 1532035152 998090 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's fairly easy to create one
< 1532035167 507209 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :but finite state automata with halt states are the most obvious example
< 1532035179 737686 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :any infinite loop in those is detectable, so you can just run them until they halt or enter an infinite loop
< 1532035217 147044 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I think even with PDAs, all infinite loops are detectable, but I'm less sure on that
< 1532035729 881481 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :you'll see the same state with the same stack iff it doesn't terminate i think
< 1532035763 672582 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :not necessarily the same, but the stack will form a repeating pattern
< 1532035771 587386 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :hmm
< 1532035780 551881 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so you can see that the loop only looks at, say, the top 10 stack elements before repeating
< 1532035794 874089 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :and after that point the top 10 elements are the same, even if they might be at a different position on the stack
< 1532035801 223489 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :right
< 1532035960 568222 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :are there any programming languages equivalent to a PDA?
< 1532035970 321363 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :plenty
< 1532036014 54729 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :like?
> 1532036015 608499 PRIVMSG #esoteric :14[[07Esolang:Categorization14]]4 10 02https://esolangs.org/w/index.php?diff=56866&oldid=56573 5* 03Ais523 5* (+35) 10/* Computational class */ add the PDA category to the list; we've been using it for years
< 1532036026 470999 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :here: https://esolangs.org/wiki/Category:Push-down_automata
< 1532036034 478560 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :Befunge-93 is probably the best known
> 1532036096 246382 PRIVMSG #esoteric :14[[07Funge-9814]]4 M10 02https://esolangs.org/w/index.php?diff=56867&oldid=53358 5* 03Ais523 5* (-33) 10not a PDA; the existence of the stack stack (together with a swap instruction) gives it more storage than that
< 1532036187 29390 :ais523!~ais523@unaffiliated/ais523 QUIT :Remote host closed the connection
< 1532036199 481146 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric
< 1532036234 70472 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :are you aware of any restrictions on lambda calculus that could work?
< 1532036299 616165 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's a bit complex, but "all arguments to a recursive or indirectly recursive call must be constants" works
< 1532036310 813104 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :i guess just adding a loop primative 
< 1532036314 926214 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :or https://esolangs.org/wiki/Splinter is pretty similar
< 1532036322 837573 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :to a strongly normalizing lambda calculus would work
< 1532036354 295254 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :typed lambda calculus + tail-recursion (the closest lambda calculus equivalent to a while loop) is probably TC, I'm not 100% sure on that though
< 1532036873 547238 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :i mean something like this https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter11/RunIO.idr
< 1532037033 952366 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :actually I'm not certain that any given type in typed lambda calculus has infinitely many functions of that type…
< 1532037079 873721 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :what?
< 1532037144 521425 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :like, if there are only finitely many functions of each type
< 1532037159 396678 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :then typed lambda calculus + tail-recursion would be a finite state machine, as there's a limited amount of state in the system
< 1532037293 977209 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :come to think of it, i'm not sure this is an interesting question, unless decidable halting languages are in a different class than always halting
< 1532037352 625707 :MDude!~MDude@c-73-187-225-46.hsd1.pa.comcast.net JOIN :#esoteric
< 1532037430 312893 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :well, you can normally define "provably not halting" as a form of halting all of its own
< 1532037450 422026 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :because if you can prove it doesn't halt, now you know the eventual fate of the program
< 1532037454 660274 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :hah!
< 1532037462 969110 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :from that point of view, decidably-halting and always-halting aren't very different
< 1532037472 750568 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :indeed
> 1532037945 512615 PRIVMSG #esoteric :14[[0714]]4 10 02https://esolangs.org/w/index.php?diff=56868&oldid=56787 5* 03Fogity 5* (-1300) 10Now refers to the official documentation instead of trying to summarise the language details.
< 1532038410 92900 :int-e!~noone@int-e.eu PRIVMSG #esoteric :subleq: https://mathoverflow.net/questions/261934/is-simply-typed-lambda-calculus-with-fixed-point-combinator-turing-complete (first answer) is a fun one.
< 1532038445 782758 :AnotherTest!~turingcom@d51A46C74.access.telenet.be QUIT :Ping timeout: 276 seconds
< 1532038642 960773 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :hmm, that paper is not publically available
< 1532038646 301746 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :subleq: oh yes, it's obviously TC if you add integers + basic operations on them (like increment, decrement, zero-test)
< 1532038675 224335 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :i don't get it, why aren't church numerals equivalent to primitive integers?
< 1532038691 841480 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :subleq: the types get increasingly complex as the numbers get larger
< 1532038707 116416 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :so they work fine in untyped lambda calculus, but in typed lambda calculus, any given type has a maximum Church number it can handle
< 1532038715 663791 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :oh
< 1532038731 816029 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that is, unless you constrain the church numerals to acting on functions of a particular simplified type, but then you can't combine them with each other
< 1532038887 162223 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hmm, I wonder if this invalidates the TCness proof for (=); Haskell
< 1532038897 29383 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :or if those characters are enough for TCness some other way
< 1532038986 38635 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let (===)==(====)=(===) in 0==3
< 1532038988 78749 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 0
< 1532039056 673015 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :so stlc with fix is not turing complete, but seemingly system f with fix is
< 1532039142 408930 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yeah, System F has proper Church numerals. (of type forall a. (a -> a) -> a -> a)
< 1532039195 867433 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right, I was just coming to that conclusion myself, Haskell isn't actually simply typed so it may work by using polymorphism
< 1532039235 867054 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two : (x -> x) -> (x -> x) = \ a b -> a (a b) in two (+1) 0
< 1532039236 770806 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yeah but it's not System F, just Hindley-Milner... so (as far as I'm concerned) it needs some thought.
< 1532039237 721566 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : <hint>:1:20: error: parse error on input ‘->’
< 1532039248 113703 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two : (x -> x) -> (x -> x) = \ a b => a (a b) in two (+1) 0
< 1532039249 884307 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : <hint>:1:20: error: parse error on input ‘->’
< 1532039260 238893 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two : ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
< 1532039262 122031 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039262 122080 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     Pattern syntax in expression context: x -> x
< 1532039264 889869 :int-e!~noone@int-e.eu PRIVMSG #esoteric :it's ::
< 1532039268 841269 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two :: ((x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
< 1532039270 577018 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039270 672868 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • You cannot bind scoped type variable ‘x’
< 1532039270 689326 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :         in a pattern binding signature
< 1532039280 628963 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I don't actually know Haskell syntax
< 1532039288 948456 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :also I thought :: was lists
< 1532039293 500907 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :let a = 4::[] in a
< 1532039296 882510 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let a = 4::[] in a
< 1532039298 798556 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039298 814953 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • Expecting one more argument to ‘[]’
< 1532039298 815025 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :       Expected a type, but ‘[]’ has kind ‘* -> *’
< 1532039305 107254 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :apparently not
< 1532039315 906462 :int-e!~noone@int-e.eu PRIVMSG #esoteric ::t join(.)
< 1532039316 381369 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two :: (forall x. (x -> x) -> (x -> x)) = \ a b -> a (a b) in two (+1) 0
< 1532039317 220160 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :(a -> a) -> a -> a
< 1532039318 150938 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039318 241657 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • Couldn't match expected type ‘forall x1. (x1 -> x1) -> x1 -> x1’
< 1532039318 241716 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :                   with actual type ‘(t0 -> t0) -> t0 -> t0’
< 1532039331 96682 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> join(.)(join(.))succ 0
< 1532039333 279506 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 4
< 1532039365 191293 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two a b :: ((x -> x) -> (x -> x)) = a (a b) in two (+1) 0
< 1532039366 943632 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : <hint>:1:5: error: Parse error in pattern: two
< 1532039381 560158 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let (two :: ((x -> x) -> (x -> x))) a b = a (a b) in two (+1) 0
< 1532039383 336578 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : <hint>:1:5: error:
< 1532039383 431783 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     Parse error in pattern: (two :: ((x -> x) -> (x -> x)))
< 1532039402 747148 :int-e!~noone@int-e.eu PRIVMSG #esoteric :hmm
< 1532039409 71340 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two a b = a (a b) in two (+1) 0
< 1532039411 43572 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 2
< 1532039418 41378 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it works just fine without the type annotation :-P
< 1532039441 491934 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let two :: (x -> x) -> x -> x; two = \f x. f (f x) in two two succ 0
< 1532039443 494604 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : <hint>:1:42: error: parse error on input ‘.’
< 1532039449 227289 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two succ 0
< 1532039451 298282 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 4
< 1532039456 737320 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in two two two succ 0
< 1532039458 809529 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 16
< 1532039484 51552 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :you don't need the annotation
< 1532039495 886956 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let two = (\f x -> f (f x)) :: (x -> x) -> x -> x in two two two succ 0
< 1532039498 28838 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 16
< 1532039503 490783 :int-e!~noone@int-e.eu PRIVMSG #esoteric :subleq: I know.
< 1532039521 938503 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I wonder whether there was a reason for disabling the pattern type signatures though... I forgot.
< 1532039546 973545 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in let three :: (x -> x) -> x -> x; three = \f x -> f (f (f x)) in let eight :: (x -> x) -> x -> x; eight = two three in eight (+1) 0
< 1532039548 726137 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 9
< 1532039555 254445 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :bleh, got the arguments backwards
< 1532039557 256613 :int-e!~noone@int-e.eu PRIVMSG #esoteric ::)
< 1532039561 200052 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :> let two :: (x -> x) -> x -> x; two = \f x -> f (f x) in let three :: (x -> x) -> x -> x; three = \f x -> f (f (f x)) in let eight :: (x -> x) -> x -> x; eight = three two in eight (+1) 0
< 1532039563 56808 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 8
< 1532039578 615080 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :that's what I was checking for, if we could do arithmetic and yet still have the same types
< 1532039581 134684 :int-e!~noone@int-e.eu PRIVMSG #esoteric :8 == 9 for large values of 8
< 1532039581 702234 :spieglau!~spieglau@82.144.205.57 JOIN :#esoteric
< 1532039595 306947 :int-e!~noone@int-e.eu PRIVMSG #esoteric :ais523: you can but only on constants, I think
< 1532039610 822521 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let f two = two two in f (\f x -> f (f x)) succ 0
< 1532039612 932091 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039613 28373 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • Occurs check: cannot construct the infinite type: t ~ t -> t1
< 1532039613 44783 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • In the first argument of ‘two’, namely ‘two’
< 1532039614 405852 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :I should have gone with 16, 2⁴ = 4² so it wouldn't matter if I had it backwards
< 1532039651 371355 :ais523!~ais523@unaffiliated/ais523 QUIT :Remote host closed the connection
< 1532039664 672547 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric
< 1532039669 119823 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let f :: (forall x. (x -> x) -> x -> x) -> (x -> x) -> x -> x; f two = two two in f (\f x -> f (f x)) succ 0
< 1532039671 215545 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : 4
< 1532039694 962761 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :right, seems like you need the explicit type annotation
< 1532039705 682492 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :which means that the subset of Haskell that uses only ( = ) ; probably isn't TC after all
< 1532039737 475276 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :it's probably TC if you add :
< 1532039738 573236 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(it works with this higher order type, but that can't be written in the (=); fragment, and it's not Haskell 2010
< 1532039782 757220 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :something I learned while doing literature review for my PhD thesis is that it's been proven that type inference for system F is impossible in general
< 1532039792 230855 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :which is why languages in practice need the annotations
< 1532039822 37853 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :what can system f do that hindley milner can't?
< 1532039846 408995 :int-e!~noone@int-e.eu PRIVMSG #esoteric :subleq: it has polymorphic arguments
< 1532039865 965218 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :subleq: use the same argument twice (or more) with a different type for each use
< 1532039877 16873 :subleq!~gavin@207.173.246.52 PRIVMSG #esoteric :oh, like rank-n types
< 1532039883 246313 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :hindley-milner lets you use the same argument multiple times in a lambda but it has to have the same type with each use
< 1532039914 288989 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let f :: (forall x. x -> x) -> ((), Bool); f g = (g (), g True) in f id
< 1532039916 497934 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : ((),True)
< 1532039931 547397 :int-e!~noone@int-e.eu PRIVMSG #esoteric :> let f g = (g (), g True) in f id
< 1532039933 570593 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : error:
< 1532039933 570645 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • Couldn't match expected type ‘()’ with actual type ‘Bool’
< 1532039933 570657 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :     • In the first argument of ‘g’, namely ‘True’
< 1532039942 304683 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :this basic idea (with respect to lambda calculi in general, not hindley-milner in particular) is key to the main result of my thesis, which invalidated several years' worth of work in a number of different research projects (including my own)
< 1532039948 786230 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :by showing that what they were aiming for was impossible :_D
< 1532039951 719029 :ais523!~ais523@unaffiliated/ais523 PRIVMSG #esoteric :* :-D
< 1532039963 352847 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(that's one of the simplest examples of the difference)
< 1532040403 577147 :ais523!~ais523@unaffiliated/ais523 QUIT :Quit: quit
< 1532040664 298391 :zzo38!~zzo38@24-207-47-161.eastlink.ca JOIN :#esoteric
< 1532041675 630466 :zzo38!~zzo38@24-207-47-161.eastlink.ca PRIVMSG #esoteric :I have received the new issue of 2600 today.
< 1532042158 829863 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :vote:
< 1532042168 816930 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :1. going to bed and gettting some healthy sleep
< 1532042179 748420 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :2. ordering a pizza and staying up late
< 1532042200 960950 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :also i'm on a no carb diet so the pizza is like super taboo
< 1532044782 939399 :lifthrasiir!~lifthrasi@ec2-52-79-98-81.ap-northeast-2.compute.amazonaws.com QUIT :Quit: No Ping reply in 180 seconds.