Context: doing some ML codegen; finding this rec requirement to be annoying.
It also seems many other languages: Rust, Scala, Kotlin, Java, … do not have this limitation.
It’s not a limitation. It’s a design choice to prevent accidental recursion which can often cause hard to find infinite looping bugs. It also lets you decide as the programmer whether you want to use an old binding of the same name or not.
For further reading, @gasche answers this question in full on stack overflow.
Side note: there’s also the sometimes useful [@nonrec] annotation for type definitions which allows you to refer to previous bindings.
10 Likes
A little more on “design choice”. ML descends from a lineage, and was designed by a community of CS/logic folks, who thought a lot about program correctness. In reasoning about program correctness, unbounded recursion is one of the big sources of problems: in the absence of unbounded recursion and associated non-well-founded datatypes, al programs terminate, for example. Now, it’s been a long, long time, but basically many languages in the ML family have a strong design choice of a core language that is terminating, and then a few features that let you step out into unbounded recursion. And you see a similar thing with mutable data: the core of the language is all immutable data, and then there’s these additions for mutability.
This is in marked contrast to (many of) the languages you mention, which all started from “regular programming languages”: which all prioritize mutability and recursion at their cores.
Rust is a singular outlier in your list, btw: if I were a working type theorist, I might have things to say, but I’m not, so I’ll just bloviate grin: it seems like Rust isn’t a fully-mutable language: mutability is strongly controlled, and that allows some amount of the ability to reason about programs that you get in FP languages (like ML).
If you go back to the origin of ML (1970s as a language for programming proof-assistants), it’s actually pretty amazing that it turned out to be so effective as a language for writing real programs and real systems.
7 Likes
Case in point: Aeneas: Rust Verification by Functional Translation (ICFP 2022 - ICFP Papers and Events) - ICFP 2022 is some very cool reasearch that uses the borrow checker constraints to convert mutable rust programs into functional pure equivalents that can be more easily verified in frameworks such as Coq or F*.
1 Like
Because oh boy, was I bitten by it in Haskell.
Also, OCaml allows one to use the idiom of keeping the same name for an evolving value as its type transforms. This lowers cognitive load and avoids bugs of using the wrong (earlier) version of the value. E.g. let x = f a in let x = g x in let x = ....
5 Likes