There was a period of time when I was all about OCaml. I appreciate the purity of Caml and StandardML more though, for whatever reason, just from an aesthetics point (the object-orientedness of OCaml just seems shoehorned in to me).
The sad truth, though, is that in my limited time I have to focus on the stuff I need for work. The only languages I’m truly fluent in anymore are C, Python, SQL, Bourne shell, and…I guess that’s it. I can get around in Lua if I need to, but I haven’t written more than a dozen lines of code in another language in at least five years.
(That’s not to say I don’t love C, Python, SQL, and Bourne shell, because I do.)
I’ve been messing around with Prolog (the first language I ever had a crush on) again just for fun, but I’m worried I’m going to have to put it down because of the aforementioned time issue. Maybe I can start writing some projects at work in ML. :)
SML is probably my favorite language. It’s compact enough that you can keep the whole language (and Basis libraries) in your head fairly easily (compared to, say, Haskell, which is a sprawling language). I find strict execution much easier to reason about than lazy, but the functional-by-default nature remains very appealing.
Basically, it’s in a good sweet spot of languages for me.
But, it’s also a dead language. There is a community, but it’s either largely disengaged (busy writing other languages for work), or students who have high engagement but short lifespans. There are a few libraries out there, and some are good but rarely/never updated, and some are not good and rarely/never updated.
I still think it’s a great language to learn, because (as lmmm says) being fluent in SML will make you a better programmer elsewhere. Just know that there aren’t many active resources out there to help you actually write projects and whatnot.
Everything that you said, plus one thing: Standard ML, unlike Haskell or OCaml, realistically allows you to prove things about programs — actual programs, not informally described algorithms that programs allegedly implement. Moreoever, this doesn’t need any fancy tools like automatic theorem provers or proof assistants — all you need is simple proof techniques that you learn in an undergraduate course in discrete mathematics and/or data structures and algorithms.
Let me be upfront: When I said “prove” in my previous comment, I didn’t mean “fully formally prove”. The sheer amount of tedious but unenlightening detail contained in a fully formal proof makes this approach prohibitively expensive without mechanical aid. Formal logic does not (and probably cannot) make a distinction between “key ideas” and “routine detail”, which is essential for writing proofs that are actually helpful to human beings to understand.
With that being said, I found Bob Harper’s notes very helpful to get started, especially Section IV, “Programming Techniques”. It is also important to read The Definition of Standard ML at some point to get an idea of the scope of the language’s design, because that tells you what you can or can’t prove about SML programs. For example, the Definition doesn’t mention concurrency except in an appendix with historical commentary. Consequently, to prove things about SML programs that use concurrency, you need a formalization of the specifics of the SML implementation you happen to be using (which, to the best of my knowledge, no existing SML implementation provides).
OCaml is yet another mainstream-aiming language full of dirty compromises and even outright design mistakes:
The types of strict lists, trees, etc. are not really inductive, due to OCaml’s permisiveness w.r.t. what can go on the right-hand side of a let rec definition.
It has an annoying Common Lisp-like distinction between “shallow” and “deep” equality.
Moreover, either kind of equality can be used to violate type abstraction.
Mutation is hardwired into several different language constructs (records, objects), rather than provided as a single abstract data type as it well should be.
Applicative functors with impure bodies are leaky abstractions.
Many complaints about OCaml here are justified in a way (I use it in my day job), so I’ve run into a number of issues myself. It is a complex language, especially the module language.
the object-orientedness of OCaml just seems shoehorned in to me
I think that’s a commonly repeated myth but OCaml OOP is not really like Java. Objects are structural which gives it a quite interesting spin compared to traditional nominal systems, classes are more like templates for objects and the object system is in my opinion not more shoehorned than polymorphic variants (unless you consider those shoehorned as well).
Objects are structural which gives it a quite interesting spin compared to traditional nominal systems…
Oh no, I get that. It’s a matter of having object-oriented constructs at all. It’s like C++ which is procedural and object-oriented, and generic, and functional, and and and. I like my languages single-paradigm, dang it! (I know it’s a silly objection, but I’m sometimes too much of a purist.)
I work full-time in Scala, and I credit Paulson with teaching many of the foundations that make me effective in that language. Indeed even when working in Python, my code was greatly improved by my ML experience.
How is Scala? I feel like there would be a significant impedance mismatch between the Java standard libraries, with their heavy object-orientation, and Scala with its (from what I understand) functional style.
I think it would also bug me that the vast majority of the documentation for my languages libraries would be written for another language (that is, I need to know how to use something in Scala, but the documentation is all Java).
It’s really nice. More expressive than Python, safer than anything else one could get a job writing.
I feel like there would be a significant impedance mismatch between the Java standard libraries, with their heavy object-orientation, and Scala with its (from what I understand) functional style.
There’s a mismatch but there are libraries at every point along the path, so it gives you a way to get gradually from A to B while remaining productive.
I think it would also bug me that the vast majority of the documentation for my languages libraries would be written for another language (that is, I need to know how to use something in Scala, but the documentation is all Java).
Nowadays there are pure-Scala libraries for most things, you only occasionally have to fall back to the Java “FFI”. It made for a clever way to bootstrap the language, but is mostly unnecessary now.
There was a period of time when I was all about OCaml. I appreciate the purity of Caml and StandardML more though, for whatever reason, just from an aesthetics point (the object-orientedness of OCaml just seems shoehorned in to me).
The sad truth, though, is that in my limited time I have to focus on the stuff I need for work. The only languages I’m truly fluent in anymore are C, Python, SQL, Bourne shell, and…I guess that’s it. I can get around in Lua if I need to, but I haven’t written more than a dozen lines of code in another language in at least five years.
(That’s not to say I don’t love C, Python, SQL, and Bourne shell, because I do.)
I’ve been messing around with Prolog (the first language I ever had a crush on) again just for fun, but I’m worried I’m going to have to put it down because of the aforementioned time issue. Maybe I can start writing some projects at work in ML. :)
SML is probably my favorite language. It’s compact enough that you can keep the whole language (and Basis libraries) in your head fairly easily (compared to, say, Haskell, which is a sprawling language). I find strict execution much easier to reason about than lazy, but the functional-by-default nature remains very appealing.
Basically, it’s in a good sweet spot of languages for me.
But, it’s also a dead language. There is a community, but it’s either largely disengaged (busy writing other languages for work), or students who have high engagement but short lifespans. There are a few libraries out there, and some are good but rarely/never updated, and some are not good and rarely/never updated.
I still think it’s a great language to learn, because (as lmmm says) being fluent in SML will make you a better programmer elsewhere. Just know that there aren’t many active resources out there to help you actually write projects and whatnot.
Everything that you said, plus one thing: Standard ML, unlike Haskell or OCaml, realistically allows you to prove things about programs — actual programs, not informally described algorithms that programs allegedly implement. Moreoever, this doesn’t need any fancy tools like automatic theorem provers or proof assistants — all you need is simple proof techniques that you learn in an undergraduate course in discrete mathematics and/or data structures and algorithms.
Absolutely. I think the niche for languages with a formal specification is fairly small, but it is irreplacable in that niche.
Just out of curiosity, do you have any reading recommendations on formal proofs for ML programs?
Let me be upfront: When I said “prove” in my previous comment, I didn’t mean “fully formally prove”. The sheer amount of tedious but unenlightening detail contained in a fully formal proof makes this approach prohibitively expensive without mechanical aid. Formal logic does not (and probably cannot) make a distinction between “key ideas” and “routine detail”, which is essential for writing proofs that are actually helpful to human beings to understand.
With that being said, I found Bob Harper’s notes very helpful to get started, especially Section IV, “Programming Techniques”. It is also important to read The Definition of Standard ML at some point to get an idea of the scope of the language’s design, because that tells you what you can or can’t prove about SML programs. For example, the Definition doesn’t mention concurrency except in an appendix with historical commentary. Consequently, to prove things about SML programs that use concurrency, you need a formalization of the specifics of the SML implementation you happen to be using (which, to the best of my knowledge, no existing SML implementation provides).
OCaml is yet another mainstream-aiming language full of dirty compromises and even outright design mistakes:
let recdefinition.Many complaints about OCaml here are justified in a way (I use it in my day job), so I’ve run into a number of issues myself. It is a complex language, especially the module language.
I think that’s a commonly repeated myth but OCaml OOP is not really like Java. Objects are structural which gives it a quite interesting spin compared to traditional nominal systems, classes are more like templates for objects and the object system is in my opinion not more shoehorned than polymorphic variants (unless you consider those shoehorned as well).
So how’s working at Jane Street? :)
Oh no, I get that. It’s a matter of having object-oriented constructs at all. It’s like C++ which is procedural and object-oriented, and generic, and functional, and and and. I like my languages single-paradigm, dang it! (I know it’s a silly objection, but I’m sometimes too much of a purist.)
I work full-time in Scala, and I credit Paulson with teaching many of the foundations that make me effective in that language. Indeed even when working in Python, my code was greatly improved by my ML experience.
How is Scala? I feel like there would be a significant impedance mismatch between the Java standard libraries, with their heavy object-orientation, and Scala with its (from what I understand) functional style.
I think it would also bug me that the vast majority of the documentation for my languages libraries would be written for another language (that is, I need to know how to use something in Scala, but the documentation is all Java).
It’s really nice. More expressive than Python, safer than anything else one could get a job writing.
There’s a mismatch but there are libraries at every point along the path, so it gives you a way to get gradually from A to B while remaining productive.
Nowadays there are pure-Scala libraries for most things, you only occasionally have to fall back to the Java “FFI”. It made for a clever way to bootstrap the language, but is mostly unnecessary now.
Very informative, thank you.