02:25 <pgiarrusso> contificate: my impression is that dh` was never talking about J, but only about W

02:46 <discocaml> <contificate> just goes to show how error prone W is

02:54 <pgiarrusso> What about backtracking mutations from J?

03:00 <pgiarrusso> I'm sure it can be done, since it happens in Rocq and Scalac at least (not for J, but still for algorithms using unification)

03:03 <companion_cube> push type variable bindings onto a undo stack

03:43 <discocaml> <uberpyro181> the substitution is applied to the context before the next unification problem (resp. type variables are updated in place)

03:43 <discocaml> <uberpyro181> so once you apply some `[x1 |-> f(x2)]`, `x1` is gone everywhere, forever

03:44 <companion_cube> you might write that on paper, but it's not a good implementation

03:44 <discocaml> <uberpyro181> if you did have successive substitutions like `[x |-> y][y |-> x]`, i mean this works out to `[y |-> y]`

03:45 <discocaml> <uberpyro181> you can't really create cycles this way

03:45 <discocaml> <uberpyro181> i agree W is too slow for real implementations and that J is the starting point for anyone looking to implement an HM system

03:46 <discocaml> <uberpyro181> W does have uses when it comes to some niche extensions. e.g. if your system lacks principal types and you want to do a tree search over typings, you want purity

03:46 <discocaml> <uberpyro181> or if you go beyond syntactic unification / free type constructors and into algebra, the trick doesn't save as much time

03:48 <discocaml> <uberpyro181> or if you go beyond syntactic unification / free type constructors and into algebra, the trick doesn't save as much time (because you need to work in terms of canonical forms)

03:52 <discocaml> <uberpyro181> for incremental typechecking, i'm not sure how much it matters, given that fully generalized types don't mutate

03:56 <discocaml> <uberpyro181> or if you go beyond syntactic unification / free type constructors and into algebra, the trick doesn't save as much time (because you need to work in terms of canonical forms)

03:56 <discocaml> <uberpyro181> (you can can mutable references to manage the context efficiently, but union-find doesn't help.)

04:10 <discocaml> <uberpyro181> if you did have successive substitutions like `[x |-> y][y |-> x]`, i mean this works out to `[x |-> y, y |-> y]`

10:57 <companion_cube> You really shouldn't bind y to y

10:57 <companion_cube> In all the unification/substitution algorithms I've implemented it leads to an infinite loop

11:06 <discocaml> <uberpyro181> i guess implementation-wise there are weird edgecases like that, but i was just trying to make a point

11:06 <discocaml> <uberpyro181> i guess it's moot anyway

11:07 <discocaml> <uberpyro181> i'll add one thing here because i didn't actually make a point

11:08 <discocaml> <uberpyro181> in my own experience, which is experimenting with weird type system extensions, the big pain point with mutable variables is that they can't be used as keys for maps and sets

11:08 <discocaml> <uberpyro181> because they can mutate which messes up tree invariants and changes the hash, obviously

11:09 <discocaml> <uberpyro181> this is really inconvenient for some type level features, the most extereme cases are like intersection/union types or other sorts of boolean types

11:09 <discocaml> <uberpyro181> because the polynomial normal form maps set of variables to their coefficients, but the variables are un-key-able

11:10 <discocaml> <uberpyro181> i don't have much experience but i'm guessing annoyances like this also crop up with other advanced type system features

11:11 <discocaml> <uberpyro181> the HM type system finds itself in a local optima in like 20 different dimensions simultaneously, between ease of implementation, performance and mutable impelmentation, sizes of types, etc

11:12 <discocaml> <uberpyro181> the age old story is that things sort of degrade when you take steps in any direction, and that breaks what works well in traditional circumstances

13:33 <discocaml> <contificate> it's just neat, is what it is

13:33 <discocaml> <contificate> if OCaml disappeared from reality, can see myself going to SML, y'know

13:33 <discocaml> <contificate> but if Haskell disappeared, nobody's going to Miranda

13:34 <discocaml> <contificate> my lukewarm take is actually that the type system is not overly important, nobody would use these languages if they lacked pattern matching

15:50 <dh`> how else would you unpack sums? generate an is_foo and unpack_foo function for each constructor?

15:51 <dh`> (is_foo x = match x with Foo _ -> true | _ -> false; unpack_foo x = match x with Foo x' -> x' | _ -> assert false)

15:52 <dh`> without sums at all, you might as well use pascal

16:43 <discocaml> <gooby_diatonic> Ig use tagged unions manually, checking the tags and such

16:53 <qu1j0t3> something that Pascal _does_ have

19:38 <avidseeker> I'm trying to install ocaml-lsp-server and I get a compilation error in topkg

19:38 <avidseeker> https://paste.debian.net/plain/1366943

19:39 <avidseeker> the probem seems to be in Exception: Fl_package_base.No_such_package ("findlib", "").

22:34 <discocaml> <diligentclerk> I'm not familiar with Miranda. From the context it seems like you're saying that Miranda's type system/type inference is much less convenient than Haskell's?

22:35 <discocaml> <diligentclerk> Oh, I looked up Miranda and I see it appears not to have algebraic data types, interesting.

22:39 <discocaml> <Kali> miranda is haskell's predecessor and is essentially just haskell with less advanced type features

22:40 <discocaml> <Kali> contificate is saying that if haskell didn't exist then nobody would go to miranda because there's nothing particularly interesting about it when you have sml, ocaml, etc.

22:42 <discocaml> <Kali> it does, where are you seeing this

22:44 <discocaml> <diligentclerk> Never mind, I misread the Wikipedia page. I noticed this sentence saying:

22:44 <discocaml> <diligentclerk> > Miranda's basic data types are char, num and bool. A character string is simply a list of char, while num is silently converted between two underlying forms: arbitrary-precision integers (a.k.a. bignums) by default, and regular floating point values as required.

22:44 <discocaml> <diligentclerk>

22:44 <discocaml> <diligentclerk> and I just assumed that the language was primarily based on lists of these.