< 1591057192 123719 :tromp_!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591057455 39478 :tromp_!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Ping timeout: 246 seconds < 1591059556 400266 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591059845 398993 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Ping timeout: 272 seconds < 1591064140 145639 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1591068908 474073 :adu!~arobbins@c-73-129-154-238.hsd1.md.comcast.net JOIN :#esoteric < 1591070248 204019 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 265 seconds < 1591072763 23336 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1591073251 361928 :ArthurSt1ong!~ArthurStr@128-124-28-90.mobile.vf-ua.net QUIT :Quit: leaving < 1591073270 23715 :ArthurStrong!~ArthurStr@128-124-28-90.mobile.vf-ua.net JOIN :#esoteric < 1591073769 644301 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :"One way to think about dependent types is to think of them as “first class” objects in the language, in that they can be assigned to variables, passed around and returned from functions, just like any other construct. But, if they’re truly first class, we should be able to pattern match on them too! Idris 2 allows us to do this. For example" < 1591073784 958591 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :I thought pattern matching on types was antithetical to the concept of Idris? > 1591074760 7734 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Jcs 5* 10New user account < 1591075023 518994 :zzo38!~zzo38@host-24-207-48-139.public.eastlink.ca PRIVMSG #esoteric :Maybe it is antithetical to Idris but not Idris 2. But, I don't know enough of Idris to really know that, anyways > 1591075156 339239 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=73168&oldid=73137 5* 03Jcs 5* (+151) 10 > 1591075267 466811 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=73169&oldid=73168 5* 03Jcs 5* (-151) 10 > 1591076573 843817 PRIVMSG #esoteric :14[[07User talk:Emerald14]]4 N10 02https://esolangs.org/w/index.php?oldid=73170 5* 03JonoCode9374 5* (+525) 10Created page with "==Tips For Making a Golfing Language== A while ago, there was a thread over on the Code Golf StackExchange (CGCC) about things to consider when making a golfing language: htt..." > 1591078948 791872 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03NikolayResh 5* 10New user account < 1591079029 451764 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591079339 470968 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Ping timeout: 272 seconds < 1591079474 387396 :adu!~arobbins@c-73-129-154-238.hsd1.md.comcast.net QUIT :Quit: adu < 1591079783 161534 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric > 1591080444 757037 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=73171&oldid=73169 5* 03NikolayResh 5* (+231) 10/* Introductions */ > 1591080615 506933 PRIVMSG #esoteric :14[[07Brainfuck implementations14]]4 10 02https://esolangs.org/w/index.php?diff=73172&oldid=72159 5* 03NikolayResh 5* (+106) 10/* Normal implementations */ < 1591081818 937433 :j-bot!~jbot@hagall.firefly.nu QUIT :Remote host closed the connection < 1591082988 840979 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Sgeo: Do they actually lose parametricity? < 1591083000 194779 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I doubt it. I think it's something a bit more subtle than that. < 1591083120 927613 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :A function that wants to match on a type has to note that it's accepting a type in its type signature < 1591083137 897897 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html < 1591083142 379438 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :"Note that multiplicities on the binders, and the ability to pattern match on non-erased types mean that the following two types are distinct < 1591083142 486662 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :" < 1591083150 984082 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :id : a -> a < 1591083151 92107 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net PRIVMSG #esoteric :notId : {a : Type} -> a -> a < 1591083448 908555 :b_jonas!~x@catv-176-63-11-208.catv.broadband.hu PRIVMSG #esoteric :so that's like when you have an Any class in Haskell, but you can match types on it because the Any class has a method that lets you macth the types, and the class constraint is passed explicitly? < 1591084377 415625 :rain1!~debian@unaffiliated/rain1 JOIN :#esoteric < 1591085015 270408 :b_jonas!~x@catv-176-63-11-208.catv.broadband.hu QUIT :Remote host closed the connection < 1591086586 929650 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 246 seconds < 1591087352 613719 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Isn't that thing just the way they write forall? < 1591087367 712365 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Hmm... < 1591087384 680719 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That's suspicious. < 1591087774 422913 :craigo!~craigo@144.136.206.168 QUIT :Ping timeout: 240 seconds < 1591087795 812093 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1591089633 908563 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 JOIN :#esoteric < 1591091976 945423 :ArthurStrong!~ArthurStr@128-124-28-90.mobile.vf-ua.net QUIT :Ping timeout: 272 seconds < 1591093316 586309 :S_Gautam!uid286066@gateway/web/irccloud.com/x-nslypcutcevucowr JOIN :#esoteric < 1591094784 90298 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 JOIN :#esoteric < 1591094986 738538 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Remote host closed the connection < 1591095360 803805 :LKoen!~LKoen___@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1591095573 823817 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1591095632 194468 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 256 seconds < 1591095653 329688 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1591095674 795837 :cpressey!~cpressey@88.144.69.212 JOIN :#esoteric < 1591097103 723699 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1591099530 266035 :cpressey!~cpressey@88.144.69.212 QUIT :Quit: WeeChat 1.9.1 < 1591100247 220429 :int-e!~noone@int-e.eu PRIVMSG #esoteric :. o O ( I don't want dependent types. I want dependable types. ) < 1591101997 173382 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :`? seal < 1591101999 376175 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :seal? ¯\(°​_o)/¯ < 1591102494 296730 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 PRIVMSG #esoteric :"seal" is an abbreviation for "sea lion". < 1591103494 425072 :S_Gautam!uid286066@gateway/web/irccloud.com/x-nslypcutcevucowr QUIT :Quit: Connection closed for inactivity < 1591104726 970827 :cpressey!~cpressey@88.144.69.212 JOIN :#esoteric > 1591105127 219200 PRIVMSG #esoteric :14[[07Cubix14]]4 M10 02https://esolangs.org/w/index.php?diff=73173&oldid=52635 5* 03PythonshellDebugwindow 5* (+23) 10/* Links */ category languages > 1591105353 438160 PRIVMSG #esoteric :14[[07Glypho14]]4 M10 02https://esolangs.org/w/index.php?diff=73174&oldid=53687 5* 03PythonshellDebugwindow 5* (+28) 10/* External resources */ < 1591105761 789955 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 QUIT :Remote host closed the connection < 1591106595 352744 :rain1!~debian@unaffiliated/rain1 QUIT :Quit: leaving > 1591107368 544798 PRIVMSG #esoteric :14[[07Dogescript14]]4 M10 02https://esolangs.org/w/index.php?diff=73175&oldid=53778 5* 03DmilkaSTD 5* (+14) 10 < 1591109237 925146 :rain1!~debian@unaffiliated/rain1 JOIN :#esoteric > 1591109400 108080 PRIVMSG #esoteric :14[[07User talk:Truttle114]]4 10 02https://esolangs.org/w/index.php?diff=73176&oldid=68710 5* 03DmilkaSTD 5* (+110) 10 < 1591109828 55231 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591110102 109807 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Ping timeout: 246 seconds > 1591110714 422317 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 10 02https://esolangs.org/w/index.php?diff=73177&oldid=73074 5* 03DmilkaSTD 5* (-2474) 10Replaced content with "{{WIP}} ::Got an amazing idea for Brainfuck" < 1591111183 514280 :wib_jonas!25bf3cd1@gateway/web/cgi-irc/kiwiirc.com/ip.37.191.60.209 QUIT :Quit: Connection closed < 1591111426 827402 :cpressey!~cpressey@88.144.69.212 PRIVMSG #esoteric :https://mathoverflow.net/a/361870 seems fairly esoteric. < 1591111759 114936 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar QUIT :Remote host closed the connection < 1591111932 863111 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar JOIN :#esoteric < 1591113639 986016 :cpressey!~cpressey@88.144.69.212 QUIT :Quit: WeeChat 1.9.1 < 1591114702 801411 :Cale!~cale@2607:fea8:9960:35:28a4:5da9:4116:e1fa QUIT :Ping timeout: 260 seconds < 1591115440 703778 :Cale!~cale@2607:fea8:9960:35:4c85:e40f:b7ff:71a8 JOIN :#esoteric < 1591115506 927467 :b_jonas!~x@catv-176-63-11-121.catv.broadband.hu JOIN :#esoteric < 1591115559 172892 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591116570 999288 :rain1!~debian@unaffiliated/rain1 PRIVMSG #esoteric :I knew it! < 1591116573 823558 :rain1!~debian@unaffiliated/rain1 PRIVMSG #esoteric :I knew rices theorem was false < 1591116763 353013 :adu!~arobbins@c-73-129-154-238.hsd1.md.comcast.net JOIN :#esoteric > 1591117550 549507 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 M10 02https://esolangs.org/w/index.php?diff=73178&oldid=73177 5* 03PythonshellDebugwindow 5* (+24) 10 > 1591117600 161238 PRIVMSG #esoteric :14[[07Mice in a maze/mice.py14]]4 M10 02https://esolangs.org/w/index.php?diff=73179&oldid=58067 5* 03PythonshellDebugwindow 5* (+30) 10/* Comments */ > 1591117643 806898 PRIVMSG #esoteric :14[[07Streetcode14]]4 M10 02https://esolangs.org/w/index.php?diff=73180&oldid=72083 5* 03PythonshellDebugwindow 5* (+36) 10/* Turing-completeness proof */ > 1591117659 856085 PRIVMSG #esoteric :14[[07COD14]]4 M10 02https://esolangs.org/w/index.php?diff=73181&oldid=73098 5* 03PythonshellDebugwindow 5* (+36) 10/* Raise an error (takes 3 inputs first) */ < 1591117767 779494 :zseri!~zseri@ytrizja.de JOIN :#esoteric < 1591118468 11370 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 JOIN :#esoteric < 1591119024 994353 :Sgeo!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1591119890 42754 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a QUIT :Remote host closed the connection < 1591120378 780147 :tromp!~tromp@2a02:a210:ca3:2800:408c:e879:b87d:9d8a JOIN :#esoteric < 1591121462 779579 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 260 seconds < 1591122559 892439 :b_jonas!~x@catv-176-63-11-121.catv.broadband.hu PRIVMSG #esoteric :fungot, is it logically possible that there exist worlds that are carried by five or more elephants, rather than just the usual four, and how would you resolve the apparent contradiction with the Bible? < 1591122560 232075 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :b_jonas: that's what we get after doing your initial decoding step. but first i need to use another version; i'm advising you to use disorient me! < 1591122680 150543 :b_jonas!~x@catv-176-63-11-121.catv.broadband.hu PRIVMSG #esoteric :yes, I can understand if that radical hypothesis disorients you. < 1591122747 316850 :zseri!~zseri@ytrizja.de QUIT :Quit: zseri < 1591122767 577705 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1591123951 246159 :Vorpal!~Vorpal@unaffiliated/vorpal QUIT :Quit: ZNC - http://znc.sourceforge.net < 1591124287 931661 :zzo38!~zzo38@host-24-207-48-139.public.eastlink.ca PRIVMSG #esoteric :Maybe I will need to add the possibility of "sections" with their own margins, within a text area, where in some cases other stuff may be aligned and printed within the margins. < 1591124335 192117 :zzo38!~zzo38@host-24-207-48-139.public.eastlink.ca PRIVMSG #esoteric :For example, it may be applicable to Sagas and planeswalkers in Magic: the Gathering. < 1591124574 306384 :user24!~user24@2a02:810a:1440:7304:94bb:5455:3471:442a JOIN :#esoteric < 1591124770 729865 :int-e!~noone@int-e.eu PRIVMSG #esoteric :rain1: only if you're imprecise < 1591124953 224767 :int-e!~noone@int-e.eu PRIVMSG #esoteric :That link is interesting though, I had not heard of Friedberg's theorem. < 1591125828 779571 :zseri!~zseri@ytrizja.de JOIN :#esoteric < 1591125886 478788 :adu!~arobbins@c-73-129-154-238.hsd1.md.comcast.net QUIT :Quit: adu < 1591126847 923940 :craigo!~craigo@144.136.206.168 JOIN :#esoteric < 1591127880 826515 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric > 1591128787 414353 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 10 02https://esolangs.org/w/index.php?diff=73182&oldid=73178 5* 03DmilkaSTD 5* (+90) 10 < 1591130031 176336 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 QUIT :Ping timeout: 246 seconds > 1591130341 844949 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 10 02https://esolangs.org/w/index.php?diff=73183&oldid=73182 5* 03DmilkaSTD 5* (+1058) 10 > 1591130829 863075 PRIVMSG #esoteric :14[[07Special:Log/upload14]]4 upload10 02 5* 03DmilkaSTD 5* 10uploaded "[[02File:BfAsmMemoryManagementGraph.png10]]" > 1591131038 135077 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 10 02https://esolangs.org/w/index.php?diff=73185&oldid=73183 5* 03DmilkaSTD 5* (+78) 10 < 1591131580 824130 :rain1!~debian@unaffiliated/rain1 QUIT :Quit: leaving < 1591131787 22891 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 JOIN :#esoteric > 1591132351 917224 PRIVMSG #esoteric :14[[07BF-ASM:814]]4 M10 02https://esolangs.org/w/index.php?diff=73186&oldid=73185 5* 03PythonshellDebugwindow 5* (+77) 10/* Memory management */ catas < 1591132366 724828 :user24!~user24@2a02:810a:1440:7304:94bb:5455:3471:442a QUIT :Quit: Leaving > 1591132548 811514 PRIVMSG #esoteric :14[[07Plugh14]]4 M10 02https://esolangs.org/w/index.php?diff=73187&oldid=67009 5* 03PythonshellDebugwindow 5* (+100) 10 < 1591132717 50813 :aloril_!~aloril@mobile-access-b0480e-37.dhcp.inet.fi QUIT :Ping timeout: 256 seconds < 1591133713 486080 :j-bot!~jbot@hagall.firefly.nu JOIN :#esoteric < 1591134588 798900 :aloril!~aloril@mobile-access-b0480e-37.dhcp.inet.fi JOIN :#esoteric < 1591135066 295432 :ArthurStrong!~ArthurStr@46-133-14-17.mobile.vf-ua.net JOIN :#esoteric < 1591136787 558194 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 240 seconds < 1591136807 144580 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1591137028 610863 :ArthurStrong!~ArthurStr@46-133-14-17.mobile.vf-ua.net QUIT :Quit: leaving < 1591137084 189574 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 256 seconds < 1591138401 330041 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1591138878 132781 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1591138934 762626 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 260 seconds < 1591138957 949324 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1591139157 254302 :moony!moony@hellomouse/dev/moony NICK :thoony < 1591139232 97648 :TheLie!~TheLie@2a02:8106:215:3300:844d:dece:9bd4:fbb2 QUIT :Remote host closed the connection < 1591139270 929639 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Ping timeout: 260 seconds < 1591139393 220121 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 252 seconds < 1591141358 498435 :thoony!moony@hellomouse/dev/moony QUIT :Quit: Bye! < 1591141468 615029 :moony!moony@hellomouse/dev/moony JOIN :#esoteric