Why Lean 4 replaced OCaml as my Primary Language

Ecosystem
, , ,
1

Why Lean 4 replaced OCaml as my Primary Language

7 Likes
2

An interesting critical appraisal from our own @Gopiandcode

I found it interesting reading! It is also a good reminder for me to take another look Lean :slight_smile:

I do have a few critical remarks on the critique to offer:

  1. I don’t understand the real thrust of “Issue no. 1” in Lean’s favour. Imperative procedures are compared between OCaml and lean – but for some reason it does not give a strictly equivalent bit of OCaml code? The critique of OCaml seems to be that optimizations on functional code are not as aggressive as they might be (for the sake of maintaining predictability), but then the lean is also apparently not optimizing. Is the advantage for Lean meant to be that it ultimately desugars to pure code that could in theory be highly optimized?

  2. The OCaml code in “Issue no. 1” seems like could be easily improved to give a more favorable view of the mix of imperative and functional approaches OCaml offers. E.g., unless I am mistaken, inc_sum could be nicely implemented with an even smaller memory footprint as

    let incr_sum (ls : int list): int list * int =
  let sum = ref 0 in
  List.mapi (fun vl i -> sum := !sum + vl; vl + i) ls, !sum

  3. Just a small correction, but I think the Lean function is not actually implementing the intended algorithm, since it is counting the number of elements, not summing them.

  4. The history of the introduction of dynamic arrays seems to be mischaracterized. The text makes it sound like 2 PRs were bogged down in naming quibbles, but the history of the second PR shows that it was actually core implementation questions related to perf that were under discussion, and that the 3rd PR which landed the feature was actually taken up as a continuation of the 2nd, learning from what was discovered from it. This correction does not undercut the key point that the Stdlib and compiler grow relatively conservatively, but IMO it is a mischaracterization nonetheless.

  5. IMO, it would give the critique more balance toa cknowledge the many substantive features which have landed over the last few years. Since 2019, we have gained, at least

    • binding operators
    • user-defined indexing operators
    • risc-v backend
    • TMC transformations
    • multicore
    • effect systems
    • a heap of additions to the stlib
    • not to mention many other nice incremental improvements

    I guess it is a somewhat a matter of personal opinion whether or not this a good velocity for an ecosystem of our size that also has strong commitments to maintaining backwards compatibility. But without mentioning all that has been achieved, I think people outside the ecosystem would get the false impression from this post that the core language is not developing actively. (Note, I have not even mentioned the advent of oxcaml, which goes unmentioned.)

IMO, none of these quibbles detract from the overall value of the post as a mirror for us to use within the ecosystem. A thing which is not at all addressed in the post – to my surprise! – is what advantages (or challenges) Lean gains by offering a fully-dependant typing discipline.

13 Likes
3

I think the main thing to keep in mind is the context of the author:

if you’re a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl!…Plus, as an extra benefit, you might even end up contributing to state of the art mathematics research~

That’s cool, but I actually don’t want or need to do those things. I’m a developer who ultimately wants to use a very well-designed language in my day job as a software developer, while making it as boring, predictable, pedestrian, and productivity-friendly as possible. I don’t want to have to explain dependent types, macro syntaxes, and so on to my co-workers. I want named and optional arguments!

My takeaway is that no language is perfect for everyone, and that’s cool.

11 Likes
4

Issue number 1 is one of the reasons Xavier Leroy cited for OCaml’s success

What made that possible? Not just fancy types and nice modules – even though systems programmers value type safety and modularity highly – but also basic properties of OCaml:

  • a language with a simple cost model, where it’s easy to track how much time and how much space is used;

  • a compiler that produces efficient code that looks like the source code, with only predictable optimizations;

  • a low-latency garbage collector, usable for soft real-time applications.

    To us PL folks, this doesn’t sound like much. Good luck getting a paper accepted at POPL or PLDI based on these ideas! Yet, that’s crucial to open the way to many exciting applications.

10 Likes
5

I’d like to add one more thing:

the language itself makes up for this with a) more memory reuse (thanks to it’s clever reference-counting with memory reuse algorithm Perceus)

Note that the Perceus creators actually ported OCaml to run on it and found that even in the simplified ideal test cases, it had a hard time beating garbage-collected OCaml in memory usage! https://www.microsoft.com/en-us/research/wp-content/uploads/2023/09/ocamlrc.pdf

Since Perceus is garbage free, the Perceus backend uses less memory than the OCaml garbage collector on all benchmarks, with a 40%+ reduction in the cfold and deriv programs. However, for the other three benchmarks the working set is suprisingly close which is a testament to how well the OCaml GC is able to manage its memory.

