< 1700526346 763353 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :question on stackexchange today: "is there a language like haskell, but that allows pattern matching on arbitrary expressions instead of just constructors?" < 1700526437 322054 :dutchkin!~dutchkin@45.144.113.234 QUIT :Remote host closed the connection < 1700526478 425642 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I guess it depends on how arbitrary you want to get < 1700526488 922867 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :like, do you want to be able to match 2 against x+1 and end up with the binding x=1? < 1700526507 462716 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :yes < 1700526508 701756 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that taken to its extremes would be pretty esoteric < 1700526527 344932 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :there are Prolog dialects that aim to do something like that, but there are a lot of complexities and caveats < 1700526538 922807 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and the syntax is a bit inconvenient < 1700526540 279218 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :so I guess it would involve a solver every time you try to pattern match < 1700526581 397915 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :just so you can write stuff like addOne (x-1) = x < 1700526639 400271 :ais523!~ais523@user/ais523 QUIT :Quit: sorry about my connection < 1700526654 507551 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name) < 1700526687 471623 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :so I guess it would involve a solver every time you try to pattern match < 1700526688 895947 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :just so you can write stuff like addOne (x-1) = x < 1700526746 800192 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :apparently you can pattern match on functions in Curry, but I guess only if the functions do nothing more than add constructors: https://en.wikipedia.org/wiki/Curry_(programming_language)#Functional_patterns < 1700527246 537598 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :Koen: firstly, Haskell would have a syntactic problem with this because if you try to use a function call as a pattern then it'll try to define the function in the head of that call. secondly, I think this isn't possible in general because you can set up some stupid paradox, < 1700527394 273664 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :like try to match `[f ()] = [False]` but with the function f defined so that it returns True if that same match matches, like `f () = case False of { [f ()] -> True; _ -> False; }` < 1700527409 713513 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :no sorry, `f () = case [False] of { [f ()] -> True; _ -> False; }` < 1700527441 782695 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :oh, that's violent < 1700527496 136496 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :I was thinking more simples issues like squareRoot (x^2) = x < 1700527501 65880 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :perhaps you can define the rules such that this is just an infinite loop, but I don't think you can get a sane matching from this < 1700527520 690188 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :eh, we can solve a square root, that's a well-known problem < 1700527590 558010 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :sure, you might also give the match problems that are slow to solve, like [x * y] = some large composite number < 1700527605 289446 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :even ones that are well-defined but much slower to solve than factoring < 1700527605 422372 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :well yes but returning -3 or 3 for squareRoot 9 would both be correcrt < 1700527627 233278 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :yeah, sometimes there can be multiple matches < 1700527658 362070 :sprout!~quassel@2a02-a448-3a80-0-d9fb-72a0-648d-8ba0.fixed6.kpn.net QUIT :Ping timeout: 256 seconds < 1700527708 845498 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :if you want to mention that paradox at https://langdev.stackexchange.com/questions/3194/are-there-haskell-like-languages-where-equations-allow-for-arbitrary-left-hand-s I think it would be a great answer < 1700527734 242700 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :(I didn't ask the question, just stumbled upon it and thought that was something for #esolangs) < 1700527812 491866 :ais523!~ais523@user/ais523 QUIT :Remote host closed the connection < 1700527827 59620 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name) < 1700527996 324451 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :I guess in the spriti of Raymond Smullyan I should suggest `f () = case [False] of { you pay me a million dollars -> False; [f ()] -> True; _ -> False; }` in which case to evaluate `f ()` the interpreter must make you to pay me a million dollars < 1700528007 645709 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :because otherwise you get a paradox < 1700528024 868982 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :but it's not clear if you can do something like that into a purely functional language like Haskell < 1700528101 223771 :ais523!~ais523@user/ais523 PRIVMSG #esolangs : Definitions and prescriptions in the rules are only to be applied using direct, forward reasoning; in particular, an absurdity that can be concluded from the assumption that a statement about rule-defined concepts is false does not constitute proof that it is true. < 1700528153 651028 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :Agora decided that just because it's *possible* to resolve something to a truth value doesn't necessarily mean you *should* < 1700528187 586638 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :like, it makes more sense to conclude that the function doesn't evaluate to anything than to pay you a million dollars to make it evaluable < 1700528202 576057 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :yeah, smullyan gives that lesson in one exercise < 1700528346 351188 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :in chapter 5 of "What is the name of this book?" < 1700528367 784789 :sprout!~quassel@2a02-a448-3a80-0-35f0-db7a-ed7f-d230.fixed6.kpn.net JOIN #esolangs sprout :sprout < 1700528984 547422 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :ah yes < 1700529004 56373 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :I read something like that like two days ago < 1700529146 114278 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :I had only ever read "the lady or the tiger" and last week I decided to get what is the name of this book in ebook < 1700529244 86153 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :the lady and the tiger might also have that lesson somewhere. I don't remember everything in the books off-hand. < 1700529280 463018 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :i remember most of the riddles being extremely easy up to a point < 1700529285 306047 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :and then suddenly becoming impossible < 1700529336 655797 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :like for two thirds of the book it's just small variations on "there are three people in front of you. the first one says that the second one is lying. hte second one says..." etc < 1700529385 612276 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 PRIVMSG #esolangs :and then suddenly it's "a princess is exchanging secret codes with her suitor. can you break the code (and prove godel's theorem)?" < 1700534168 396903 :ais523!~ais523@user/ais523 QUIT :Quit: quit < 1700538505 958212 :dutchkin!~dutchkin@45.144.113.234 JOIN #esolangs dutchkin :dutchkin < 1700538964 209257 :Koen!~Koen@2a01:e34:ec7c:30:b00d:bb02:8745:36c8 QUIT :Quit: Leaving... > 1700540358 182910 PRIVMSG #esolangs :14[[07Hrdfish14]]4 M10 02https://esolangs.org/w/index.php?diff=119738&oldid=119729 5* 03PythonshellDebugwindow 5* (+18) 10/* See also */ Hrdfsh > 1700540401 762172 PRIVMSG #esolangs :14[[07Hrdfsh14]]4 M10 02https://esolangs.org/w/index.php?diff=119739&oldid=119721 5* 03PythonshellDebugwindow 5* (+30) 10Hrdfish > 1700540648 369431 PRIVMSG #esolangs :14[[07Special:Log/move14]]4 move10 02 5* 03PythonshellDebugwindow 5* 10moved [[02Meow10]] to [[Meow (Martsadas)]]: Disambiguation > 1700540757 698647 PRIVMSG #esolangs :14[[07Meow14]]4 M10 02https://esolangs.org/w/index.php?diff=119742&oldid=119741 5* 03PythonshellDebugwindow 5* (+89) 10Disambiguation page > 1700540913 846966 PRIVMSG #esolangs :14[[07Meowlang14]]4 M10 02https://esolangs.org/w/index.php?diff=119743&oldid=88072 5* 03PythonshellDebugwindow 5* (+105) 10Distinguish confusion, add categories > 1700540946 398850 PRIVMSG #esolangs :14[[07Meow (Martsadas)14]]4 M10 02https://esolangs.org/w/index.php?diff=119744&oldid=119740 5* 03PythonshellDebugwindow 5* (+2) 10Bold > 1700541015 401891 PRIVMSG #esolangs :14[[07Language list14]]4 M10 02https://esolangs.org/w/index.php?diff=119745&oldid=119734 5* 03PythonshellDebugwindow 5* (+42) 10/* M */ add > 1700541100 924696 PRIVMSG #esolangs :14[[07Cripl14]]4 M10 02https://esolangs.org/w/index.php?diff=119746&oldid=104017 5* 03PythonshellDebugwindow 5* (-8) 10Fix double redirect > 1700541135 510410 PRIVMSG #esolangs :14[[07UniLang14]]4 M10 02https://esolangs.org/w/index.php?diff=119747&oldid=118626 5* 03PythonshellDebugwindow 5* (+2) 10Fix double redirect > 1700541193 140730 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Para 5* 10New user account > 1700541253 153439 PRIVMSG #esolangs :14[[07CharCode14]]4 M10 02https://esolangs.org/w/index.php?diff=119748&oldid=119106 5* 03PythonshellDebugwindow 5* (+79) 10Categories > 1700541344 884637 PRIVMSG #esolangs :14[[07ProjectEuler:2414]]4 M10 02https://esolangs.org/w/index.php?diff=119749&oldid=117002 5* 03PythonshellDebugwindow 5* (+1) 10Fix double redirect > 1700541380 636561 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=119750&oldid=119552 5* 03Para 5* (+182) 10 > 1700541416 895357 PRIVMSG #esolangs :14[[07Onlynumber14]]4 M10 02https://esolangs.org/w/index.php?diff=119751&oldid=116940 5* 03PythonshellDebugwindow 5* (+1) 10Fix double redirect > 1700541472 205407 PRIVMSG #esolangs :14[[07Befunge-9814]]4 M10 02https://esolangs.org/w/index.php?diff=119752&oldid=107304 5* 03PythonshellDebugwindow 5* (+3) 10Fix double redirect > 1700541658 776954 PRIVMSG #esolangs :14[[07Language list14]]4 M10 02https://esolangs.org/w/index.php?diff=119753&oldid=119745 5* 03PythonshellDebugwindow 5* (+12) 10/* R */ add > 1700541957 814105 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03Snacked 5* 10New user account > 1700542053 565672 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=119754&oldid=119750 5* 03Snacked 5* (+143) 10 > 1700542392 523569 PRIVMSG #esolangs :14[[071 byte :514]]4 M10 02https://esolangs.org/w/index.php?diff=119755&oldid=116554 5* 03PythonshellDebugwindow 5* (+27) 10Stub, category > 1700542493 431772 PRIVMSG #esolangs :14[[07A114]]4 M10 02https://esolangs.org/w/index.php?diff=119756&oldid=65385 5* 03PythonshellDebugwindow 5* (+74) 10External resources, categories < 1700544292 758426 :Sgeo_!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname < 1700544478 664439 :Sgeo!~Sgeo@user/sgeo QUIT :Ping timeout: 255 seconds < 1700546031 228099 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User < 1700546681 417927 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1700547394 603973 :dutchkin!~dutchkin@45.144.113.234 QUIT :Ping timeout: 255 seconds < 1700547549 659949 :dutchkin!~dutchkin@194.124.76.102 JOIN #esolangs dutchkin :dutchkin < 1700547958 30794 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User < 1700551429 743406 :dutchkin!~dutchkin@194.124.76.102 PART #esolangs :Konversation terminated! < 1700556168 752697 :cpressey!~cpressey@host-92-21-196-138.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey < 1700556976 559567 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs : "nothing wrong with reading the values (or bytes) of an abstract data structure" => sure there is, it leads to the maintainer of that data type not being able to improve the implementation without incompatibility <-- Okay, I was thinking in terms of the integrity of the data structure when I wrote that, not software engineering issues. I < 1700556977 53488 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :grant that the phrase "nothing wrong" was too sweeping. It was late. < 1700557070 964752 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Even "software engineering issues" is probably interpretable, maybe "programming-in-the-large" would be more specific < 1700557887 697021 :Sgeo_!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer < 1700559236 68012 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1700561138 431091 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord < 1700561191 909224 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 268 seconds < 1700561317 141806 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life > 1700562716 81981 PRIVMSG #esolangs :14[[07Template talk:Py14]]4 10 02https://esolangs.org/w/index.php?diff=119757&oldid=119716 5* 03None1 5* (+198) 10You convert to wiki formatting locally first < 1700563833 909375 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User < 1700564146 7485 :Koen!~Koen@2a01:e34:ec7c:30:b192:32da:e70d:f325 JOIN #esolangs * :Koen > 1700565712 942481 PRIVMSG #esolangs :14[[07Cutw14]]4 10 02https://esolangs.org/w/index.php?diff=119758&oldid=110199 5* 03None1 5* (+28) 10 > 1700565722 499356 PRIVMSG #esolangs :14[[07Cutw14]]4 M10 02https://esolangs.org/w/index.php?diff=119759&oldid=119758 5* 03None1 5* (-1) 10/* See also= */ < 1700565726 504489 :FreeFull!~freefull@46.205.214.63.nat.ftth.dynamic.t-mobile.pl QUIT : > 1700565743 182598 PRIVMSG #esolangs :14[[07Alphuck14]]4 10 02https://esolangs.org/w/index.php?diff=119760&oldid=89425 5* 03None1 5* (+23) 10/* Hello, World! program */ > 1700565814 697425 PRIVMSG #esolangs :14[[07Talk:Cutw14]]4 N10 02https://esolangs.org/w/index.php?oldid=119761 5* 03None1 5* (+160) 10Created page with "I came here from random page and wanted to make an interpreter for this esolang. --~~~~" < 1700565986 649621 :cpressey!~cpressey@host-92-21-196-138.as13285.net QUIT :Quit: Client closed > 1700566088 406012 PRIVMSG #esolangs :14[[07Cutw14]]4 10 02https://esolangs.org/w/index.php?diff=119762&oldid=119759 5* 03None1 5* (+2085) 10 > 1700566134 614142 PRIVMSG #esolangs :14[[07User:None114]]4 10 02https://esolangs.org/w/index.php?diff=119763&oldid=119724 5* 03None1 5* (+24) 10/* My Implementations */ > 1700566206 697290 PRIVMSG #esolangs :14[[07Cutw14]]4 10 02https://esolangs.org/w/index.php?diff=119764&oldid=119762 5* 03None1 5* (-4) 10/* JavaScript interpreter */ < 1700566216 725889 :APic!apic@apic.name PRIVMSG #esolangs :Moin < 1700566271 868894 :cpressey!~cpressey@host-92-21-196-138.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey < 1700566572 462354 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs : this just requires a memory-safe language, not a strongly typed one <--- Thing is, "strongly typed" is not very well defined, and in practice it seems to mean "disallows 'dangerous' type casts" which seems to boil down to "memory-safe" < 1700566744 693565 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :cpressey: that's definitely not what I think of as strongly typed. by strongly typed I mean statically typed, the types determined at compile time < 1700566801 215555 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :C is statically typed but widely regarded as weakly typed because you can cast anything to anything < 1700566949 645080 :int-e!~noone@int-e.eu PRIVMSG #esolangs :also unions < 1700566955 149978 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Which suggests the essence of "weak vs strong" has nothing really to do with when you apply the type checking but rather what the type checking prevents.  Lots of dynamically typed languages would have strong typing under this interpretation. < 1700567016 711417 :int-e!~noone@int-e.eu PRIVMSG #esolangs :"my types are stronger than yours" < 1700567021 693488 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Except for the fact that you can inevitably link in C libraries and call out to C functions in these languages, which destroys all these properties, but we're going to ignore that, right < 1700567099 74496 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Anyway, it's all microservices now, which permit a most excellent form of information hiding: the internals of this data structure are on a different machine entirely < 1700567128 23487 :int-e!~noone@int-e.eu PRIVMSG #esolangs :there's also an expressiveness angle mixed into strength sometimes < 1700567179 824135 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(there is a connection... the more expressive the type system, the less need you'll have for casts) < 1700567239 864367 :MizMahem!sid296354@user/mizmahem QUIT :Ping timeout: 256 seconds < 1700567286 193373 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(C may be strongly typed but then you also have void * everywhere connected to heap management... and the compiler won't save you when you cast the wrong thing) < 1700567366 937394 :Swyrl!sid553797@user/wryl QUIT :Ping timeout: 252 seconds < 1700567371 473633 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :memory safety isn't just about casting anything to anything else, as you know, it's also about not indexing out of arrays, and about not dereferencing stale pointers > 1700567398 242697 PRIVMSG #esolangs :14[[07Wymaewyha14]]4 N10 02https://esolangs.org/w/index.php?oldid=119765 5* 03Yes 5* (+694) 10Created page with "Wymaewyha stands for When You Make An Esolang When Your Half Asleep
It is a brainfuck deteritave by [[User:Yes]] that was probably made when he was half asleep.
It is what it sounds like.

