01:07 <eltonpinto> https://github.com/ocaml/ocaml/pull/10195 found this PR to be interesting

07:50 <d_bot> <ostera> is there any reason whatsoever that a match over polymorphic variants should behave different than one over regular variants?

07:50 <d_bot> <ostera>

07:50 <d_bot> <ostera> eg, are these two semantically equivalent?

07:50 <d_bot> <ostera>

07:50 <d_bot> <ostera> ```ocaml

07:50 <d_bot> <ostera> type a = A | B

07:50 <d_bot> <ostera> match (x : a) with

07:50 <d_bot> <ostera> | A -> ()

07:50 <d_bot> <ostera> | B -> ()

07:50 <d_bot> <ostera>

07:50 <d_bot> <ostera> type b = [ | `A | `B ]

07:50 <d_bot> <ostera> match (y : b) with

07:50 <d_bot> <ostera> | `A -> ()

07:50 <d_bot> <ostera> | `B -> ()

07:50 <d_bot> <ostera> ```

07:51 <d_bot> <ostera> i'm asking because i found out that in ReScript polymorphic variants on an exhaustive switch compile to a cascade of if-else's that has a default case

08:08 <d_bot> <darrenldl> any long term data storage enthusiast or lossy network link user here? i recently released ocaml-lt-code (forward error correction thingy), and have been exploring ways to apply it concretely

08:15 <d_bot> <octachron> @ostera : it depends on what you mean by semantics: the memory representation of polymorphic variants is not the same as the one for regular variants (typically the equivalent of tags is much more sparse on the polymorphic variants side). This has some consequences on the compilation of pattern matchings. If you are asking if your second match should be considered exhaustive, the answer is yes.

08:34 <d_bot> <ostera> excellent, that's what i thought

08:34 <d_bot> <ostera> thanks @octachron

08:51 <d_bot> <octachron> Note that you can check the behavior of the pattern matching compiler with `-dlambda` . In your example, the `match` is seen as constant and there is no conditionals, and tweaking it to make the branches non-constant, there is still only one `if`.

10:34 <d_bot> <Kakadu> Do you know if https://download.ocamlcore.org/ocaml-metrics/ has been resurrected in opam? I foun donly mirage's metrics but it look like some runtime metrics and not code quality metrics...

11:31 <d_bot> <Competitive Complications> hi

11:31 <d_bot> <Competitive Complications> where can i find about the typing rules for recursive modules?

11:32 <d_bot> <Competitive Complications> I haven't found them on https://caml.inria.fr/pub/docs/u3-ocaml/ocaml.pdf nor https://ocaml.org/manual/manual024.html

11:53 <d_bot> <octachron> Do you have a more precise question? Otherwise, you would have to dive in research articles.

11:55 <d_bot> <Competitive Complications> @octachron

11:55 <d_bot> <Competitive Complications> On page 36 of http://gallium.inria.fr/~remy/mpri/2013/cours.pdf, I have the typing rule for recursive functions

11:55 <d_bot> <Competitive Complications> I'm interested in typing rules for more generic things. Be it recursive values (which should just be `(a -> a) -> a`, recursive modules (???) or recursive dependent values

12:06 <d_bot> <octachron> Then you have to refer to research articles, the question is not yet settled. The implementation in OCaml is essentially a pragmatic prototype.

12:08 <d_bot> <octachron> https://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf describes the OCaml implementation.

12:08 <d_bot> <Competitive Complications> That's ok with me. If you have good papers in mind, especially recent ones, I'd be glad. In the meanwhile, I'm reading https://people.mpi-sws.org/~dreyer/papers/recmod/main-short.pdf

12:08 <d_bot> <Competitive Complications> If you know of one that tries to tackle recursive dependent values directly, that would be even better

12:12 <d_bot> <octachron> Sorry, I am not familiar with the literature and I don't know the good entry points.

12:13 <d_bot> <Competitive Complications> No problem 🙂

12:29 <d_bot> <Competitive Complications> It'd be nice to have a #brainstorm channel to just share thoughts about this kind of things without spamming everyone

12:39 <d_bot> <Drup> for recursion × dependent values, there are many approaches, but it's generally due to termination consideration rather than just the dependency, which doesn't impose all that many issues

12:40 <d_bot> <Drup> recursive modules are a mess though, but it's a bit more complicated than just because of dependent types, because it adds abstraction in the mix

12:44 <d_bot> <Drup> Are you interested by a specific use or just "all the recursive things" ?