5 Likes
6

The usual argument I hear against reference counting for functional languages come from persistent data structures like balanced trees.

With GC, inserting into an Okasaki-style red-black tree is O(log n) because the algorithm only goes down a single path in the tree.

With reference counting, it seems that insertion into a persistent data structure would have to visit every node in the tree (to increment the refcount for each node) and the algorithm would degenerate to O(n).

It doesn’t look like those benchmarks link corroborate this argument though, or else I would expect performance to be worse. I would be interested in seeing how they managed to overcome this limitation.

Edit: They seem to point out in the paper (although I only skimmed and don’t see how it works).

Moreover, if we use the tree persistently [33], and the tree is shared or has shared parts, the algorithm adapts to copying exactly the shared spine of the tree (and no more), while still rebalancing in place for any unshared parts

1 Like
7

I’d also list OCaml as my main programming language. Over the past few weeks I’ve been using Lean 4 for formal proofs.

Regarding issue no. 1: today, generative AIs (ChatGPT, Claude, etc.) are also consumers of code. They’re not yet good at distinguishing which features or syntax belong to one version versus another. Because the official Lean 4 docs have relatively few end-to-end examples, I rely on these models quite a bit. However, even the strongest models rarely produce valid Lean 4; they often mix in Lean 3 syntax/features. That’s a rough experience when you’re learning a new language.

With OCaml + a generative AI, I do sometimes see hallucinated functions, but the syntax is usually valid. When the types are wrong, the compiler’s messages are often enough for the model (or me) to fix the program. That workflow breaks down when the syntax itself is wrong.

In Lean, a syntax error often reports only that a token/character was unexpected, without making the root cause clear. This is compounded by Lean 4’s macro-based syntax-extension system: the model frequently makes incorrect assumptions about available notations. So even though model performance depends heavily on the size/coverage of its training data (likely larger for OCaml than for Lean), if a language’s feature set changes frequently or has breaking changes, the user experience with a generative AI gets much worse.

8

Mmmm ….. my memory is fading away, but ….. (thinking back to functional implementations of AVL trees) suppose that you retain a pointer to the “before insertion” and “after insertion” roots. Then there will remain large subtrees that will get an incremented refcount, but only at the roots of those subtrees, right? all the children of those roots remain unchanged, no? The refcount records the number of -immediate- pointers into a block, right? Not ancestors’ pointers. So the spine of the update changes, as do the refcounts of the nodes pointed-to by the spine. And nothing more. At least, that’s how I remember it. And I might be fading …..

2 Likes
9

I keep hearing people saying that Lean is surprising fast, and that may very well be the case (it benefits from nice research in programming language optimizations), but I have not seen clear benchmarks published to compare it with other languages (for example from the Computer Languages Benchmark Game), or I haven’t heard of efforts to port macro-benchmarks to compare with other programming languages. Do you know of benchmark sets that provide some actual data on the performance comparison between Lean and other programming languages?

4 Likes
10

I hadn’t considered that technique, but it sounds like it makes a lot of sense actually. Thanks.

This makes me interested in seeing how other functional data structures not based on trees (like list-zippers) perform under Lean. I’ll probably go off and implement one to see.

11

This paired with the complexity of manipulating the syntax tree means that it is extremely difficult to make any non-trivial macro extension to the language.

This sounds very exaggerated to me. Its not exactly easy, but I think the difficulty is mainly all the boilerplate you need to setup, and the knowledge of the AST you need to acquire, so to me its more difficult to do simple modifications, relative to their complexity.

12

To be fair, that is pretty difficult and involves a lot of head-scratching. At least it did for me. Part of the problem is that ppxlib provides s bunch of smart constructor functions that you’re supposed to use to build the AST, so you need to learn this rather surface area API to be able to start generating the items you want. It’s a very steep learning curve.

its more difficult to do simple modifications

I think most use cases need simple modifications, so we are front-loading the learning curve for almost all PPX use cases.

2 Likes
13

I think most use cases need simple modifications, so we are front-loading the learning curve for almost all PPX use cases.

Agreed ! But the article said the complex stuff was difficult. In my opinion, some sort of a macro system would be a nice addition, to provide something less powerful but easier to use. If you need to full power, then you have to learn the difficult stuff.

14

I think there is metaquot which is an easier way to generate AST nodes. But the OP said ‘non-trivial’ stuff is difficult, not ‘complex’ things. Eg metaquot is quite limited in what it can do, like it can’t take a string as an argument dynamically amd generate an AST node using that. I agree difficult things require work, but this kind of thing should not be that difficult…

15

First, I’ll just state up-front that I’m not trying to convince anybody to use Camlp5. But:

