< 1524703794 730346 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1524704103 249156 :augur!~augur@199-241-201-187.PUBLIC.monkeybrains.net JOIN :#esoteric < 1524704379 250333 :augur!~augur@199-241-201-187.PUBLIC.monkeybrains.net QUIT :Ping timeout: 260 seconds < 1524705136 523447 :variable!~variable@freebsd/developer/variable QUIT :Quit: /dev/null is full < 1524705151 251035 :augur!~augur@199-241-201-187.PUBLIC.monkeybrains.net JOIN :#esoteric < 1524705944 631812 :probablymoony!moony@unaffiliated/moonythedwarf NICK :moony < 1524705987 92591 :moony!moony@unaffiliated/moonythedwarf NICK :Ajit-pai < 1524706108 291599 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :game 7, 4-3 leafs, 2nd period ends < 1524706171 551380 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i don't keep up with baseball hth < 1524706572 958510 :Ajit-pai!moony@unaffiliated/moonythedwarf NICK :moony < 1524707257 970202 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :shit boston evened it up < 1524708704 725542 :int-e_!~noone@int-e.eu JOIN :#esoteric < 1524708772 375731 :int-e!~noone@int-e.eu QUIT :Ping timeout: 256 seconds < 1524708992 371066 :copumpkin!copumpkinm@haskell/developer/copumpkin QUIT :Ping timeout: 260 seconds < 1524709010 48190 :optimus[m]!optimusmat@gateway/shell/matrix.org/x-efpwghlsypjjefgq QUIT :Ping timeout: 256 seconds < 1524709699 290030 :augur!~augur@199-241-201-187.PUBLIC.monkeybrains.net QUIT :Ping timeout: 260 seconds < 1524712472 669738 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524712524 275781 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524712568 178054 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524712601 157136 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524712685 420659 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524712724 271705 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524712807 825430 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524712866 227840 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524712960 8709 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524712993 116099 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524713070 724570 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524713120 23738 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524713199 506213 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524713308 367717 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524713441 438611 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524714669 309604 :imode!~imode@unaffiliated/imode QUIT :Ping timeout: 260 seconds < 1524714739 259598 :brandonson!~brandon@208.91.114.1 QUIT :Ping timeout: 260 seconds < 1524714844 825630 :brandonson!~brandon@208.91.114.1 JOIN :#esoteric < 1524715457 362087 :propumpkin!~copumpkin@haskell/developer/copumpkin QUIT :Ping timeout: 248 seconds < 1524717701 318305 :arseniiv!~arseniiv@46.191.172.79 QUIT :Ping timeout: 256 seconds < 1524719559 264141 :moei!~moei@softbank221078042071.bbtec.net QUIT :Ping timeout: 255 seconds < 1524719609 196417 :moei!~moei@softbank221078042071.bbtec.net JOIN :#esoteric < 1524719771 273234 :imode!~imode@unaffiliated/imode JOIN :#esoteric < 1524721287 717068 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net QUIT :Ping timeout: 240 seconds < 1524721901 990971 :xkapastel!uid17782@gateway/web/irccloud.com/x-wosriqkrmyqpdqch QUIT :Quit: Connection closed for inactivity < 1524722192 786509 :brandonson!~brandon@208.91.114.1 QUIT :Ping timeout: 255 seconds < 1524722290 123760 :brandonson!~brandon@208.91.114.1 JOIN :#esoteric < 1524723897 580155 :moei!~moei@softbank221078042071.bbtec.net QUIT :Quit: Leaving... < 1524725785 335195 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 265 seconds < 1524726212 170037 :imode!~imode@unaffiliated/imode QUIT :Ping timeout: 260 seconds < 1524728283 186952 :moei!~moei@softbank221078042071.bbtec.net JOIN :#esoteric > 1524728586 405893 PRIVMSG #esoteric :14[[07Special:Log/newusers14]]4 create10 02 5* 03Viercc 5* 10New user account < 1524728847 130382 :brandonson!~brandon@208.91.114.1 QUIT :Ping timeout: 255 seconds < 1524728942 239689 :brandonson!~brandon@208.91.114.1 JOIN :#esoteric > 1524729003 336532 PRIVMSG #esoteric :14[[07Esolang:Introduce yourself14]]4 M10 02https://esolangs.org/w/index.php?diff=54920&oldid=54914 5* 03Viercc 5* (+176) 10 < 1524729481 36462 :AnotherTest!~turingcom@d51a46c74.access.telenet.be JOIN :#esoteric < 1524731177 27707 :AnotherTest!~turingcom@d51a46c74.access.telenet.be QUIT :Ping timeout: 276 seconds < 1524731253 826261 :int-e_!~noone@int-e.eu PRIVMSG #esoteric :@metar lowi < 1524731254 460230 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :LOWI 260820Z 06005KT 030V110 9999 FEW012 SCT035 BKN060 13/10 Q1017 NOSIG < 1524731551 486240 :oerjan!oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1524732271 246100 :AnotherTest!~turingcom@natx-145.kulnet.kuleuven.be JOIN :#esoteric < 1524732447 152801 :copumpkin!copumpkinm@haskell/developer/copumpkin JOIN :#esoteric < 1524733304 98483 :optimus[m]!optimusmat@gateway/shell/matrix.org/x-kkqoiorlfcprobpb JOIN :#esoteric < 1524734743 852037 :xkapastel!uid17782@gateway/web/irccloud.com/x-xmtevpbziggljkbv JOIN :#esoteric < 1524735591 581839 :optimus[m]!optimusmat@gateway/shell/matrix.org/x-kkqoiorlfcprobpb QUIT :Ping timeout: 240 seconds < 1524735592 873841 :copumpkin!copumpkinm@haskell/developer/copumpkin QUIT :Ping timeout: 260 seconds < 1524735680 418762 :oerjan!oerjan@hagbart.nvg.ntnu.no QUIT :Quit: Later < 1524735846 271918 :variable!~variable@freebsd/developer/variable QUIT :Quit: /dev/null is full < 1524737866 155176 :copumpkin!copumpkinm@haskell/developer/copumpkin JOIN :#esoteric < 1524738691 558817 :optimus[m]!optimusmat@gateway/shell/matrix.org/x-chuifsfdmrzbdxhc JOIN :#esoteric < 1524739134 266193 :AnotherTest!~turingcom@natx-145.kulnet.kuleuven.be QUIT :Ping timeout: 260 seconds < 1524740395 251366 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Is there any (non-esoteric?) language with a type representing an index into a specific array < 1524740653 905100 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Agda? < 1524740717 660766 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :c? < 1524740718 635520 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I guess that's not exactly true. < 1524740741 848653 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :oh, into a specific array? < 1524740753 273942 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I'd ideally like this to be strongly typed and also allow the array to mutate < 1524740755 608381 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :so if you can use foo[i] you can't use bar[i]? < 1524740762 707590 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :izabera: yeah < 1524740766 718955 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :whyyyyyyyyyyyyyyyyyyyyyyyy < 1524740768 384017 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :An array of length n has n+1 indices. < 1524740789 73412 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :izabera: mostly because I ran into a bug in my code due to me mixing up arrays < 1524740799 428736 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb: There are C++ iterators which are also not really this. < 1524740810 72077 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :maybe you should learn how computers work < 1524740817 160383 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :izabera: that requires effort < 1524740818 185276 :izabera!~izabera@unaffiliated/izabera PRIVMSG #esoteric :functional programming is bad for you < 1524740830 381746 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I'm gonna learn how maths works instead < 1524740849 220590 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :which math are you starting with < 1524740866 467797 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :shachaf: haven't decided yet < 1524740878 352268 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Maybe group theory? Group theory is fun < 1524740886 998310 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Anyway I'm pretty sure I've seen this somewhere. < 1524740890 290784 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Although not really foundational < 1524741090 908424 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Speaking of array index types, do you like wavelet trees? < 1524741116 426272 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Did you know rank maps from the type of indices of an array to the type of indices of a subarray? < 1524741120 362391 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I remember looking at them, but I don't know what they are! < 1524741147 159965 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I made a picture at http://slbkbs.org/ranksel.svg < 1524741229 776572 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb: I think Ada might have something similar to what you're asking for but I can't really tell. < 1524741256 120963 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :subtype Index_Type is Integer range Array'Range < 1524741278 633853 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You'd have to ask Sgeo_. I bet it's not really what you're asking for though. < 1524741318 164228 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :The next question is "Would such types be remotely usable in practice" < 1524741471 472498 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :It depends on why you want indexing. < 1524741519 185553 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :In the instance that inspired this, I have an index into an array of indices into another array < 1524741614 335628 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Reasonable. < 1524741653 577562 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :And I messed up and used my index as an index straight into the second array < 1524741656 300276 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think in most languages that support something like this it would be more trouble than it's worth. < 1524741688 218832 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But maybe you could approximate it with less work. < 1524741748 986885 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :For example you could have two types of arrays and indices and not do the dependenty thing where your index only works for a particular array but restrict it to a type instead. < 1524741806 355442 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :An array is just a kind of function, after all. < 1524741952 492444 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524742068 798071 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524742155 295427 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524742203 34322 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524742249 409681 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@src Real < 1524742249 443070 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :class (Num a, Ord a) => Real a where < 1524742249 476683 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric : toRational :: a -> Rational < 1524742264 752666 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb: can you learn so many maths that that class makes any sense hth < 1524742312 467239 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :shachaf: well, the real numbers and the rational numbers are basically the same, except there's more real numbers < 1524742330 535180 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Every real number is pretty close to a rational number < 1524742345 65102 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I'm going to stop here because I really don't feel like justifying that typeclass's name < 1524742366 26842 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Do you think of continuity "backwards" or "forwards"? < 1524742399 134663 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I try not to think of continuity, personally < 1524742411 407344 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :imo you're missing out < 1524742434 429583 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :But if I did I'd probably think of it in some weird way that's not quite either of those options < 1524742456 204296 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Oh, I want to hear your weird way. < 1524742504 46175 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What about naturality? < 1524742524 130985 :xkapastel!uid17782@gateway/web/irccloud.com/x-xmtevpbziggljkbv QUIT :Quit: Connection closed for inactivity < 1524742564 167199 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I don't find naturality natural < 1524742606 226016 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Do you mean continuity as in continuous functions, and naturality as in natural transformations? < 1524742610 950147 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Yes and yes. < 1524742644 431868 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :The former, I think of in terms of neighbourhoods < 1524742667 998966 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :The latter, I can never get into my head for some reason < 1524742681 26259 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :A natural transformation e : F -> G : C -> D is a functor e : 2xC -> D which is F at 0 and G at 1 < 1524742735 562249 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What could be more natural? < 1524742768 146149 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :What does this have to do with natural numbers? < 1524742777 748192 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :And natural logarithms < 1524742778 753481 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :? < 1524742780 354984 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :2 is a natural number, and so are 0 and 1. < 1524742868 206391 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You can read https://pdfs.semanticscholar.org/3833/f692e93a795b51bd3d7acfd9477f9ee6d536.pdf which I think is the thing that introduced natural transformations? < 1524743032 839338 :xkapastel!uid17782@gateway/web/irccloud.com/x-uenieejjmrsmnegh JOIN :#esoteric < 1524744722 445375 :int-e_!~noone@int-e.eu NICK :int-e < 1524745305 298663 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric < 1524745972 407381 :AnotherTest!~turingcom@d51A46C74.access.telenet.be JOIN :#esoteric < 1524747487 97524 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :shachaf: thanks for the link, I've bookmarked < 1524749917 493183 :hufferinho!~hufferinh@89.136.166.37 JOIN :#esoteric < 1524750179 425918 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524750324 232045 :xkapastel!uid17782@gateway/web/irccloud.com/x-uenieejjmrsmnegh QUIT :Quit: Connection closed for inactivity < 1524750441 308869 :variable!~variable@freebsd/developer/variable QUIT :Ping timeout: 240 seconds < 1524751063 637837 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Remote host closed the connection < 1524753274 73836 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524753596 366976 :variable!~variable@freebsd/developer/variable QUIT :Ping timeout: 265 seconds < 1524753646 48620 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524753733 357479 :ProofTechnique[m!prooftechn@gateway/shell/matrix.org/x-evjwjrllnfxngvwo JOIN :#esoteric < 1524753845 309142 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker JOIN :#esoteric < 1524753947 702562 :variable!~variable@freebsd/developer/variable QUIT :Ping timeout: 276 seconds < 1524754133 618654 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524754250 223825 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524754399 307355 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524754655 587273 :variable!~variable@freebsd/developer/variable QUIT :Client Quit < 1524754804 538459 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524755029 194716 :rodgort!~rodgort@68.ip-149-56-14.net QUIT :Quit: Leaving < 1524755616 601768 :hufferinho!~hufferinh@89.136.166.37 PART :#esoteric < 1524755783 321779 :rodgort!~rodgort@68.ip-149-56-14.net JOIN :#esoteric < 1524755960 204819 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net JOIN :#esoteric < 1524756776 521816 :xkapastel!uid17782@gateway/web/irccloud.com/x-tohwtbtljmogcnfh JOIN :#esoteric < 1524757211 300294 :arseniiv!~arseniiv@46.191.172.79 JOIN :#esoteric < 1524759018 365199 :sleffy!~sleffy@24.7.67.0 JOIN :#esoteric < 1524759277 753555 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net QUIT :Remote host closed the connection < 1524760120 375748 :variable!~variable@freebsd/developer/variable QUIT :Quit: /dev/null is full < 1524760773 693881 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net JOIN :#esoteric < 1524762473 550742 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :about a type of indexes to a particular array: maybe this is possible in Haskell. There’s a type of references to a particular _state thread_, STRef s a, where a is the type of referenced values and s is a magic which is works mostly because of the type of `runST`. Maybe one could define something like this for arrays. I think, you’d need to wrap arrays into some new type which would work with its indices like ST s and STRef s work < 1524762525 908503 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :could it be that Oleg or, say, Edward Kmett have written about something like this? IDK < 1524762568 330971 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :Taneb: ^ < 1524762924 703884 :imode!~imode@unaffiliated/imode JOIN :#esoteric < 1524763119 498584 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :however, I couldn’t yet imagine what type hackery is needed to represent a type of an array containing such indexes to other arrays. Existential somewhere, maybe. It seems dependent-like features of Haskell types are limited in this case (or not, I’m too far from an expert here) < 1524763626 543762 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :also, could these indices be pairs of an array (pointer to info about array etc.) and an index? Then it’s pretty hard to mismatch something, and the space is 8 bytes more per element, which is quite light in some cases(?) < 1524763697 173583 :brandonson!~brandon@208.91.114.1 QUIT :Ping timeout: 260 seconds < 1524763737 394894 :sleffy!~sleffy@24.7.67.0 QUIT :Ping timeout: 256 seconds < 1524763748 913489 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :8 bytes at most* (I presume 128-bit addresses aren’t yet a thing) < 1524763775 340417 :brandonson!~brandon@208.91.114.1 JOIN :#esoteric < 1524763900 195947 :int-e!~noone@int-e.eu PRIVMSG #esoteric :IPv6 *whistles* < 1524763943 79964 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :int-e: are they used as pointers in some language? :o < 1524763955 396452 :int-e!~noone@int-e.eu PRIVMSG #esoteric :*whistles some more* < 1524763971 753574 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric ::: < 1524764051 531631 :int-e!~noone@int-e.eu PRIVMSG #esoteric :it may be worth noting that the 's' in 'ST s' is a phantom type... there's no corresponding value at runtime at all. < 1524764063 700416 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :https://twitter.com/Hillelogram/status/987432178840756225 money + mouth. < 1524764108 764969 :contrapumpkin!~copumpkin@haskell/developer/copumpkin JOIN :#esoteric < 1524764390 82249 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net QUIT :Remote host closed the connection < 1524764449 303711 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :imode: interesting < 1524764506 888107 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :the article that's the result of this thread was on HN's front page recently. < 1524764579 710427 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :I think imperative code can be easy to analyze as long as you have limits to what a given subroutine is allowed to mutate < 1524764599 79343 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :hence why all of his examples are well-contained. < 1524764642 81947 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :https://hillelwayne.com/post/theorem-prover-showdown/ the article in question. < 1524764861 835254 :int-e!~noone@int-e.eu PRIVMSG #esoteric :nice troll < 1524764892 372735 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net JOIN :#esoteric < 1524765087 957434 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 JOIN :#esoteric < 1524765178 497386 :PinealGlandOptic!~PinealGla@82.144.205.57 JOIN :#esoteric < 1524765252 671341 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :his analysis of the crowds involved was pretty spot on in my travels. < 1524765329 353488 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(to my mind the main thrust behind "reasoning about (pure!) function programs is easy" is that the absence of mutation ensures separation between different parts of the program... so you can reason about a program in a modular way "for free", rather than bringing out guns like separation logic. < 1524765334 384057 :int-e!~noone@int-e.eu PRIVMSG #esoteric :) < 1524765373 481404 :oerjan!oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1524765379 303497 :idris-bot!~idris-bot@dslb-002-203-000-049.002.203.pools.vodafone-ip.de JOIN :#esoteric < 1524765382 757875 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :a good benchmark of your views would be to produce a valid proof of his examples in your theorem prover of choice. < 1524765390 686085 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :else you become a "bulldog", as he puts it. :P < 1524765401 507509 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I'm putting "for free" in quotes because there is often a performance price that you pay for purity) < 1524765413 852325 :int-e!~noone@int-e.eu PRIVMSG #esoteric :imode: Isabelle has already been done :P < 1524765436 125602 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :so has leftpad in several languages. we could always use a few more! :P < 1524765468 442885 :int-e!~noone@int-e.eu PRIVMSG #esoteric :yeah but they wouldn't fall under "my theorem prover of choice". < 1524765516 888273 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :nothing stops you from putting your beliefs to work is all I'm saying. < 1524765795 278118 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :Yes, I'd like some magic array index thing too. Not one where the index is tied to a single array, but nor one where you just define different types of indexes for different arrays, but ones where the index type can be conceptually different each time in a loop and lets you prove that the index is in bounds for that array. And yes, I think the ST-l < 1524765795 454901 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :ike foreach type trick might be able to do that. < 1524765804 14745 :SopaXorzTaker!~SopaXorzT@unaffiliated/sopaxorztaker QUIT :Remote host closed the connection < 1524766022 389704 :int-e!~noone@int-e.eu PRIVMSG #esoteric :imode: http://downthetypehole.de/paste/Bh5NU2Xi ... this is one of these stupid cases where the specification is harder to understand than the implementation :P < 1524766119 468315 :int-e!~noone@int-e.eu PRIVMSG #esoteric :oh. < 1524766160 182740 :int-e!~noone@int-e.eu PRIVMSG #esoteric :To demonstrate the point, I forgot this bit: ∧ length (left_pad c n xs) = n < 1524766447 370552 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :hmm... how about an assembler with invariant checking etc < 1524766514 254349 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :like, you have guarantees about how the instructions behave and it tries to prove things from that apward < 1524766558 769655 :sleffy!~sleffy@c-24-7-67-0.hsd1.ca.comcast.net JOIN :#esoteric < 1524766576 874046 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :that should pretty much prevent any runtime overhead? < 1524766682 509480 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :(on the other hand, the instructions would have to be rather different from a normal CPU) < 1524766701 201269 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :you could have guarantees for spans of instructions built into the hardware. < 1524766720 23737 :imode!~imode@unaffiliated/imode PRIVMSG #esoteric :basically hardware assertions. < 1524766756 321604 :augur!~augur@104-244-24-85.PUBLIC.monkeybrains.net JOIN :#esoteric < 1524766989 454927 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net QUIT :Remote host closed the connection < 1524767008 164905 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :imode: hmmmm... but if you have hardware assertions you can USE those in your instruction pipelining < 1524767023 371074 :\oren\_!~oren@ec2-52-2-213-98.compute-1.amazonaws.com PRIVMSG #esoteric :so it might not even have an overhead < 1524767502 163968 :rdococ!rdococ@unaffiliated/rdococ PRIVMSG #esoteric :Syntactic iodine: Something that you don't know is there, and something that you don't know you need, like iodine is in iodised table salt. < 1524767538 529866 :rdococ!rdococ@unaffiliated/rdococ PRIVMSG #esoteric :(Granted, what's in iodised table salt is actually various iodide salts as opposed to elemental iodine, but you get the gist.) < 1524767664 140961 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :rdococ: sounds tricky to need it if you don't know it's there... < 1524767708 294272 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :maybe a language using ZWSPes to separate tokens < 1524767731 277807 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :but only when they're not both alphanumeric < 1524768581 396214 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1524768996 815240 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 QUIT :Quit: http://www.kiwiirc.com/ - A hand crafted IRC client < 1524771011 52620 :augur!~augur@104-244-24-85.PUBLIC.monkeybrains.net PART #esoteric :"Leaving..." < 1524771869 972864 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`? e < 1524771871 321452 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :e is a freenode admin. e is not known to be an Agora player. < 1524771883 75301 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :hm. < 1524771912 435203 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :That reminds me of why someone way back when thought I was good at palindromes < 1524772078 29703 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :arseniiv: your array idea would probably work as a use of kmett's reflection library < 1524772121 135020 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :Taneb: why? < 1524772132 384489 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :oerjan, I wrote, in here, "E, esoteric, ire to see" < 1524772148 699654 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :It was oklopol who commented that < 1524772155 987590 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Whatever happened to them? < 1524772189 298934 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 JOIN :#esoteric < 1524772196 788834 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`quote oklopol.*never come < 1524772197 684436 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :656) i think i'll just take the usual route and go do post doc research somewhere far away and never come back and become a drug lord and kill myself < 1524772205 84213 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :presumably that. < 1524772214 933133 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :(he did go to Brazil.) < 1524772220 678512 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Ahah! < 1524772221 201622 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :rdococ: re syntactic iodine => rust has a lot of those, and sometimes it horrifies me how complex some of the syntax and name lookup rules are < 1524772226 549186 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :time to stalk him a moment -> < 1524772233 419812 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Hmm, I know an academic from Brazil! < 1524772262 135509 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :the part that bothers me the most is how constructors and fresh variable names are (not) distinguished in patterns < 1524772283 553151 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :and I find the name lookup rules rather complicated, but at least those are less worrisome < 1524772295 852019 :rdococ!rdococ@unaffiliated/rdococ PRIVMSG #esoteric :`help < 1524772296 197523 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Runs arbitrary code in GNU/Linux. Type "`", or "`run " for full shell commands. "`fetch [] " downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert " can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/ < 1524772327 513632 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb: Remember when you used to write limericks? < 1524772335 61198 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I try not to < 1524772403 983512 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric : There was a chap from Scandinavia/Who didn't have any poetic behaviour/So online he complained/And helpfulness reigned/Taneb became his limerick saviour < 1524772416 44060 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :What happened to olsner, anyway? < 1524772423 74958 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :the way the type inference interacts with the method lookup is also somewhat worrisome by the way < 1524772426 250958 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I can't tell people whose nick starts with o apart. < 1524772431 276046 :olsner!~salparot@c213-89-109-20.bredband.comhem.se PRIVMSG #esoteric :shachaf: nothing? < 1524772440 420837 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :if his homepage is to be believed, he's back at turku univ. < 1524772441 750623 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :in the way you can suddenly have your program break when new apparently unrelated functions are added < 1524772448 693980 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :shachaf, I never actually figured out if oklopol and oklofol were different people < 1524772455 887456 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :*oklofok < 1524772478 135582 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? palindrome < 1524772479 443859 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately. < 1524772485 324589 :olsner!~salparot@c213-89-109-20.bredband.comhem.se PRIVMSG #esoteric :I always assumed both oklokin are one and the same < 1524772509 464281 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Is () a palindrome? < 1524772520 436771 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :``` allwisdoms | grep -Ei palindrome | sport < 1524772521 734611 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :bash: allwisdoms: command not found \ 1/0: < 1524772527 303221 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :shachaf: there was a poll about that somewhere < 1524772534 836043 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :``` allquotes | grep -Ei palindrome | sport < 1524772535 993071 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :1/0: < 1524772543 233165 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :``` allquotes | grep -Ei palindrom | sport < 1524772544 466527 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :1/0: < 1524772546 150891 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :none? < 1524772546 916362 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :hmm < 1524772636 763947 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :
ACTION was speaking about oklopol btw, didn't see people starting to talk about olsner
< 1524772646 667368 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :
ACTION suspect olsner isn't at turku
< 1524772652 428723 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :olsner that endsner < 1524772669 781518 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :oerjan: why? does turku not have internet? < 1524772670 248252 :olsner!~salparot@c213-89-109-20.bredband.comhem.se PRIVMSG #esoteric :oerjan: I also strongly suspect I am not at turku < 1524772679 486694 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :oh good < 1524772688 203007 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I would like to visit Turku some day < 1524772694 213664 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :It seems to be an interesting place < 1524772702 908110 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I have been to Turku. < 1524772722 865877 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I took a boat to Stockholm. < 1524772742 709828 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover JOIN :#esoteric < 1524772747 617872 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :I've never been to any part of Finland < 1524772775 724563 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :Taneb: i would have said everyone oklo* is the same, except i saw a different one on PPCG or somewhere < 1524772811 230863 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :what about oklo?o? < 1524772828 285528 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Also what's the deal with ? being way harder to match efficiently for glob patterns than * ? < 1524772851 896356 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :In fact it's not even known how efficiently you can do it? < 1524772888 153788 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :what? < 1524772899 785768 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`olist 1118 < 1524772900 624945 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :olist 1118: shachaf oerjan Sgeo FireFly boily nortti b_jonas < 1524772908 707655 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :do you mean like with the matched document preprocessed? < 1524772913 678207 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :o! < 1524772945 326250 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean with neither preprocessed. < 1524772967 673363 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`1 grwp -Ei palindrome < 1524772969 380613 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :1/1:palindrome:A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately. < 1524772982 125059 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`1 grwp -Ei palindrom < 1524772983 569455 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :1/1:palindrome:A palindrome is a word that remains the same if you take it to the mirror dimension, and then take each individual letter back to the normal dimension separately. < 1524773009 399824 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :really? < 1524773021 200287 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? palindromedary camel < 1524773022 433565 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :palindromedary camel? ¯\(°​_o)/¯ < 1524773051 713497 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :i,i A palindromedary camel is one whose humps look the same from either side. < 1524773130 287467 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :oerjan, I'm unconvinced < 1524773163 582961 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :let's take an oklo poll < 1524773172 735283 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@poll-list < 1524773172 768848 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :["\"k\"","Pikami","abc","dictator-for-life","maximum-edit-distance","pizza","should-lambdabot-be-more-polite","test"] < 1524773215 911382 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :@poll-result pizza < 1524773215 986980 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :Poll results for pizza (Closed): pepperoni=1 < 1524773221 431522 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :wow < 1524773234 548793 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :scow pizza < 1524773252 48954 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? tanebventions < 1524773253 346868 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Tanebventions include necessity, Go, submarine jousting, Fueue, the universe, special relativity, metar, sand, dragons, persistence, the BBC, _46bit, progress, sanity, Italian, the grace period, the Oxford comma, ruin, and this sentence. See also tanebventions: maths or tanebventions: foods. He never invents anything involving sex. < 1524773255 893500 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I do like little peppers on pizza < 1524773320 774704 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`slwd tanebvention//s/ruin/the limerick, &/ < 1524773322 684196 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :tanebvention//Tanebventions include necessity, Go, submarine jousting, Fueue, the universe, special relativity, metar, sand, dragons, persistence, the BBC, _46bit, progress, sanity, Italian, the grace period, the Oxford comma, the limerick, ruin, and this sentence. See also tanebventions: maths or tanebventions: foods. He never invents anything involving sex. < 1524773436 939683 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`learn A limerick is a verse with two left metrical feet and three right metrical feet. < 1524773439 332316 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Learned 'limerick': A limerick is a verse with two left metrical feet and three right metrical feet. < 1524773514 937256 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :this olist seemed a bit short < 1524773536 834636 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :oerjan: That's only because olists come but once a year. < 1524773545 428772 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :If it updated three times a week you'd think it's fine. < 1524773596 188426 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :they come twice a year I think < 1524773628 600713 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I mean Mercury years. < 1524773883 730415 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`learn Fueue will be explained more properly once we've made another pass through all the other tanebventions. < 1524773886 247813 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Learned 'fueue': Fueue will be explained more properly once we've made another pass through all the other tanebventions. < 1524773998 740179 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? necessity < 1524773999 990159 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :If necessity did not exist, it would be necessary for Taneb to invent it. < 1524774001 194920 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? go < 1524774003 39172 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia. < 1524774007 969117 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? submarine jousting < 1524774009 379783 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Submarine jousting is unexplainable. < 1524774016 318569 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? the universe < 1524774017 537068 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :The universe was invented by Taneb as an opposing force to oerjan. Escardó proved that it was indiscreet. < 1524774028 94295 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? special relativity < 1524774029 420210 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :special relativity? ¯\(°​_o)/¯ < 1524774497 737671 :int-e!~noone@int-e.eu PRIVMSG #esoteric :imode: http://downthetypehole.de/paste/GpP7OKaR is the fulcrum thing. The unique thing is awkward to specify and less interesting. < 1524774542 218291 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I think I confuse the words "fulcrum" and "frustum". < 1524774589 668917 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hah, I may be doing the same thing. < 1524774611 630066 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Well, yours seems like neither of those? < 1524774639 745148 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I don't know what it is. < 1524774690 597863 :int-e!~noone@int-e.eu PRIVMSG #esoteric :shachaf: the terminology isn't mine, but I suppose idea is to balance the left and right parts of a list as well as possible < 1524774712 68402 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :That sounds like a fulcrm, I suppose. < 1524774735 682417 :int-e!~noone@int-e.eu PRIVMSG #esoteric :imode mentioned https://twitter.com/Hillelogram/status/987432178840756225 and https://hillelwayne.com/post/theorem-prover-showdown/ earlier. < 1524775146 568130 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :unidemode < 1524775201 914449 :int-e!~noone@int-e.eu PRIVMSG #esoteric :anyway, that was enough fun for now... < 1524775277 949307 :int-e!~noone@int-e.eu PRIVMSG #esoteric :actually... "unique" has a lousy specification. < 1524775293 688232 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :oerjan: is it that library which could be used to supply a config through constraints and which uses that Proxy stuff? < 1524775323 552202 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :arseniiv: yes < 1524775325 299617 :int-e!~noone@int-e.eu PRIVMSG #esoteric :What are "the unique elements" of [1,2,3,2,1]? I read it as [3], because 1 and 2 aren't unique in that list... < 1524775346 746888 :int-e!~noone@int-e.eu PRIVMSG #esoteric :but it intends the result to be [1,2,3] in any order < 1524775365 304317 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :arseniiv: you could make the array the config value < 1524775398 691436 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :int-e: [1,2,3] are the unique elements, and [3] are the unique -u elements < 1524775417 643542 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :also, [1,2] are the unique -d elements, and [1,2,2,1] are the unique -D elements < 1524775426 547267 :int-e!~noone@int-e.eu PRIVMSG #esoteric :TMI < 1524775447 700231 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(which really can't be a complaint on here, so carry on) < 1524775455 45480 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :How do you catch a unique element? < 1524775519 291915 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net JOIN :#esoteric < 1524775543 616922 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`? tmi < 1524775545 1791 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :tmi? ¯\(°​_o)/¯ < 1524775692 176933 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`learn TMI is short for toenail mushroom infestation < 1524775694 561127 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Learned 'tmi': TMI is short for toenail mushroom infestation < 1524775715 227934 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :eww < 1524775743 349261 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :i take it my wisdom got tmi spot on < 1524775751 521894 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :is that the one on the Harry toenail of ... what was it < 1524775753 302288 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? titles < 1524775754 703599 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Titles J. K. Rowling had specifically denied on her webpage would be the titles of the sixth or seventh Harry Potter book are: Harry Potter and the{ Green Flame Torch, Mountain of Fantasy, Fortress of Shadows, Forest of Shadows, Graveyard of Memories, Pyramids of Furmat, Pillar of Storgé, Toenail of Icklibõgg}. < 1524775777 279415 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :Harry toenail of Icklibõgg < 1524775842 599382 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :that was strangely not on my mind hth < 1524775894 211240 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :maybe it should be a different organ < 1524776016 728408 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? hth < 1524776017 968229 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :hth ([ʰtʰh̩]) is help received from a hairy toe. It is not at all hambiguitous. < 1524776044 831701 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :hm i sense a pattern < 1524776060 75225 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`` grWp -l toe < 1524776060 414744 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? toe < 1524776062 30026 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :apt \ dingas \ hth \ portmanteau \ potatoes \ rincewind \ the \ title \ tmi \ toe \ twnh \ welp \ wth < 1524776062 391463 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :The TOE is the Toe of Everything, from which our universe sprang. < 1524776062 649183 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? toenail < 1524776064 26061 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :toenail? ¯\(°​_o)/¯ < 1524776068 374215 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? portmanteau < 1524776069 676087 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :​«Portmanteau» is the French spelling of “port man toe”. < 1524776077 224378 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? wth < 1524776078 469194 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :WTH is wavy toe hair. hth. < 1524776084 71283 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? toe < 1524776085 340845 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :The TOE is the Toe of Everything, from which our universe sprang. < 1524776089 866119 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`? twnh < 1524776091 145860 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :twnh is dubious hambiguitous help that will or will not be help. It is provided by a toe with no hair. < 1524776096 570082 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`dowg toe < 1524776098 438834 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :9094:2016-09-26 learn The TOE is the Toe of Everything, from which our universe sprang. \ 6001:2015-09-16 rm wisdom/toe \ 5996:2015-09-15 learn the Toe of Harriness\'s Enclosure \ 5995:2015-09-15 learn The Toe of Harriness\'s Enclosure \ 5993:2015-09-15 learn the Toe of Harriness\'s Enclosure \ 5991:2015-09-15 learn the Toe of Harriness\'s Enclave \ 5990:2015-09-1 < 1524776102 200681 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`dowg wth < 1524776104 162323 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :8919:2016-08-15 learn WTH is wavy toe hair. hth. < 1524776110 703767 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`dowg portmanteau < 1524776112 655068 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :6161:2015-10-30 le/rn portmanteau/\xc2\xabPortmanteau\xc2\xbb is the French spelling of \xe2\x80\x9cport man toe\xe2\x80\x9d. < 1524776115 668049 :LKoen!~LKoen@vbo91-1-82-238-218-67.fbx.proxad.net QUIT :Remote host closed the connection < 1524776117 403304 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`owrjan < 1524776118 673595 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :Your omnidryad saddle principal swatty kind "Darth Ook" oerjan the shifty loud hero is a hazy expert in minor compaction. Also a Groadep who minces Roald Dahl. He could never render the word "amortized" so he put it here for connivance. His ark-nemesis is Noah. He twice punned without noticing it. < 1524776133 813246 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :`swrjan s/kind/toe-obsessed/ < 1524776135 837219 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :oerjan//Your omnidryad saddle principal swatty toe-obsessed "Darth Ook" oerjan the shifty loud hero is a hazy expert in minor compaction. Also a Groadep who minces Roald Dahl. He could never render the word "amortized" so he put it here for connivance. His ark-nemesis is Noah. He twice punned without noticing it. < 1524776150 760591 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`? swrjan < 1524776152 65108 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :swrjan? ¯\(°​_o)/¯ < 1524776177 708413 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :we need a command in bin that seds the source code of that very command < 1524776278 105059 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`mkx bin/qued//sled bin/qued//"$1" < 1524776280 134178 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :bin/qued < 1524776304 885042 :int-e!~noone@int-e.eu PRIVMSG #esoteric :meh it's hard to stop. http://downthetypehole.de/paste/qa3R2yV3 has a few comments. < 1524776344 544740 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`qued s,xxx,, < 1524776345 410325 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :bin/qued//sled bin/qued//"$1" < 1524776371 236611 :PinealGlandOptic!~PinealGla@82.144.205.57 QUIT :Quit: leaving < 1524776425 973434 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`qued s,ed bin,wd ../bin, < 1524776427 952880 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :bin/qued//slwd ../bin/qued//"$1" < 1524776447 491923 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :`qued s,xxx,y, < 1524776448 546763 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :​../bin/qued//slwd ../bin/qued//"$1" < 1524776648 678656 :LKoen!~LKoen@2a01:e35:2eed:a430:bc3f:aa7:f199:6d1c JOIN :#esoteric < 1524777366 72998 :LKoen!~LKoen@2a01:e35:2eed:a430:bc3f:aa7:f199:6d1c 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.” < 1524779015 428258 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :`qued ; < 1524779016 409167 :HackEso!~h@techne.zem.fi PRIVMSG #esoteric :​../bin/qued//slwd ../bin/qued//"$1" < 1524779057 834296 :variable!~variable@freebsd/developer/variable JOIN :#esoteric < 1524779362 299601 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :oh! < 1524779410 518159 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :I've got it < 1524779574 622658 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :arseniiv: Nora's Hair Styling on Demand, Call Us Any Time Full Movie HD < 1524780077 904705 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :in fact, remove the Us < 1524780082 763921 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :Nora's Hair Styling on Demand, Call Any Time Full Movie HD < 1524780096 554168 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :unless you already found a better name that is < 1524780117 177201 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :although someone who's actually good at English puns will probably be able to give a better suggestion < 1524780381 290933 :brandonson!~brandon@208.91.114.1 QUIT :Ping timeout: 240 seconds < 1524780493 708573 :brandonson!~brandon@208.91.114.1 JOIN :#esoteric < 1524780619 685957 :oerjan!oerjan@hagbart.nvg.ntnu.no PRIVMSG #esoteric :. o O ( i feel like i'm obliged to suggest pedicure at this point ) < 1524780683 143575 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :oerjan: that was my original suggestion yesterday: "have you named it Nora's Nailcare 2: Reverse Polish Full Movie HD yet? Or is that name inappropriate for a language that isn't stack-based?" < 1524780694 633101 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :you can still reuse that name for a different language < 1524780746 20892 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :I'm not so sure that there should be more Nora languages. < 1524780781 630601 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :The world of spam is diverse. < 1524780841 114149 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :a spam-based language has been very close to the top of the page in https://esolangs.org/wiki/List_of_ideas for a long time < 1524781012 943782 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :Spam based language? < 1524781027 465539 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :Oh < 1524781031 548700 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :hi Sgeo_ < 1524781043 645069 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :Thought you meant spam that managed to accidentally persist in the esolang wiki < 1524781047 217584 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :Hi shachaf < 1524781058 562007 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Does Ada support types of indices into a specific array? < 1524781083 759425 :Phantom_Hoover!~phantomho@unaffiliated/phantom-hoover QUIT :Remote host closed the connection < 1524781091 493452 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :If not, does Agda? < 1524781157 815024 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :As in the type of the index contains the array? For both, no idea. Although it wouldn't surprise me if Agda could, just based on it being dependently typed. < 1524781236 66745 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :But what about Ada? < 1524781250 460474 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :You can do "subtype Index_Type is INteger range Array'Range", right? < 1524781391 419080 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :I don't know Ada (or Agda except that it's dependently typed). < 1524781419 175232 :Sgeo_!~Sgeo@ool-18b98dd9.dyn.optonline.net PRIVMSG #esoteric :I could probably recognize that what you typed looks more like Ada than any other language I know < 1524781514 781682 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :shachaf: in SQL, when a column has a FOREIGN KEY constraint, would that count as the column having a type that indexes into another array? < 1524781522 813928 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 PRIVMSG #esoteric :or at least similar enough? < 1524782029 346756 :AnotherTest!~turingcom@d51A46C74.access.telenet.be QUIT :Ping timeout: 256 seconds < 1524782465 861399 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Maybe. < 1524782475 191330 :shachaf!~shachaf@unaffiliated/shachaf PRIVMSG #esoteric :Taneb brought this up, not me. < 1524782764 753149 :oerjan!oerjan@hagbart.nvg.ntnu.no QUIT :Quit: Nite < 1524784241 692042 :wob_jonas!b03f1891@gateway/web/cgi-irc/kiwiirc.com/ip.176.63.24.145 QUIT :Quit: http://www.kiwiirc.com/ - A hand crafted IRC client < 1524786370 585327 :arseniiv!~arseniiv@46.191.172.79 PRIVMSG #esoteric :wob_jonas> Nora's Hair Styling on Demand, Call Any Time Full Movie HD> oh nooooooooooo why should it be Nora all the time I don’t get it :P < 1524787161 303487 :arseniiv!~arseniiv@46.191.172.79 QUIT :Ping timeout: 240 seconds