Commands

 wake up              start program go back to slee
< 1700567414 63270 :int-e!~noone@int-e.eu PRIVMSG #esolangs :I'm sure memory safety means different things to different people too.
> 1700567422 754034 PRIVMSG #esolangs :14[[07User:Yes14]]4 10 02https://esolangs.org/w/index.php?diff=119766&oldid=107502 5* 03Yes 5* (+19) 10
> 1700567451 591654 PRIVMSG #esolangs :14[[07User:Yes14]]4 10 02https://esolangs.org/w/index.php?diff=119767&oldid=119766 5* 03Yes 5* (+0) 10
< 1700567459 196086 :int-e!~noone@int-e.eu PRIVMSG #esolangs :And you don't need strong types for that, see Python. Or, hell, Lisp if we want ancient history.
< 1700567579 774798 :__monty__!~toonn@user/toonn JOIN #esolangs toonn :Unknown
> 1700567677 717044 PRIVMSG #esolangs :14[[07lang14]]4 10 02https://esolangs.org/w/index.php?diff=119768&oldid=118778 5* 03Yes 5* (+132) 10added [[English]] to intepeters
< 1700567684 261999 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :yes. the two are different. that's what I was trying to say earlier.
< 1700567695 642969 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :but apparently we thought of different things as strong typing.
< 1700567734 45679 :Swyrl!sid553797@user/wryl JOIN #esolangs Wryl :Wryl
> 1700567771 775749 PRIVMSG #esolangs :14[[07lang14]]4 10 02https://esolangs.org/w/index.php?diff=119769&oldid=119768 5* 03Yes 5* (+11) 10not sure why i named it specs in the first place so changed it to "possible outputs"
< 1700567776 825001 :MizMahem!sid296354@user/mizmahem JOIN #esolangs MizMahem :🐍🐔
> 1700568018 140247 PRIVMSG #esolangs :14[[07lang14]]4 10 02https://esolangs.org/w/index.php?diff=119770&oldid=119769 5* 03Yes 5* (+161) 10added cpp to intepeters
> 1700568160 303282 PRIVMSG #esolangs :14[[07lang14]]4 M10 02https://esolangs.org/w/index.php?diff=119771&oldid=119770 5* 03Yes 5* (+2) 10/* C++ Interpreter */
> 1700568190 532152 PRIVMSG #esolangs :14[[07Talk:lang14]]4 10 02https://esolangs.org/w/index.php?diff=119772&oldid=114865 5* 03Yes 5* (+105) 10/* EVEN SHORTER INTERPRETER */
> 1700568527 501004 PRIVMSG #esolangs :14[[07User talk:Lyxal14]]4 10 02https://esolangs.org/w/index.php?diff=119773&oldid=93338 5* 03Yes 5* (+296) 10/* hey uh */ new section
< 1700568935 288241 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :This is why, over time, I've become more and mroe careful to say "statically typed" when I mean statically typed, and "the type system allows  and prevents " when I'm talking about what the type system can and can't do
< 1700569110 30562 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :The thing here is a narrative where people are using these nonspecific terms (like "strong" and "strict") and making claims under them (that you need "strong" or "strict" typing to correctly implement the LCF architecture, basically)
< 1700569353 680694 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :(And by "people" I mean, like, Lawrence Paulson and Michael Gordon!  If you have a page on Wikipedia identifying you as a computer scientist I expect a certain level of rigour, y'know?)
< 1700569459 50999 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :I think you could *probably* implement the LCF architecture in untyped lambda calculus.
< 1700569462 53616 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :I am tempted to try.
< 1700569491 450613 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :I would need a refresher course in all that Church encoding stuff.
< 1700569663 437591 :int-e!~noone@int-e.eu PRIVMSG #esolangs :ML translates to System F (preserving types) which has subject reduction so you can erase types. But the types are crucial to the correctness. Also the module system for encapsulating internals of proofs and theorems, preventing you from injecting axioms without going through the dedicated function for that.
< 1700569684 228583 :int-e!~noone@int-e.eu PRIVMSG #esolangs :So, yes and no. As usual.
< 1700571087 928719 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :has LCF been implemented in Haskell?
< 1700571630 64541 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Dunno, does Agda have an LCF style kernel?
< 1700571712 622585 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(It's a bit of a mismatch because it's primarily a programming language.)
< 1700571865 428328 :int-e!~noone@int-e.eu PRIVMSG #esolangs :But it's the only bigger name in the field that I can think of that isn't ML or Lisp. Oh and Idris is self-hosting with bootstrapping via scheme?
< 1700571902 416795 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :in a sense, every typed expression (without undefined) in Haskell is already a theorem of sorts
< 1700571937 882739 :Koen!~Koen@2a01:e34:ec7c:30:b192:32da:e70d:f325 QUIT :Remote host closed the connection
< 1700571968 675364 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Sure but AIUI a big part about LCF is managing theorems and exioms, without caring about their proofs.
< 1700572328 163730 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Wikipedia says: Basic idea
< 1700572328 338017 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :Theorems in the system are terms of a special "theorem" abstract data type. The general mechanism of abstract data types of ML ensures that theorems are derived using only the inference rules given by the operations of the theorem abstract type. Users can write arbitrarily complex ML programs to compute theorems; the validity of theorems does not depend on the complexity of such programs, but follows from the soundness of the
< 1700572328 338101 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs : abstract data type implementation and the correctness of the ML compiler.
< 1700572342 843220 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :that sounds quite possible to replicate in Haskell
< 1700572368 13822 :int-e!~noone@int-e.eu PRIVMSG #esolangs :But you asked whether it was done, not whether it could be done.
< 1700572720 907191 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :right. but i took your answer as suggesting  that it would be hard to manage thms/axioms in Haskell
< 1700572868 209496 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Ah but I only meant that programming language implementations aren't theorem provers (LCF style in particular) even if they're dependently typed because they lack theorems as a concept. That's independent from the language they're implemented in (which in your case, would be Haskell)
< 1700572886 724780 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :I feel like untyped lambda calculus would be a singularly bad language to implement this sort of program
> 1700572960 997173 PRIVMSG #esolangs :14[[07Talk:lang14]]4 M10 02https://esolangs.org/w/index.php?diff=119774&oldid=119772 5* 03None1 5* (+0) 10/* lyxal is a genius */
< 1700573068 839548 :Koen!~Koen@2a01:e34:ec7c:30:7c4d:19e1:171d:3e0c JOIN #esolangs * :Koen
< 1700573699 935601 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Here's Gordon's take, which you can compare to WP's: "Milner had the brilliant idea of using an abstract data type whose predefined values were instances of axioms and whose operations were inference rules. Strict typechecking then ensured that the only values that could be created were those that could be obtained from axioms by applying a
< 1700573700 531129 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :sequence of inference rules – namely theorems."
< 1700573711 580969 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :By "strict typechecking" he means "abstract data types".
< 1700573732 983664 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :You can implement the LCF architecture in any language with proper abstract data types.
< 1700573815 500131 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :tromp: I started writing an LCF kernel in Haskell once.  Would be surprised if no one else ever wrote one and got further than I did.
> 1700573818 635223 PRIVMSG #esolangs :14[[07lang14]]4 10 02https://esolangs.org/w/index.php?diff=119775&oldid=119771 5* 03None1 5* (+61) 10/* Python 3 Interpeter */
< 1700573874 811526 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :Haskell has proper abstract data types.  They're not very popular among Haskell programmers it seems, but that's a different issue, I'm sure they have their reasons...
< 1700574196 460056 :cpressey!~cpressey@host-92-21-196-138.as13285.net PRIVMSG #esolangs :I need to stop thinking about these things :/
< 1700574201 830938 :cpressey!~cpressey@host-92-21-196-138.as13285.net QUIT :Quit: Client closed
< 1700576378 97089 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Ping timeout: 256 seconds
< 1700578178 167136 :Koen!~Koen@2a01:e34:ec7c:30:7c4d:19e1:171d:3e0c QUIT :Remote host closed the connection
< 1700583653 157877 :razetime!~razetime@sd202148.hung.ab.nthu.edu.tw JOIN #esolangs razetime :realname
< 1700583675 882965 :razetime!~razetime@sd202148.hung.ab.nthu.edu.tw QUIT :Remote host closed the connection
< 1700584324 664280 :FreeFull!~freefull@46.205.214.63.nat.ftth.dynamic.t-mobile.pl JOIN #esolangs FreeFull :FreeFull
> 1700584877 574545 PRIVMSG #esolangs :14[[07Sd14]]4 M10 02https://esolangs.org/w/index.php?diff=119776&oldid=78851 5* 03PythonshellDebugwindow 5* (+57) 10Categories
> 1700585466 520504 PRIVMSG #esolangs :14[[07lang14]]4 M10 02https://esolangs.org/w/index.php?diff=119777&oldid=119775 5* 03PythonshellDebugwindow 5* (+0) 10/* Python 3 Interpeter */ Fix
> 1700586524 755277 PRIVMSG #esolangs :14[[07Wymaewyha14]]4 M10 02https://esolangs.org/w/index.php?diff=119778&oldid=119765 5* 03PythonshellDebugwindow 5* (+130) 10Stub, wikify, add categories
> 1700586743 767208 PRIVMSG #esolangs :14[[07Hi14]]4 M10 02https://esolangs.org/w/index.php?diff=119779&oldid=115244 5* 03PythonshellDebugwindow 5* (+25) 10Category
> 1700591033 181160 PRIVMSG #esolangs :14[[07Special:Log/newusers14]]4 create10 02 5* 03SigmaOctantis 5*  10New user account
> 1700591422 284759 PRIVMSG #esolangs :14[[07Esolang:Introduce yourself14]]4 10 02https://esolangs.org/w/index.php?diff=119780&oldid=119754 5* 03SigmaOctantis 5* (+396) 10/* Introductions */
< 1700596774 170117 :V!~v@ircpuzzles/2022/april/winner/V QUIT :Ping timeout: 260 seconds
< 1700597013 527423 :V!~v@ircpuzzles/2022/april/winner/V JOIN #esolangs V :Wie?
< 1700597329 854748 :V!~v@ircpuzzles/2022/april/winner/V QUIT :Ping timeout: 256 seconds
< 1700597510 949927 :V!~v@ircpuzzles/2022/april/winner/V JOIN #esolangs V :Wie?
< 1700599528 508918 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1700599841 569423 :__monty__!~toonn@user/toonn QUIT :Quit: leaving
> 1700601371 380329 PRIVMSG #esolangs :14[[07Saturnus14]]4 N10 02https://esolangs.org/w/index.php?oldid=119781 5* 03SigmaOctantis 5* (+2703) 10Created page with "Saturnus is a programming language that aims to have a simplified mix of Rust programming language and Lua.  The main target for Saturnus compiler is Lua, but multi-target compilation will arrive in the future, so stay tuned if you like the language.  The origina
> 1700601675 933409 PRIVMSG #esolangs :14[[07Saturnus14]]4 10 02https://esolangs.org/w/index.php?diff=119782&oldid=119781 5* 03SigmaOctantis 5* (+35) 10
> 1700607406 567621 PRIVMSG #esolangs :14[[07Saturnus14]]4 M10 02https://esolangs.org/w/index.php?diff=119783&oldid=119782 5* 03PythonshellDebugwindow 5* (+73) 10Categories
> 1700607582 552536 PRIVMSG #esolangs :14[[07Language list14]]4 M10 02https://esolangs.org/w/index.php?diff=119784&oldid=119753 5* 03PythonshellDebugwindow 5* (+51) 10/* S */ add
> 1700607877 740340 PRIVMSG #esolangs :14[[07IDKHIW14]]4 M10 02https://esolangs.org/w/index.php?diff=119785&oldid=119409 5* 03PythonshellDebugwindow 5* (+33) 10Stub, category
< 1700608466 26321 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname
> 1700611129 445795 PRIVMSG #esolangs :14[[07Cellular automaton14]]4 M10 02https://esolangs.org/w/index.php?diff=119786&oldid=78704 5* 03PythonshellDebugwindow 5* (+34) 10/* See also */ Category