< 1698368102 649266 :myname!~myname@ks300980.kimsufi.com QUIT :Ping timeout: 258 seconds < 1698368198 233393 :myname!~myname@ks300980.kimsufi.com JOIN #esolangs * :myname < 1698368534 418662 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord < 1698368580 985004 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 255 seconds < 1698368615 324649 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life > 1698374721 890828 PRIVMSG #esolangs :14[[07Sharp14]]4 M10 02https://esolangs.org/w/index.php?diff=118424&oldid=103545 5* 03PythonshellDebugwindow 5* (+17) 10/* Concepts */ Nowiki < 1698375994 953131 :ais523!~ais523@user/ais523 QUIT :Quit: quit < 1698382821 583949 :wpa!uid568065@id-568065.helmsley.irccloud.com QUIT :Quit: Connection closed for inactivity < 1698382981 661329 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :I had mention before about "scalar monad" of category of matrices, which would be a identity matrix multiplied and divided by the nonzero scalar number (unless, it is a mistake), and that the Kleisli category is just as good as the original, and that it could also be a comonad just as good as the monad. < 1698383041 963916 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :But, I guess that identity monad of any category is a kind of scalar monad, and that a scalar monad is also possible by multiplying any category by any abelian group (such as a group of only one element). Is it? < 1698384298 194020 :b_jonas!~x@89.134.29.108 QUIT :Ping timeout: 260 seconds > 1698384338 185148 PRIVMSG #esolangs :14[[07Four14]]4 M10 02https://esolangs.org/w/index.php?diff=118425&oldid=77876 5* 03PythonshellDebugwindow 5* (+118) 10Categories < 1698384399 443991 :b_jonas!~x@89.134.6.47 JOIN #esolangs * :b_jonas < 1698384626 920271 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :Sometimes a bold 2 is used in category theory to mean a category with two objects and the arrow only one way. But, I think it would be consistent with usual mathematical notation for non-bold numbers to denote discrete categories. < 1698384716 947419 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :What is your opinion? < 1698389209 376642 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User < 1698393906 468757 :__monty__!~toonn@user/toonn JOIN #esolangs toonn :Unknown < 1698394794 106708 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer < 1698398643 234532 :arseniiv!~arseniiv@188.64.15.98 JOIN #esolangs arseniiv :the chaotic arseniiv > 1698404124 64807 PRIVMSG #esolangs :14[[073 Bits, 3 Bytes14]]4 10 02https://esolangs.org/w/index.php?diff=118426&oldid=118367 5* 03None1 5* (+124) 10Added Python interpreter and implemented category tag > 1698404422 595994 PRIVMSG #esolangs :14[[07Drawfuck14]]4 10 02https://esolangs.org/w/index.php?diff=118427&oldid=105205 5* 03None1 5* (+50) 10 > 1698404439 130690 PRIVMSG #esolangs :14[[07Drawfuck14]]4 M10 02https://esolangs.org/w/index.php?diff=118428&oldid=118427 5* 03None1 5* (+1) 10 > 1698404521 492936 PRIVMSG #esolangs :14[[073 Bits, 3 Bytes14]]4 10 02https://esolangs.org/w/index.php?diff=118429&oldid=118426 5* 03None1 5* (+23) 10/* See also */ > 1698404589 963799 PRIVMSG #esolangs :14[[072 Bits, 1 Byte14]]4 10 02https://esolangs.org/w/index.php?diff=118430&oldid=118297 5* 03None1 5* (+58) 10 > 1698409701 733303 PRIVMSG #esolangs :14[[07Drawfuck14]]4 10 02https://esolangs.org/w/index.php?diff=118431&oldid=118428 5* 03None1 5* (+214) 10 > 1698409851 421026 PRIVMSG #esolangs :14[[07Drawfuck14]]4 M10 02https://esolangs.org/w/index.php?diff=118432&oldid=118431 5* 03None1 5* (-1) 10 > 1698409905 630903 PRIVMSG #esolangs :14[[07Drawfuck14]]4 M10 02https://esolangs.org/w/index.php?diff=118433&oldid=118432 5* 03None1 5* (-2) 10 > 1698410076 694443 PRIVMSG #esolangs :14[[07User:None114]]4 10 02https://esolangs.org/w/index.php?diff=118434&oldid=118377 5* 03None1 5* (+28) 10/* My Implementations */ < 1698410773 460782 :b_jonas!~x@89.134.6.47 QUIT :Ping timeout: 255 seconds < 1698410880 108673 :b_jonas!~x@89.134.28.158 JOIN #esolangs * :b_jonas > 1698414637 493950 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Huywall 5* 10New user account < 1698416932 839124 :cpressey!~cpressey@host-80-47-6-160.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey < 1698417468 338759 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :zzo38: my opinion is that you could probably make it consistent, but I don't see that it gets you anything really interesting < 1698417496 499996 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :5+9=14 except 5, 9, and 14 are categories and + is some special operation that takes pairs of categories and yields another category < 1698417557 42857 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Other than forcing you to come up with the definition of + in this context that handles the extra structure < 1698417638 840967 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :But then, I'm heavily biased away from category theory, so don't trust anything I say about it. < 1698418145 903103 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :For that matter, don't trust anything I say about anything. < 1698418479 368430 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname < 1698418693 478452 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :I'm trying to get my brain to do something productive but I'm having no luck. < 1698419201 857574 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :there seems to be no decent statement of the halting problem for lambda calculus online.... < 1698419307 456058 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :but several wrong one, that ask if there is a function that given argument x will produce true or false depending on whether x has a normal form < 1698419320 843853 :int-e!~noone@int-e.eu PRIVMSG #esolangs :try "weak normalization" < 1698419378 79443 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(There's also solvability which is related and important for semantics (it characterizes non-bottom values) but quite different.) < 1698419432 518120 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :a decent statement would ask for a function that is given a *description* of a term, rather than just the term < 1698419446 745447 :int-e!~noone@int-e.eu PRIVMSG #esolangs :The "normalization" terminology is a bit overloaded though. < 1698419485 567418 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tromp: How's that different as long as you don't do infinitary lambda calculus? < 1698419490 686390 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :The untyped lambda calculus isn't even weakly normalizing < 1698419502 668860 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Some terms don't have a normal form < 1698419537 817027 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :if you're just given the term, then the function would have to be strict, and obviously can't yield true or false when given omega < 1698419569 916226 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :but given a description of omega, it could at least recognize that < 1698419581 87753 :int-e!~noone@int-e.eu PRIVMSG #esolangs :cpressey: Those notions have a term-level meaning too. A term can be weakly normalizing and if you use left-most outermost reduction then that will reach a normal form. < 1698419652 888356 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :e.g. here's a bad statement : https://boarders.github.io/posts/halting1.html < 1698419702 479309 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Well I think omega is non-terminating, even though it kind of never makes any progress when reducing it. < 1698419705 913544 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :"Halting problem" feels like "There is no effective algorithm to say whether or not a given term has a normal form" < 1698419729 862512 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :but you must be given a *description* of the term < 1698419752 998102 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Oh. < 1698419772 137380 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Sorry, I was focussed on defining halting. < 1698419781 449167 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :i noticed:) < 1698419789 318197 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Sure, you need an encoding of terms to use them as inputs to something else. > 1698419806 974516 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=118435&oldid=118417 5* 03PaxtonPenguin 5* (+16) 10 < 1698419821 516393 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :but i couldn't find any such proper statement of the lambda calculus halting problem < 1698419831 339378 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Encoding TM's on TM tapes is old hat, encoding lambda terms in lambda terms is less well trodden < 1698419845 474826 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Which is the kind of thing computability theory is usually very sketchy on, because the details are interchangeable. < 1698419871 647364 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Whether you use BLC-like lists of bools, or an actual tree type... they can be transcoded. > 1698419933 687583 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=118436&oldid=118435 5* 03PaxtonPenguin 5* (+74) 10 < 1698419943 938103 :int-e!~noone@int-e.eu PRIVMSG #esolangs :And yeah that definition is bad because it foregoes the encoding step. > 1698419955 115856 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=118437&oldid=118436 5* 03PaxtonPenguin 5* (+4) 10 < 1698420004 37701 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :I've seen attempts to add quoting to the lambda calculus, and thought that I'm sure you can also do that with Church-type encodings of some kind, so the quoting doesn't really add anything except convenience. < 1698420006 943039 :int-e!~noone@int-e.eu PRIVMSG #esolangs :. o O ( Maybe the last person who was precise about encodings was Gödel. ;-) ) < 1698420041 758932 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(I know that to be false but I think it makes a nice piece of shittalk) > 1698420057 763044 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=118438&oldid=118437 5* 03PaxtonPenguin 5* (+80) 10 > 1698420152 588468 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=118439&oldid=118438 5* 03PaxtonPenguin 5* (+51) 10 > 1698420165 751817 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/Sandbox14]]4 M10 02https://esolangs.org/w/index.php?diff=118440&oldid=118439 5* 03PaxtonPenguin 5* (+2) 10 < 1698420183 431370 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tromp: In any case, for you (and also me) BLC is the natural choice I think. You just have to decide whether to use bare lambda terms or the full convention with input. < 1698420224 866050 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :here's a proper proof of impossibility of halting probnlem in lambda calcu;us: < 1698420246 213369 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Denote by "T" some encoding of lambda term T, < 1698420246 290464 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :and let decode be a corresponding decoder, i.e. < 1698420246 306517 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :decode "T" = T < 1698420246 319269 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Suppose there exist a lambda term hasNF which, < 1698420246 325266 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :when applied to "T" for some lambda term T, < 1698420246 927124 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :results in True when T has a normal form, < 1698420247 5614 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :and in False when T has none. < 1698420247 931285 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Let P = \p. hasNF (decode p p) Omega Id < 1698420248 4508 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :P "P" = hasNF (int "P" "P") Omega Id < 1698420248 936946 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs : = hasNF ( P "P") Omega Id < 1698420248 971740 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs : = Omega iff P "P" has a normal form < 1698420249 927160 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Contradiction < 1698420302 173377 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :sorry for spamming:( < 1698420304 532719 :int-e!~noone@int-e.eu PRIVMSG #esolangs :. o O ( s/decode/uni/ ) < 1698420332 41633 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Or int, I guess. < 1698420341 538388 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Ah no < 1698420411 406988 :int-e!~noone@int-e.eu PRIVMSG #esolangs :tromp: Per the previous discussion you should pass a description of P "P" to `hasNF`. So more of a hasNF (apply p (quote p)) > 1698420510 943729 PRIVMSG #esolangs :14[[07User:PaxtonPenguin/ExtremelyLongNameThatNoOneWillGuess14]]4 N10 02https://esolangs.org/w/index.php?oldid=118441 5* 03PaxtonPenguin 5* (+4) 10Created page with "Test" < 1698420529 707089 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :ah, right. thanks for noticing! this is subtle indeed < 1698420532 389821 :razetime!~razetime@sd202148.hung.ab.nthu.edu.tw JOIN #esolangs razetime :realname < 1698420910 327454 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Hmm. Something like quote [] = "010110", quote (0:xs) = "01000010010110" ++ quote xs, quote (1:xs) = "010000100101110" ++ quote xs, and apply xs ys = "01" ++ xs ++ ys. < 1698420932 31665 :int-e!~noone@int-e.eu PRIVMSG #esolangs :BLC is too simple ;-) < 1698420980 827576 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(The most likely mistake here is that I may have swapped the 0 and 1 in the input of quote) < 1698421028 811164 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(and of course those two digits are bools) < 1698421149 154073 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs : Other than forcing you to come up with the definition of + in this context that handles the extra structure => I think disjoint union suffices: objects(C + D) = objects(C) ⊔ objects(D); morphisms are copied as well. No new ones are added < 1698421206 708810 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Err, and of course `apply` should be using "00" instead of "01". Tsk. < 1698421298 982539 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :such a + should ideally satisfy the coproduct definition if taken to a suitable category of categories (e. g. Cat, of all small categories). Probably works for 2-categories and so on, I don’t see anything that needs to be added in those cases < 1698421423 607402 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :so my proof should have these lines instead: < 1698421425 663976 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Given "T", we can compute the encoding of T applied to "T", denoted "T "T" ". < 1698421431 483194 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Let P "T" = hasNF "T "T" " Omega Id < 1698421599 283675 :int-e!~noone@int-e.eu PRIVMSG #esolangs :. o O ( ⌜T ⌜T⌝⌝ ) < 1698421646 181156 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :arseniiv: I'm slightly suspicious of this "disjoint union" of which you speak.  But I don't remember my reasons for that suspicion.  Anyway, what you say seems plausible. < 1698421655 333149 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Sadly that looks ugly in the fixed font. But that notation can actually be nested :) < 1698421792 591000 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :zzo38: I think what I saw denoted as 0, 1, 2, 3, … somewhere was indeed discrete categories. Though one could easily see why ordinals as preorder categories can be useful to many people. This is essentially cardinal arithmetic vs. ordinal arithmetic, I suspect at 95% < 1698421887 213733 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :cpressey: I’d be interested to know if you remember what it was! < 1698421910 302004 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :btw I think disjoint union doesn’t have enough love in math popularization and even just in some math courses < 1698421950 125362 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :it’s always cartesian this cartesian that < 1698421984 236953 :int-e!~noone@int-e.eu PRIVMSG #esolangs :. o O ( Do they also give out cartesian hats? ) < 1698422005 69069 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :also I embraced universal properties with all my heart when I finally started cracking them one after another < 1698422026 660350 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :arseniiv: something about how algebraic data types are a luxury; you can do it all with pairs and Either; and Either could be replaced by Kuratowski pairs...? < 1698422127 82448 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Of course I guess disjoint union is disjoint union even if you do it with something like Kuratowski pairs < 1698422162 975106 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :cpressey: in lambda calculus, sure it all can be encoded, by Scott, some other guy or them jointly, I forget which way is which but it differs in what we recurse to < 1698422181 777233 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :I mean more generally, it has so much use in e. g. even examples of structures < 1698422237 108146 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Wikipedia is making me think there is no such thing as a Kuratowski pair now.  Have I got the name wrong or have I ASCII-ized the letters in it or something < 1698422278 620002 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :anecdote: I think I even saw disjoint union in disguise, encoded in its usual way via (0, x) and (1, x), with no calling it by its name. I guess that can be warranted if one doesn’t want to add distractions to the reader but still < 1698422296 160096 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :Oh I was accidentally searching wiktionary.  OK then! < 1698422313 451462 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :cpressey: it should be. At first I didn’t remember about them but then I remembered it’s {{x}, {x, y}} < 1698422339 59663 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :initially I thought it somehow relates to λ heehee < 1698422559 993713 :cpressey!~cpressey@host-80-47-6-160.as13285.net PRIVMSG #esolangs :I guess my suspicion was more about tags -- was trying to see if it's possible to escape that concept.  0 and 1 would still be tags.  Kuratowski pair isn't quite right, but it's close.  Something like {x} and {{x}}, with the union being {x, {x}}?  The "tag" is still there I guess, it's just represented by an extra level of nesting < 1698422786 357459 :cpressey!~cpressey@host-80-47-6-160.as13285.net QUIT :Quit: Client closed < 1698423278 965034 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :cpressey: yeah, I don’t know any representation with no tags, that is if we define disjoint union by concrete implementation < 1698423304 259321 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :and don’t have any equivalent concept before that < 1698423355 555458 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :like Either and algebraic data types you mentioned < 1698423775 417879 :sprout_!~quassel@2a02-a448-3a80-0-c48d-b712-9bab-12f5.fixed6.kpn.net JOIN #esolangs * :sprout < 1698423822 376669 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :one can say implementation with tags is due to A + A ≅ 2 × A and similar equations. Though that requires union to be here because otherwise we can’t inject different operands of + into the same A on rhs not having disjoint union beforehand. So I guess that’s why type theories tend to have disjoint union as a primitive (or algebraic types or inductive types) < 1698423866 37346 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :because union as a primitive might not be ideal < 1698423992 582728 :sprout!~quassel@2a02-a448-3a80-0-a140-dd2-1bda-8a59.fixed6.kpn.net QUIT :Ping timeout: 258 seconds < 1698424095 465075 :sprout_!~quassel@2a02-a448-3a80-0-c48d-b712-9bab-12f5.fixed6.kpn.net NICK :sprout < 1698424130 951797 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :because union has universal property based on subtyping A <: B and not functions A → B, in a type system with no explicit subtyping involved, especially no user-definable one, it’s somewhat unhinged; that’s how I get it < 1698424158 4856 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :disjoint union has the same property but wrt A → B < 1698424186 523491 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :. o O ( set theory with subtyping ) < 1698424199 756259 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :hm wait it’s the usual one probably > 1698424414 606721 PRIVMSG #esolangs :14[[07Wise14]]4 10 02https://esolangs.org/w/index.php?diff=118442&oldid=118330 5* 03DivergentClouds 5* (+119) 10changed branching operators to only check C digits > 1698425536 21937 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Philiquaz 5* 10New user account > 1698425820 203583 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=118443&oldid=118410 5* 03Philiquaz 5* (+179) 10 < 1698425835 56034 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz… > 1698425853 161745 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=118444&oldid=118443 5* 03Philiquaz 5* (-9) 10 < 1698426560 384700 :razetime!~razetime@sd202148.hung.ab.nthu.edu.tw QUIT :Ping timeout: 255 seconds < 1698427528 5194 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User < 1698428459 58421 :Wryl-o-the-wisp!sid553797@user/wryl QUIT : < 1698428477 949539 :Wryl-o-the-wisp!sid553797@user/wryl JOIN #esolangs Wryl :Wryl < 1698431797 126183 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz… > 1698431958 655472 PRIVMSG #esolangs :14[[07A-SCP-M14]]4 N10 02https://esolangs.org/w/index.php?oldid=118445 5* 03Philiquaz 5* (+6013) 10Created page with "'''A-SCP-M''' is an assembly language in the same vein as the SCP project. As a result, it must be contained to being an esoteric joke language, and must not under any circumstances actually be implemented or used. If you feel the vague urge to implement it, or you se < 1698432935 834123 :b_jonas!~x@89.134.28.158 PRIVMSG #esolangs :“algebraic data types are a luxury; you can do it all with pairs and Either” => standard ML goes halfway there: you can define your own algebraic data types, that gives you a disjoint union, but each variant constructor can take only zero or one arguments, so you need tuples to make a product < 1698432971 215904 :b_jonas!~x@89.134.28.158 PRIVMSG #esolangs :though I might be misremembering this < 1698433104 859103 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User > 1698434004 257879 PRIVMSG #esolangs :14[[07A-SCP-M14]]4 M10 02https://esolangs.org/w/index.php?diff=118446&oldid=118445 5* 03PythonshellDebugwindow 5* (+52) 10Categories > 1698434131 983362 PRIVMSG #esolangs :14[[07Language list14]]4 M10 02https://esolangs.org/w/index.php?diff=118447&oldid=118375 5* 03PythonshellDebugwindow 5* (+14) 10/* A */ add < 1698438401 641189 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :b_jonas: yeah I saw that in code though haven’t read exactly ML docs/definitions. I think each constructor takes exactly one argument and you use `unit` (IIRC) in case there are effectively none, like Haskell’s () < 1698438429 557991 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :having 0 or 1 looks unsystematic enough to be eschewed < 1698438437 736713 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :than having 1 < 1698438724 421947 :b_jonas!~x@89.134.28.158 PRIVMSG #esolangs :arseniiv: might be unsysthematic but no argument constructor is real, see the fieldnum type in view-source:http://math.bme.hu/~ambrus/pu/olvashato/aknakereso.sml for exmaple < 1698438774 127248 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :b_jonas: quirky. Then I don’t know how it happened to ML < 1698438837 279870 :b_jonas!~x@89.134.28.158 PRIVMSG #esolangs :but of course that doesn't prove that there aren't curry-style multi-argument constructors too, even if I don't have them in my code < 1698438938 822526 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :though in all examples I have seen in articles and such, I never encountered that either < 1698439001 102432 :arseniiv!~arseniiv@188.64.15.98 PRIVMSG #esolangs :it looks like a feature of ML languages but maybe some of them added syntax? < 1698439170 125972 :arseniiv!~arseniiv@188.64.15.98 QUIT :Quit: gone too far < 1698440879 242133 :__monty__!~toonn@user/toonn QUIT :Quit: leaving < 1698442561 728739 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Read error: Connection reset by peer < 1698447270 270079 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)