00:25:46 <Koen> question on stackexchange today: "is there a language like haskell, but that allows pattern matching on arbitrary expressions instead of just constructors?"
00:27:17 -!- dutchkin has quit (Remote host closed the connection).
00:27:58 <ais523> I guess it depends on how arbitrary you want to get
00:28:08 <ais523> like, do you want to be able to match 2 against x+1 and end up with the binding x=1?
00:28:27 <Koen> yes
00:28:28 <ais523> that taken to its extremes would be pretty esoteric
00:28:47 <ais523> there are Prolog dialects that aim to do something like that, but there are a lot of complexities and caveats
00:28:58 <ais523> and the syntax is a bit inconvenient
00:29:00 <Koen> so I guess it would involve a solver every time you try to pattern match
00:29:41 <Koen> just so you can write stuff like      addOne (x-1) = x
00:30:39 -!- ais523 has quit (Quit: sorry about my connection).
00:30:54 -!- ais523 has joined.
00:31:27 <Koen> so I guess it would involve a solver every time you try to pattern match
00:31:28 <Koen> just so you can write stuff like      addOne (x-1) = x
00:32:26 <Koen> 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
00:40:46 <b_jonas> 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,
00:43:14 <b_jonas> 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; }`
00:43:29 <b_jonas> no sorry, `f () = case [False] of { [f ()] -> True; _ -> False; }`
00:44:01 <Koen> oh, that's violent
00:44:56 <Koen> I was thinking more simples issues like      squareRoot (x^2) = x
00:45:01 <b_jonas> 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
00:45:20 <b_jonas> eh, we can solve a square root, that's a well-known problem
00:46:30 <b_jonas> sure, you might also give the match problems that are slow to solve, like [x * y] = some large composite number
00:46:45 <b_jonas> even ones that are well-defined but much slower to solve than factoring
00:46:45 <Koen> well yes but returning -3 or 3 for squareRoot 9 would both be correcrt
00:47:07 <b_jonas> yeah, sometimes there can be multiple matches
00:47:38 -!- sprout has quit (Ping timeout: 256 seconds).
00:48:28 <Koen> 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
00:48:54 <Koen> (I didn't ask the question, just stumbled upon it and thought that was something for #esolangs)
00:50:12 -!- ais523 has quit (Remote host closed the connection).
00:50:27 -!- ais523 has joined.
00:53:16 <b_jonas> 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
00:53:27 <b_jonas> because otherwise you get a paradox
00:53:44 <b_jonas> but it's not clear if you can do something like that into a purely functional language like Haskell
00:55:01 <ais523> <Agora's ruleset>      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.
00:55:53 <ais523> Agora decided that just because it's *possible* to resolve something to a truth value doesn't necessarily mean you *should*
00:56:27 <ais523> 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
00:56:42 <b_jonas> yeah, smullyan gives that lesson in one exercise
00:59:06 <b_jonas> in chapter 5 of "What is the name of this book?"
00:59:27 -!- sprout has joined.
01:09:44 <Koen> ah yes
01:10:04 <Koen> I read something like that like two days ago
01:12:26 <Koen> 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
01:14:04 <b_jonas> the lady and the tiger might also have that lesson somewhere. I don't remember everything in the books off-hand.
01:14:40 <Koen> i remember most of the riddles being extremely easy up to a point
01:14:45 <Koen> and then suddenly becoming impossible
01:15:36 <Koen> 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
01:16:25 <Koen> and then suddenly it's "a princess is exchanging secret codes with her suitor. can you break the code (and prove godel's theorem)?"
02:36:08 -!- ais523 has quit (Quit: quit).
03:48:25 -!- dutchkin has joined.
03:56:04 -!- Koen has quit (Quit: Leaving...).
04:19:18 <esolangs> [[Hrdfish]] M https://esolangs.org/w/index.php?diff=119738&oldid=119729 * PythonshellDebugwindow * (+18) /* See also */ Hrdfsh
04:20:01 <esolangs> [[Hrdfsh]] M https://esolangs.org/w/index.php?diff=119739&oldid=119721 * PythonshellDebugwindow * (+30) Hrdfish
04:24:08 <esolangs> [[Special:Log/move]] move  * PythonshellDebugwindow *  moved [[Meow]] to [[Meow (Martsadas)]]: Disambiguation
04:25:57 <esolangs> [[Meow]] M https://esolangs.org/w/index.php?diff=119742&oldid=119741 * PythonshellDebugwindow * (+89) Disambiguation page
04:28:33 <esolangs> [[Meowlang]] M https://esolangs.org/w/index.php?diff=119743&oldid=88072 * PythonshellDebugwindow * (+105) Distinguish confusion, add categories
04:29:06 <esolangs> [[Meow (Martsadas)]] M https://esolangs.org/w/index.php?diff=119744&oldid=119740 * PythonshellDebugwindow * (+2) Bold
04:30:15 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=119745&oldid=119734 * PythonshellDebugwindow * (+42) /* M */ add
04:31:40 <esolangs> [[Cripl]] M https://esolangs.org/w/index.php?diff=119746&oldid=104017 * PythonshellDebugwindow * (-8) Fix double redirect
04:32:15 <esolangs> [[UniLang]] M https://esolangs.org/w/index.php?diff=119747&oldid=118626 * PythonshellDebugwindow * (+2) Fix double redirect
04:33:13 <esolangs> [[Special:Log/newusers]] create  * Para *  New user account
04:34:13 <esolangs> [[CharCode]] M https://esolangs.org/w/index.php?diff=119748&oldid=119106 * PythonshellDebugwindow * (+79) Categories
04:35:44 <esolangs> [[ProjectEuler:24]] M https://esolangs.org/w/index.php?diff=119749&oldid=117002 * PythonshellDebugwindow * (+1) Fix double redirect
04:36:20 <esolangs> [[Esolang:Introduce yourself]]  https://esolangs.org/w/index.php?diff=119750&oldid=119552 * Para * (+182) 
04:36:56 <esolangs> [[Onlynumber]] M https://esolangs.org/w/index.php?diff=119751&oldid=116940 * PythonshellDebugwindow * (+1) Fix double redirect
04:37:52 <esolangs> [[Befunge-98]] M https://esolangs.org/w/index.php?diff=119752&oldid=107304 * PythonshellDebugwindow * (+3) Fix double redirect
04:40:58 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=119753&oldid=119745 * PythonshellDebugwindow * (+12) /* R */ add
04:45:57 <esolangs> [[Special:Log/newusers]] create  * Snacked *  New user account
04:47:33 <esolangs> [[Esolang:Introduce yourself]]  https://esolangs.org/w/index.php?diff=119754&oldid=119750 * Snacked * (+143) 
04:53:12 <esolangs> [[1 byte :5]] M https://esolangs.org/w/index.php?diff=119755&oldid=116554 * PythonshellDebugwindow * (+27) Stub, category
04:54:53 <esolangs> [[A1]] M https://esolangs.org/w/index.php?diff=119756&oldid=65385 * PythonshellDebugwindow * (+74) External resources, categories
05:24:52 -!- Sgeo_ has joined.
05:27:58 -!- Sgeo has quit (Ping timeout: 255 seconds).
05:53:51 -!- tromp has joined.
06:04:41 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
06:16:34 -!- dutchkin has quit (Ping timeout: 255 seconds).
06:19:09 -!- dutchkin has joined.
06:25:58 -!- tromp has joined.
07:23:49 -!- dutchkin has left (Konversation terminated!).
08:42:48 -!- cpressey has joined.
08:56:16 <cpressey> <b_jonas> "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
08:56:17 <cpressey> grant that the phrase "nothing wrong" was too sweeping. It was late.
08:57:50 <cpressey> Even "software engineering issues" is probably interpretable, maybe "programming-in-the-large" would be more specific
09:11:27 -!- Sgeo_ has quit (Read error: Connection reset by peer).
09:33:56 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
10:05:38 -!- Lord_of_Life_ has joined.
10:06:31 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
10:08:37 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
10:31:56 <esolangs> [[Template talk:Py]]  https://esolangs.org/w/index.php?diff=119757&oldid=119716 * None1 * (+198) You convert to wiki formatting locally first
10:50:33 -!- tromp has joined.
10:55:46 -!- Koen has joined.
11:21:52 <esolangs> [[Cutw]]  https://esolangs.org/w/index.php?diff=119758&oldid=110199 * None1 * (+28) 
11:22:02 <esolangs> [[Cutw]] M https://esolangs.org/w/index.php?diff=119759&oldid=119758 * None1 * (-1) /* See also= */
11:22:06 -!- FreeFull has quit.
11:22:23 <esolangs> [[Alphuck]]  https://esolangs.org/w/index.php?diff=119760&oldid=89425 * None1 * (+23) /* Hello, World! program */
11:23:34 <esolangs> [[Talk:Cutw]] N https://esolangs.org/w/index.php?oldid=119761 * None1 * (+160) Created page with "I came here from random page and wanted to make an interpreter for this esolang. --~~~~"
11:26:26 -!- cpressey has quit (Quit: Client closed).
11:28:08 <esolangs> [[Cutw]]  https://esolangs.org/w/index.php?diff=119762&oldid=119759 * None1 * (+2085) 
11:28:54 <esolangs> [[User:None1]]  https://esolangs.org/w/index.php?diff=119763&oldid=119724 * None1 * (+24) /* My Implementations */
11:30:06 <esolangs> [[Cutw]]  https://esolangs.org/w/index.php?diff=119764&oldid=119762 * None1 * (-4) /* JavaScript interpreter */
11:30:16 <APic> Moin
11:31:11 -!- cpressey has joined.
11:36:12 <cpressey> <b_jonas> 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"
11:39:04 <b_jonas> 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
11:40:01 <cpressey> C is statically typed but widely regarded as weakly typed because you can cast anything to anything
11:42:29 <int-e> also unions
11:42:35 <cpressey> 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.
11:43:36 <int-e> "my types are stronger than yours"
11:43:41 <cpressey> 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
11:44:59 <cpressey> 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
11:45:28 <int-e> there's also an expressiveness angle mixed into strength sometimes
11:46:19 <int-e> (there is a connection... the more expressive the type system, the less need you'll have for casts)
11:47:19 -!- MizMahem has quit (Ping timeout: 256 seconds).
11:48:06 <int-e> (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)
11:49:26 -!- Swyrl has quit (Ping timeout: 252 seconds).
11:49:31 <b_jonas> 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
11:49:58 <esolangs> [[Wymaewyha]] N https://esolangs.org/w/index.php?oldid=119765 * Yes * (+694) Created page with "Wymaewyha stands for When You Make An Esolang When Your Half Asleep <br> It is a brainfuck deteritave by [[User:Yes]] that was probably made when he was half asleep. <br> It is what it sounds like.  <h2>Commands</h2> <pre> wake up              start program go back to slee
11:50:14 <int-e> I'm sure memory safety means different things to different people too.
11:50:22 <esolangs> [[User:Yes]]  https://esolangs.org/w/index.php?diff=119766&oldid=107502 * Yes * (+19) 
11:50:51 <esolangs> [[User:Yes]]  https://esolangs.org/w/index.php?diff=119767&oldid=119766 * Yes * (+0) 
11:50:59 <int-e> And you don't need strong types for that, see Python. Or, hell, Lisp if we want ancient history.
11:52:59 -!- __monty__ has joined.
11:54:37 <esolangs> [[lang]]  https://esolangs.org/w/index.php?diff=119768&oldid=118778 * Yes * (+132) added [[English]] to intepeters
11:54:44 <b_jonas> yes. the two are different. that's what I was trying to say earlier.
11:54:55 <b_jonas> but apparently we thought of different things as strong typing.
11:55:34 -!- Swyrl has joined.
11:56:11 <esolangs> [[lang]]  https://esolangs.org/w/index.php?diff=119769&oldid=119768 * Yes * (+11) not sure why i named it specs in the first place so changed it to "possible outputs"
11:56:16 -!- MizMahem has joined.
12:00:18 <esolangs> [[lang]]  https://esolangs.org/w/index.php?diff=119770&oldid=119769 * Yes * (+161) added cpp to intepeters
12:02:40 <esolangs> [[lang]] M https://esolangs.org/w/index.php?diff=119771&oldid=119770 * Yes * (+2) /* C++ Interpreter */
12:03:10 <esolangs> [[Talk:lang]]  https://esolangs.org/w/index.php?diff=119772&oldid=114865 * Yes * (+105) /* EVEN SHORTER INTERPRETER */
12:08:47 <esolangs> [[User talk:Lyxal]]  https://esolangs.org/w/index.php?diff=119773&oldid=93338 * Yes * (+296) /* hey uh */ new section
12:15:35 <cpressey> 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 <x> and prevents <y>" when I'm talking about what the type system can and can't do
12:18:30 <cpressey> 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)
12:22:33 <cpressey> (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?)
12:24:19 <cpressey> I think you could *probably* implement the LCF architecture in untyped lambda calculus.
12:24:22 <cpressey> I am tempted to try.
12:24:51 <cpressey> I would need a refresher course in all that Church encoding stuff.
12:27:43 <int-e> 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.
12:28:04 <int-e> So, yes and no. As usual.
12:51:27 <tromp> has LCF been implemented in Haskell?
13:00:30 <int-e> Dunno, does Agda have an LCF style kernel?
13:01:52 <int-e> (It's a bit of a mismatch because it's primarily a programming language.)
13:04:25 <int-e> 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?
13:05:02 <tromp> in a sense, every typed expression (without undefined) in Haskell is already a theorem of sorts
13:05:37 -!- Koen has quit (Remote host closed the connection).
13:06:08 <int-e> Sure but AIUI a big part about LCF is managing theorems and exioms, without caring about their proofs.
13:12:08 <tromp> Wikipedia says: Basic idea
13:12:08 <tromp> 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
13:12:08 <tromp>  abstract data type implementation and the correctness of the ML compiler.
13:12:22 <tromp> that sounds quite possible to replicate in Haskell
13:12:48 <int-e> But you asked whether it was done, not whether it could be done.
13:18:40 <tromp> right. but i took your answer as suggesting  that it would be hard to manage thms/axioms in Haskell
13:21:08 <int-e> 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)
13:21:26 <b_jonas> I feel like untyped lambda calculus would be a singularly bad language to implement this sort of program
13:22:40 <esolangs> [[Talk:lang]] M https://esolangs.org/w/index.php?diff=119774&oldid=119772 * None1 * (+0) /* lyxal is a genius */
13:24:28 -!- Koen has joined.
13:34:59 <cpressey> 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
13:35:00 <cpressey> sequence of inference rules – namely theorems."
13:35:11 <cpressey> By "strict typechecking" he means "abstract data types".
13:35:32 <cpressey> You can implement the LCF architecture in any language with proper abstract data types.
13:36:55 <cpressey> 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.
13:36:58 <esolangs> [[lang]]  https://esolangs.org/w/index.php?diff=119775&oldid=119771 * None1 * (+61) /* Python 3 Interpeter */
13:37:54 <cpressey> 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...
13:43:16 <cpressey> I need to stop thinking about these things :/
13:43:21 -!- cpressey has quit (Quit: Client closed).
14:19:38 -!- tromp has quit (Ping timeout: 256 seconds).
14:49:38 -!- Koen has quit (Remote host closed the connection).
16:20:53 -!- razetime has joined.
16:21:15 -!- razetime has quit (Remote host closed the connection).
16:32:04 -!- FreeFull has joined.
16:41:17 <esolangs> [[Sd]] M https://esolangs.org/w/index.php?diff=119776&oldid=78851 * PythonshellDebugwindow * (+57) Categories
16:51:06 <esolangs> [[lang]] M https://esolangs.org/w/index.php?diff=119777&oldid=119775 * PythonshellDebugwindow * (+0) /* Python 3 Interpeter */ Fix
17:08:44 <esolangs> [[Wymaewyha]] M https://esolangs.org/w/index.php?diff=119778&oldid=119765 * PythonshellDebugwindow * (+130) Stub, wikify, add categories
17:12:23 <esolangs> [[Hi]] M https://esolangs.org/w/index.php?diff=119779&oldid=115244 * PythonshellDebugwindow * (+25) Category
18:23:53 <esolangs> [[Special:Log/newusers]] create  * SigmaOctantis *  New user account
18:30:22 <esolangs> [[Esolang:Introduce yourself]]  https://esolangs.org/w/index.php?diff=119780&oldid=119754 * SigmaOctantis * (+396) /* Introductions */
19:59:34 -!- V has quit (Ping timeout: 260 seconds).
20:03:33 -!- V has joined.
20:08:49 -!- V has quit (Ping timeout: 256 seconds).
20:11:50 -!- V has joined.
20:45:28 -!- ais523 has joined.
20:50:41 -!- __monty__ has quit (Quit: leaving).
21:16:11 <esolangs> [[Saturnus]] N https://esolangs.org/w/index.php?oldid=119781 * SigmaOctantis * (+2703) Created 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
21:21:15 <esolangs> [[Saturnus]]  https://esolangs.org/w/index.php?diff=119782&oldid=119781 * SigmaOctantis * (+35) 
22:56:46 <esolangs> [[Saturnus]] M https://esolangs.org/w/index.php?diff=119783&oldid=119782 * PythonshellDebugwindow * (+73) Categories
22:59:42 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=119784&oldid=119753 * PythonshellDebugwindow * (+51) /* S */ add
23:04:37 <esolangs> [[IDKHIW]] M https://esolangs.org/w/index.php?diff=119785&oldid=119409 * PythonshellDebugwindow * (+33) Stub, category
23:14:26 -!- Sgeo has joined.
23:58:49 <esolangs> [[Cellular automaton]] M https://esolangs.org/w/index.php?diff=119786&oldid=78704 * PythonshellDebugwindow * (+34) /* See also */ Category