12:53 <d_bot> <Competitive Complications> I want to explore what currently exists and form my opinion. Ideally, I just want to have a "dependently typed system" (quotes, because I don't want a Curry-Howard implementation, am ok with Type:Type, don't need type checking to be decidable and am thus ok with unbounded recursion) and row polymorphism. and I'm thinking that if I had a nice understanding of recursion for dependent types, I would not need any sp

12:53 <d_bot> <Competitive Complications> i also don't mind if there is no memory representation for the entire lang or if the entire lang of typed terms is not compilable as long as there is a semantically meaningful pass that can be applied after typing and yields nice enough errors

12:54 <d_bot> <Competitive Complications> isn't abstraction subsumed by existential types in recursive types?

12:54 <d_bot> <Drup> it's "encodable in", not "subsumed"

12:55 <d_bot> <Competitive Complications> i see

12:55 <d_bot> <Drup> (and it's not terribly nice to use, imho)

12:55 <d_bot> <Drup> The sugar is important 🙂

12:56 <d_bot> <Competitive Complications> (do you feel it's that way because of a lack of sugar/tool/support or because of inherent limitations of the encoding?)

12:56 <d_bot> <Competitive Complications> agreed, but not the layer i'm working right now

12:56 <d_bot> <Drup> sure

12:57 <d_bot> <Competitive Complications> but yeah, given this, i should be ok with any approach to recursion x dependent values that you have in mind

12:57 <d_bot> <Drup> in any case, I'm not sure I have a specific reference. Imho, if you only want a calculus and you don't care about being impredicative, you can go wild with recursion, nothing matters 🙂

12:58 <d_bot> <Competitive Complications> agreed, but even then, i haven't seen anything there

12:59 <d_bot> <Competitive Complications> if you have examples of systems "going wild", I'm all for it

13:00 <d_bot> <Competitive Complications> like, OCaml goes wild, but hasn't gone dependent types

13:00 <d_bot> <Drup> OCaml doesn't goes wild at all, there are lot's of constraints wrt recursive things

13:00 <d_bot> <Drup> by "go wild" i mean "just do the basic unrestricted thing"

13:01 <d_bot> <Drup> as I said, if you care neither about compilation nor decidability, it doesn't matter, you don't need to do anything special, that's why noone talks about it.

13:02 <d_bot> <Competitive Complications> I am looking for what this is

13:02 <d_bot> <Competitive Complications> the basic fixpoint constructor has type `(a -> a) -> a`, I'm not sure how you translate that type into dependent types. `(x : A(??) -> A(x)) -> A(??)`

13:03 <d_bot> <Drup> Ah, from that. You probably need some indexed stuff, I'm not familiar with those calculus

13:03 <d_bot> <Competitive Complications> you can still interpret, typecheck, and compile a sub-part. but i don't really want to make a case for it. if you have examples of restrictions where recursion x dependent values are studied, I'm still very interested. I'd expect to understand more

13:03 <d_bot> <Drup> you can look at size types for the decidability aspect

13:04 <d_bot> <Drup> https://www.cambridge.org/core/journals/journal-of-functional-programming/article/wellfounded-recursion-with-copatterns-and-sized-types/39794AEA4D0F5003C8E9F88E564DA8DD

13:05 <d_bot> <Drup> (just an exemple, there is a rich literature)

13:06 <d_bot> <Drup> what you are looking for is probably on the more theoretical side, but you can look at the references starting from there

13:09 <d_bot> <Competitive Complications> if you have a bunch of examples, so that if one doesn't look good, i can move to another one, that would be great

13:09 <d_bot> <Competitive Complications> else, I will just check at the references from your link

13:11 <d_bot> <Drup> for modules, the most recent work is probably https://dl.acm.org/doi/10.1145/2076021.2048141, but it's very different from what you want, I think

13:19 <d_bot> <Alistair> How does typing for optional arguments w/ defaults work? Since I expect `fun ?l:(pat = e) -> ...` gets desugared too: ```ocaml

13:19 <d_bot> <Alistair> fun ?l:x -> let pat = match x with

13:19 <d_bot> <Alistair> | Some x -> x

13:19 <d_bot> <Alistair> | None -> e

13:19 <d_bot> <Alistair> in ...```

13:22 <d_bot> <Competitive Complications> thanks 🙂

15:30 <Corbin> Is there a good recipe for translating Rust to OCaml? I'm trying to decide how to structure the struct-like types for a library, and I'm not sure if I should translate a traits-heavy approach to functors or just inline a bunch of stuff.

15:31 <Corbin> The library's https://github.com/egraphs-good/egg FWIW. I've implemented this data structure before, but I used struct-of-arrays techniques to break up the structs, and I was able to cheat a bunch because it was an untyped environment.

15:33 <Corbin> TBH I'm inching closer and closer to just writing some Rust, wrapping the library, and giving it a friendly little JSON face. I don't like Rust but I like confusing hashtable logic even less.

16:43 <companion_cube> Corbin: struct of arrays in ocaml works, but it's very tedious

16:44 <companion_cube> Corbin: im actually interested in Egg, I have a congruence closure in OCaml if you're willing to look, and the extensibility aspect is on my todolist

16:45 <Corbin> companion_cube: I'm certainly interested in what others have built, but we both know that you know OCaml way better than me.

16:45 <companion_cube> What does that change? :)

16:45 <companion_cube> What do you want to use Egg for?

16:45 <Corbin> Well, I don't want to just yoink your code, but I also don't think I'll have constructive feedback from code review.

16:46 <Corbin> I'm writing programming languages. I prototyped Egg already, and wrote high-level operations on my high-level language AST. But it was not great, mostly because alpha-equivalence is a pain and beta-reduction is non-trivial.

16:47 <companion_cube> (my congruence closure isn't struct of array ified yet)

16:47 <companion_cube> Ah, so equally the use case of the paper

16:47 <companion_cube> Have you considered bindlib? Or DB indices?

16:47 <Corbin> My current attempt is no names at all, just categorical combinators. I'll eventually implement the high-level language by classical reduction techniques, but I'm still working on low-level parts.

16:47 <companion_cube> Hmmm, are these the same as SKIBC?

16:47 <Corbin> This fixes the alpha-equivalence problem, because no names, and it makes beta-reduction simple enough to be a standard e-matching rule. So now I can go full egg.

16:48 <Corbin> No, these are id, curry, apply, pair, dup, that sort of thing.

16:49 <Corbin> SKI reduction's really cool, but also really hard to safely put into an egg-ish form because S is so unrelentingly explosive.

16:50 <Anarchos> Corbin sure, S is a distributive operator

16:53 <Corbin> TIL bindlib. This looks super-useful. It's like ABTs or Haskell's "bound" library. I don't want to do this sort of thing ever again, but if I have to, I'll make sure to remember bindlib.

16:53 <companion_cube> Corbin: oh interesting

16:53 <companion_cube> Does this correspond to a stack machine? Or like exponential categories or whatever?

16:54 <Corbin> It corresponds to Cartesian closed categories. It was at this point that I realized I was on the same mountain as Curien in the 1980s, so I went back and read a bunch of papers, and I'm here because OCaml's got the best implementation of that sort of machine.

16:54 <companion_cube> Yeah bindlib is HOAS I think

16:55 <companion_cube> Ah, fun.

16:55 <Corbin> Elliott's got a paper which goes in the other direction, and shows that we don't need names if we have the right combinators: http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf

16:55 <Corbin> So basically my goal is now: Take high-level language, desugar, remove names and get categorical combinators in a fancy category. Then, make the category less fancy by interpreting it with a stack of monad transformers (there's another two Elliott papers on this, IIRC)

16:56 <companion_cube> My problem is that I could never grasp categories :)

16:56 <companion_cube> Egg is closer to my level of skill

16:57 <Corbin> Egg's core rebuilding algorithm turned me to mush. When I rewrote it in Monte, I changed that loop entirely so that it was iterative instead of recursive.

16:57 <Corbin> Actually, I changed something which I wish Egg would change too. The Rust version is unsafe in that it is only correct if the user remembers to manually rebuild the e-graph in-between doing matches.

16:58 <Corbin> My API takes a *list* of pairs of e-classes to unify, and automatically rebuilds after iteratively working through the list. So the user can't possibly injure themselves and misoptimize.

16:59 <Anarchos> companion_cube what are the troubles with categories ?

17:00 <Corbin> https://github.com/monte-language/typhon/blob/master/mast/lib/egg.mt.md#core sorry for the orange language.

17:00 <companion_cube> Anarchos: gets too abstract for me too quickly

17:00 <Anarchos> companion_cube i must admit i strugle to understand yoneda's lemma and all the fuz around representable functors....

17:01 <Anarchos> Corbin orange is the new black ;)