Oh! thanks for sharing haha~ I hadn’t logged in here in a while but I figure it might have spawned some discussion here (and hopefully my characterisation wasn’t too unflattering of OCaml, just venting some shortcomings I’ve felt over time).
Let me respond to some of the points!
Yeah, that’s a fair point, I think in hindsight, I probably didn’t articulate my point well here. I guess the more broader point is OCaml is wysiwyg and there are fewer surprises. The example I gave was about optimizations as I felt that was easiest to explain, though in my day to day programming what I’m more interested in is the amount of work the compiler is willing to do to infer things
Namely, a huge gamechanger for me in just day to day lean code is how it does type based disambiguation (with some conflation between types and namespaces).
g.neigboursOf elt
|>.filter (not $ elts.contains ·)
|>.filter (not $ seen.contains ·)
|> queue.append
In particular, in the above code, g.neigboursOf disambiguates to Graph.neighboursOf (based on the fact that g: Graph), neighboursOf: Graph → Node → List Node, so the subsequent .filters are disambiguated to List.filter.
Another cool thing that I enjoyed in Lean was that it effectively “solves” the argument parameter convention problem — referring here to the way that different libraries in the OCaml ecosystem have different conventions for where the t parameter should go in a function (should it be List.filter: ‘a list → (‘a → bool) → ‘a list or List.filter: (‘a → bool) → ‘a list → ‘a list?). Some libraries choose to place the “self” type last, so these functions can be composed easier, others adhere to a convention of that the parameter must be first, or some use labels.
In lean (x : List A).filter disambiguates to supplying x as the first argument of the matching type, so filter could very well be typed List.filter: (A → Bool) → List A → List A, but the compiler would just work it out.
(minor note for clarification: I’m not saying these are features that would be a good fit for OCaml, it’s just this was an annoyance for me, and OCaml largely adheres to a WYSIWYG with minimal compiler magic, which means that these kinds of niceties are largely out of scope).
mhhm yep yep, mapi would work better. I realise my narrative around point 1 was worse than I thought, the exposition about the allocations was primarily to illustrate how an OCaml developer can reason about their code and optimise it accordingly. Rereading it, I did focus way too much on the optimisations, when what I really wanted to focus on was like WYSIWYG.
Yep, indeed, that was my mistake! Someone pointed it out on reddit and I need to get round to fixing that haha.
Mhhm yep that’s fair. I guess the primary point I was making was that the rate at which additions are made is pretty slow, and I think in an earlier draft I had a comment about how these multiple iterations involved deliberating on different performance considerations and a path for bridging between safety and efficiency etc. but I think they got cut.
It is developing actively certainly, but as a developer who was a) active in the community, and b) would have been keen to contribute to the language, the ecosystem is substantially harder to make a useful contribution to in comparsion to lean. most of the interesting additions to the library occur primarily in offline meetups it seems at INRIA/JaneStreet, and are lead by teams of one or two people. Consider modular explicits? is there anything that a developer joining the community at this point could actually do to help that become part of the language? OXcaml is exciting, but another Jane street contribution from within their hallowed halls. In contrast, as an “outsider” the Lean ecosystem and compiler are a lot more approachable, the discussions about internal details occur in the public and it’ seems feasible for an external contributor to help. From when I was more interested in contributing, I distinctly recall several threads of people excited about modular implicits, interested in contributing somehow only to be dissuaded by this requires substantial internal knowledge of the type checker, probably there are one or two people who can contribute, you’ll have to wait for them to make some more changes. (Certainly the expertise required to contribute to the Lean compiler might be the same, but the discussions are public, the Lean FRO holds public office hours regarding compiler development and language updates) .Progress is certainly going on, but not something that the average end user can really make any contribution to.
I’m curious if you’ve tried using other macro-systems from languages such as Racket? I’m not saying macros are inherently super complex pieces of software to write, but they can be challenging to reason about especially in the interplay between meta and runtime evaluation, syntax hygiene and so forth. The fact that OCaml macros require so much boilerplate means that you have to juggle all of that complexity alongside deciphering what kinds of syntax transformation you are implementing. This is all not even to mention how much this complicates maintaining or updating ppxs over time.
Things like syntax hygiene have been developed over a long periods of time and have a proven track record in Lisps of substantially reducing such bugs. You certainly can write macros in OCaml, but that doesn’t mean that it’s easy, nor easy to maintain. (This discussion feels like it parallels telling a C developer that memory safe languages are helpful, and them responding, the difficulty is mostly managing pointers but malloc/free is sufficient).
OCaml also doesn’t afaik allow type-based macro expansions as PPXs all run before the typechecker is called. I remember one or two attempts to allow type information in ppx but these were largely hacks.