Plenty of research is happening, which is why SML has a wide variety of variant interpreters and compilers, all adhering (mostly) to the standard core. ConcurrentML is an interesting paradigm, and MLTon made some good strides into full-program optimization.
But most of that is academic, and OCaml really stole most of the thunder (by being small and fast, despite having more syntactic warts -- and no, making things look like JS ain't a solution to that).
As an aside: The ML-ML/MachineLearning and JS-JavaScript/Jane Street interpretations makes comments on anything even tangentially related harder to parse. Reason coming in and closing the loop has not made this easier. I wonder whether this affects anyone else.
> And thankfully there's little cause for "NLP" ambiguity these days.
Is there not? When I Google "NLP" the first results are for "Neuro-Linguistic Programming", which I assume is NOT the definition you'd consider the important one. The fact that it also has "programming" in the name and has to do with "linguistics" does not make things easier.
True, but its popularity seems to have decreased enough that I don't get that many quackery-NLP news in my personal bubble / here. So when NLP does turn up, it usually means the right thing.
That people now use "ML" when it's just a simple matter of NLP is another matter…
One reason is probably, that it's a small language with a fully specified semantics. Also, despite its age, it is still a modern language. It's had features like lambdas, type inference, algebraic data types, generics, modules, etc. for decades.
One area people tend to use ML-based languages is software that makes heavy use of algebraic/inductive datatypes, e.g., compilers and interactive theorem provers. (Implementing a theorem prover was the original motivation for ML.) That said, the ML family is general-purpose and suitable for many tasks.
Whenever this comes up, the answer seems to be "for programming language research and proofs in academia" and not much else.
It's a pity. SML is in many ways a joy to work with. The language doesn't change, which is a nice thing in itself in the current climate, but it has many things people still look for in modern languages (type inference, pattern matching, a module system). Multiple compliant compilers are available that produce fast code. The syntax is delightful, relying on neither brace delimiters nor syntactic whitespace. The language and Basis library are small enough that a developer can realistically aim to learn the whole thing. It is a comfortably idiomatic general-purpose functional language: lacking object or procedural syntax but relaxed about side-effects and occasional use of mutable types.
There are problems. Everyone will have their own list of things they expect a language to have, that SML lacks (mine: a map container in the standard library; record updating without rebinding all the elements individually; universal printf/toString, no matter how hacky). There is no standard foreign-function interface for calling native libraries, and no standard memory model - each compiler has its own. There is no standard build system (though I dunno, maybe this is a good thing). Libraries are sorely lacking, although those written many years ago usually still work. Because the language is a stem for academic developments, there are several variations that are intriguing but not actually compatible - CakeML seems to be an example, as it doesn't support functors or records.
I find SML pretty nice for writing small command-line utilities - like a functional alternative to Go or Python.
> It's a pity. SML is in many ways a joy to work with. The language doesn't change, which is a nice thing in itself in the current climate, but it has many things people still look for in modern languages (type inference, pattern matching, a module system). Multiple compliant compilers are available that produce fast code. The syntax is delightful, relying on neither brace delimiters nor syntactic whitespace.
is it now ? Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated ; likewise for people that are taught LISP.
Well of course I think so, since I said it... But -
> Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated
It's possible to wonder why a language like SML doesn't get more use outside academia, since so many people have been taught it as students. And it seems a reasonable explanation that many people who were taught these languages simply disliked the experience. If you're forced to learn a weird non-procedural language with no obvious application and a super-picky type checker that you can't understand, why would you like it?
I had a vaguely similar experience myself, when taught SML as a student in the 90s. I enjoyed it as an exercise, but by the end of the course I still didn't have any useful intuition for how to write a whole program in it. Meanwhile over on the C++ course, the object/procedural mix seemed to make more obvious sense as a way to structure things.
Now, after years working in C++, I think of SML as the easier language and in many ways more natural.
I was taught SML as a first year CS student to learn the basics of programming (although I had already used C-like languages). ML stands for Meta Language - it was originally designed and used to prove theorems. That's why SML itself tends to be quite an academic thing to this day.
Education, primarily * . It is the simplest in the family that includes Rust, Haskell, Scala, OCaml, Swift, F#, Elm, etc. So it makes an excellent environment for learning the foundational concepts of this family. In particular, you can find your ground first before you're forced to reckon with implicits (Scala) type classes/traits (Haskell, Rust, Scala), macros (Rust), etc.
I do some sporadic, long-term work on Ponyo [0] to provide a base for exploration. I've also got a WIP "ebook" [1] on Standard ML.
* Although it's also used for prototyping. A lot of Google and Facebook projects were prototyped in SML or OCaml such as React, Reason, certain WASM components, etc.
I really liked SMLNJ plus there's MLTON which is a highly optimizing SML compiler, albeit not so friendly with error messages (or it wasn't when I used it).
It is possible I am misunderstanding something, but I am pretty sure that is not cat(1) implemented in CakeML. It is an implementation of cat(1) verified using the same HOL libraries, tactics, etc. that they used to verify the implementation of CakeML. I didn't look closely enough to see if they have gone all the way and reimplemented HOL inside of CakeML.
If I recall correctly, most CakeML code is actually written in HOL4 and then translated down to CakeML, and compiled to machine code from there. Unfortunately there isn't very much in the way of documentation or examples for writing concrete CakeML, as the developers seem to use it more as an intermediate representation.
Edit: The page describes two frontends. The first is a "proof-producing synthesis" of a CakeML AST from "ML-like functions in HOL". This is what I believe is the more typical use case of CakeML. The second frontend is a more traditional frontend which parse concrete CakeML syntax.
24 comments
[ 4.1 ms ] story [ 48.1 ms ] threadBut most of that is academic, and OCaml really stole most of the thunder (by being small and fast, despite having more syntactic warts -- and no, making things look like JS ain't a solution to that).
And thankfully there's little cause for "NLP" ambiguity these days.
Is there not? When I Google "NLP" the first results are for "Neuro-Linguistic Programming", which I assume is NOT the definition you'd consider the important one. The fact that it also has "programming" in the name and has to do with "linguistics" does not make things easier.
That people now use "ML" when it's just a simple matter of NLP is another matter…
[0]: https://developers.google.com/ml-kit/
[1]: http://www.elsman.com/mlkit/
- HOL4, Isabelle, ProofPower : Standard ML
- Coq, HOL Light, HOL Zero : OCaml
- Lean : C++
- Agda, Idris: Haskell
- Mizar : Pascal
- Metamath : C
It's a pity. SML is in many ways a joy to work with. The language doesn't change, which is a nice thing in itself in the current climate, but it has many things people still look for in modern languages (type inference, pattern matching, a module system). Multiple compliant compilers are available that produce fast code. The syntax is delightful, relying on neither brace delimiters nor syntactic whitespace. The language and Basis library are small enough that a developer can realistically aim to learn the whole thing. It is a comfortably idiomatic general-purpose functional language: lacking object or procedural syntax but relaxed about side-effects and occasional use of mutable types.
There are problems. Everyone will have their own list of things they expect a language to have, that SML lacks (mine: a map container in the standard library; record updating without rebinding all the elements individually; universal printf/toString, no matter how hacky). There is no standard foreign-function interface for calling native libraries, and no standard memory model - each compiler has its own. There is no standard build system (though I dunno, maybe this is a good thing). Libraries are sorely lacking, although those written many years ago usually still work. Because the language is a stem for academic developments, there are several variations that are intriguing but not actually compatible - CakeML seems to be an example, as it doesn't support functors or records.
I find SML pretty nice for writing small command-line utilities - like a functional alternative to Go or Python.
is it now ? Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated ; likewise for people that are taught LISP.
Well of course I think so, since I said it... But -
> Caml has been taught for a long time to a lot of to-be engineering students in france, and it was frankly almost universally hated
It's possible to wonder why a language like SML doesn't get more use outside academia, since so many people have been taught it as students. And it seems a reasonable explanation that many people who were taught these languages simply disliked the experience. If you're forced to learn a weird non-procedural language with no obvious application and a super-picky type checker that you can't understand, why would you like it?
I had a vaguely similar experience myself, when taught SML as a student in the 90s. I enjoyed it as an exercise, but by the end of the course I still didn't have any useful intuition for how to write a whole program in it. Meanwhile over on the C++ course, the object/procedural mix seemed to make more obvious sense as a way to structure things.
Now, after years working in C++, I think of SML as the easier language and in many ways more natural.
* Facebook - OCaml for Hack, Reason, Flow - static analysis and compilers
* Jane Street - heavy user for their entire backend
* Bloomberg
* Citrix
etc https://ocaml.org/learn/companies.html
Haskell is also closely related but different as it has lazy evaluation unlike SML
https://wiki.haskell.org/Haskell_in_industry
I was taught SML as a first year CS student to learn the basics of programming (although I had already used C-like languages). ML stands for Meta Language - it was originally designed and used to prove theorems. That's why SML itself tends to be quite an academic thing to this day.
I do some sporadic, long-term work on Ponyo [0] to provide a base for exploration. I've also got a WIP "ebook" [1] on Standard ML.
* Although it's also used for prototyping. A lot of Google and Facebook projects were prototyped in SML or OCaml such as React, Reason, certain WASM components, etc.
[0] https://github.com/eatonphil/ponyo
[1] http://ponyo.org/guides
I really liked SMLNJ plus there's MLTON which is a highly optimizing SML compiler, albeit not so friendly with error messages (or it wasn't when I used it).
https://github.com/CakeML/cakeml/blob/master/examples/iocatP...
Edit: The page describes two frontends. The first is a "proof-producing synthesis" of a CakeML AST from "ML-like functions in HOL". This is what I believe is the more typical use case of CakeML. The second frontend is a more traditional frontend which parse concrete CakeML syntax.