It is -completely- straightforward (albeit tedious) to extend the OCaml official grammar & AST in order to support antiquotations in almost all AST-relevant positions. You can then use that menhir-generated parser to write “metaquotations” for expressions and patterns, in a pretty simple way. As a bonus, you get portability of your macro-processor code between versions of the OCaml AST, b/c while the AST changes, the surface syntax changes much, much, much more slowly.

As a demonstration of this, I wrote pa_ppx_parsetree – antiquotation support for every version of the OCaml AST in the range [4.10..5.2]. I didn’t do 5.3 only b/c I’ve been lazy: I should do it.

The code in that project is a demonstration that it is actually straightforward (again, but VERY TEDIOUS) to port forward what amounts to full support for antiquotations in the (admittedly very large) OCaml grammar, from version-to-version of the OCaml AST, as it evolves.

I should add the caveat that yes, I used Camlp5 to -write- this preprocessor. But Camlp5 isn’t used to do any of the parsing (it’s a Menhir parser) nor the conversion to the OCaml AST (it’s a Camlp5-generated tree-walker, generated by pa_ppx_q_ast), and hence, you could imagine removing Camlp5 support by rewriting each bit of functionality from Camlp5 that is used in implementing pa_ppx_parsetree.

As a demonstration of this functionality, I took ppx_jsobject_conv and replaced all (or most – It’s been a while since I hacked on it – I’ve been lazy like I said) of the AST manipulation with meta-quotation expanded by pa_ppx_parsetree: here’s the project:

and here’s the parsetree project:

as well as the q_ast project:

3 Likes
16

After I noticed the suggestion of using quoted strings with extension nodes to embed foreign syntax in the manual, I tried it while working through John Harrison’s Handbook of Practical Logic and Automated Reasoning, and was actually pleasantly surprised by how simple ppxlib.metaquot made the process.

You can see the fruits of my experiments here, complete with (restricted) antiquotation using $, which just required adding a metavariable variant to my syntax and updating my parser to handle it.

The ppx itself (based on a Menhir parser):

2 Likes
17

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.

7 Likes
18

Case in point:

Now, granted, modular implicits are a complex feature that requires substantial expertise to be qualified to contribute to, but considering even dynamic arrays took 6 years, it sometimes feels like any change to the OCaml language requires this level of investment.

And as mentioned in the post, a language being slow in its evolution isn’t a huge problem for me in itself, provided there are reasonable means for developers to work around these limitations, namely, suitable metaprogramming and build customisability, but in both regards here OCaml’s offerings are somewhat lacklustre (metaprogramming being ppxlib, and build customisability being dune and it’s inflexibility).

As a case in point, recently while trying to write some FFI bindings for Lean to the Godot Game engine, over maybe 30/40 minutes of hacking I was able to implement my own incomplete and adhoc in-house ctypes implementation specialised to the conventions of the engine, and the whole time I could only thank myself I hadn’t chosen to try to do this in OCaml, where it would have been substantially more difficult and far more brittle.

5 Likes
19

I was not claiming the boilerplate is good, its definitely a real issue. I was reacting to your claim that writing big ppx is almost impossible, when I think that the boilerplate is more of an issue for small ppx (because for a big ppx the boilerplate is going to be 5% of the dev time when for a small one its going to be 50%).

As for the syntax hygiene, I am not sure. I have written a few of ppxes and I never had the issue show up. I know its important in other languages, so maybe it depends on the kind of ppx you are writing. Maybe also because ocaml allows “inner variable” its less of an issue

let x = 123 in
let expanded_macro = 
  let x = 456 in
  ...
in
f x

This ocaml code is fine, but the C equivalent would not be:

int x = 123;
// start of macro expansion
int x = 456;
int expanded_macro = ...;
// end of macro expansion
return f (x)
1 Like
20

The C language does have braces and scoped variables (and the infamous do { ... } while (0) idiom). So, your example is not really representative. The issue with unhygienic macros come from local macro variables shadowing outer variables passed as macro parameters:

#define FOO(v) (let x = 0 in let y = v in y + y)

If you now expand FOO(x) with an unhygienic macro expansion, everything breaks down. The ability to make sure that the name of the inner variable x is different from any subterm of v is critical for any hygienic macro system, be it in OCaml or in C or any other language. (That is why it is recommended in C to use normally illegal variable names inside macros, e.g. __x.)

That said, the issue is compounded in C by the fact that definitions are recursive by default, while they are not in OCaml. So, the following would work in OCaml, even with an unhygienic macro system, but not in C:

#define FOO(v) (let x = v in x + x)
4 Likes