Unix System Programming with Standard ML (2001) [pdf](mlton.org)
mlton.org
Unix System Programming with Standard ML (2001) [pdf]
http://www.mlton.org/References.attachments/Shipman02.pdf
48 comments
SML modules are a classic example of a "shadow language" ( https://gbracha.blogspot.com/2014/09/a-domain-of-shadows.htm... ). I'd like to see an ML-like language where modules/interfaces are normal values, functors are just normal functions, etc.
Modeling such a system at the value level is easy enough, but having it run at compile-time introduces some tricky issues (especially around IO).
Modeling such a system at the value level is easy enough, but having it run at compile-time introduces some tricky issues (especially around IO).
Andreas Rossberg's 1ML is (was?) an effort to unify the module syntax with that of functions and values (https://people.mpi-sws.org/~rossberg/papers/Rossberg%20-%201..., https://github.com/rossberg/1ml)
The module syntax is certainly clumsy in comparison to the rest of the language, and it's not just the syntax - everything about functor arguments is a bit murky.
The module syntax is certainly clumsy in comparison to the rest of the language, and it's not just the syntax - everything about functor arguments is a bit murky.
Thanks for the link, it looks just like what I was after!
I've been reading through the paper and it looks really nice. It seems to rely on dependent records, which I assumed might be the case; but it claims the dependency is "benign" and elaborates-way when translated to System-F (I haven't reached that part yet); so it does seem to have found the right "trick" (i.e. a tractable subset of dependent types which enables modules, without losing too much inference or devolving into a game of prove-the-lemma).
Incidentally, it's also a nice use of "first class types" which isn't (fully) dependently-typed. It irks me when I read blog posts about e.g. Agda or Idris, which describe first-class types (i.e. no stratification, passing types in and out of functions, etc.) but call that "dependent types"; then don't mention the actual "dependent" part (type signatures which bind values to names, which can be referenced "later on" in the type).
I've been reading through the paper and it looks really nice. It seems to rely on dependent records, which I assumed might be the case; but it claims the dependency is "benign" and elaborates-way when translated to System-F (I haven't reached that part yet); so it does seem to have found the right "trick" (i.e. a tractable subset of dependent types which enables modules, without losing too much inference or devolving into a game of prove-the-lemma).
Incidentally, it's also a nice use of "first class types" which isn't (fully) dependently-typed. It irks me when I read blog posts about e.g. Agda or Idris, which describe first-class types (i.e. no stratification, passing types in and out of functions, etc.) but call that "dependent types"; then don't mention the actual "dependent" part (type signatures which bind values to names, which can be referenced "later on" in the type).
Is ML used in industry? If so, what would be the scenarios/use cases?
> what would be the scenarios/use cases?
MLs are good at representing and manipulating complicated data with intricate invariants (e.g. using algebraic data types for representions, pattern-matching for traversing/manipulating data, abstract/existential types for encapsulation and enforcing interfaces, etc.). In practice this makes it good for handling other languages (after all, "ML" stands for "meta language").
Its original purpose was manipulating mathematical proofs/expressions, and it's still popular for that, e.g. Isabelle's core is written in PolyML, Coq is written in Ocaml, and I think some others like the various HOLs use it too; note that these see a little use in industry for verification (although some famous verification examples, like AMD's FPU verification, used ACL2 which is based on Lisp rather than ML).
It's also good for manipulating Web languages like HTML and Javascript, which has spawned a few compile-to-Web languages which are ML-like or implemented in ML, e.g. http://opalang.org and http://www.impredicative.com/ur . This might also be why Facebook made/use Reason ( https://reasonml.github.io ), which AFAIK is an alternative syntax for Ocaml.
Jane Street seem to be heavy users of Ocaml, since they sponsor a lot of work on the compiler and infrastructure.
MLs are good at representing and manipulating complicated data with intricate invariants (e.g. using algebraic data types for representions, pattern-matching for traversing/manipulating data, abstract/existential types for encapsulation and enforcing interfaces, etc.). In practice this makes it good for handling other languages (after all, "ML" stands for "meta language").
Its original purpose was manipulating mathematical proofs/expressions, and it's still popular for that, e.g. Isabelle's core is written in PolyML, Coq is written in Ocaml, and I think some others like the various HOLs use it too; note that these see a little use in industry for verification (although some famous verification examples, like AMD's FPU verification, used ACL2 which is based on Lisp rather than ML).
It's also good for manipulating Web languages like HTML and Javascript, which has spawned a few compile-to-Web languages which are ML-like or implemented in ML, e.g. http://opalang.org and http://www.impredicative.com/ur . This might also be why Facebook made/use Reason ( https://reasonml.github.io ), which AFAIK is an alternative syntax for Ocaml.
Jane Street seem to be heavy users of Ocaml, since they sponsor a lot of work on the compiler and infrastructure.
The wiki page for SML claims it's used by chip manufacturers like ARM, but no citation.
However, languages like Ocaml and F# are direct descendants of ML, and those languages see wider modern adoption. In this sense ML is kind of equivalent to C, and something like Ocaml is kind of equivalent to C++. Haskell is also in the ML family but its laziness and emphasis on purity keeps it a bit separate from its cousins.
In general, FP sees adoption where correctness is of overriding importance -- e.g., Jane Street's use of Ocaml.
However, languages like Ocaml and F# are direct descendants of ML, and those languages see wider modern adoption. In this sense ML is kind of equivalent to C, and something like Ocaml is kind of equivalent to C++. Haskell is also in the ML family but its laziness and emphasis on purity keeps it a bit separate from its cousins.
In general, FP sees adoption where correctness is of overriding importance -- e.g., Jane Street's use of Ocaml.
OCaml has first-class modules & functors (functions on modules). I can write something like:
let f (type t) some_arg (module M : Stringable with type t = t) = M.to_string some_arg
val f : 'a -> (module Stringable with type t = 'a) -> string
module type Stringable = sig
type t
val to_string : t -> string
let id x = x
id (module Int)Interesing; I've not used Ocaml much (mostly just reading, e.g. the Coq source), so I'm more familiar with StandardML's more verbose separation.
Scala is interesting in this sense; I'd consider it to be an ML-like language. It attempts to unify object systems and module systems, and they are fairly first class in Scala. Modules (objects) can be used as normal values; you can encode functors as functions or classes as needed; signatures (traits) are usable as values to some degree, too.
>Furthermore, path-dependent types allow Scala to unify modules and objects, so that the same language constructs can be used to specify the overall structure of a program as well as its implementation details. The unification of the module and term languages is witnessed by the following comparison with the ML module system: Scala objects correspond to ML modules, classes to functors, and interfaces to signatures [Odersky and Zenger 2005].
https://arxiv.org/pdf/1904.07298.pdf
>Furthermore, path-dependent types allow Scala to unify modules and objects, so that the same language constructs can be used to specify the overall structure of a program as well as its implementation details. The unification of the module and term languages is witnessed by the following comparison with the ML module system: Scala objects correspond to ML modules, classes to functors, and interfaces to signatures [Odersky and Zenger 2005].
https://arxiv.org/pdf/1904.07298.pdf
Compared to OCaml, SML pattern matching syntax can be frustrating, mainly because there's no guards. It's not needed that often - but when it's needed, the code with guards is much simpler than multiple branches with nested conditionals.
> The only thing holdong sml back in my eyes is somewhat clunky syntax and the module system
Those are both tricky, but I think the much bigger deal is that the package ecosystem is about as lush as the parts of Antarctica that are above sea level.
I suspect that the standard getting whacked together before the language really had a chance to mature had the unfortunate effect of stunting its growth.
Those are both tricky, but I think the much bigger deal is that the package ecosystem is about as lush as the parts of Antarctica that are above sea level.
I suspect that the standard getting whacked together before the language really had a chance to mature had the unfortunate effect of stunting its growth.
Isn't the simplicity of SML one of its strengths, even Ocaml being more complex?
If you're going for more sugar, F# might fit the bill. Can handle shebangs, too.
If you're going for more sugar, F# might fit the bill. Can handle shebangs, too.
If you like SML, it might be worth trying Erlang. It comes out of a telecom company, too. The mechanical sympathy I love in SML, I find in Erlang. The ideas that seeded SML, seem to have have found more fertile ground at Ericsson where they still thrive. YMMV.
Erlang has dynamic typing, no? Static typing is especially what interests me in SML, and it's a such core thing, I'm kinda honestly confused what's similar between SML and Erlang?? (I don't know either of them well, so I'd be really interested to learn about some deep similarities from experienced people.)
Both languages were designed with a similar audience in mind. Engineers who write programs incidental to engineering in another discipline. Telcom engineers in both cases.
Erlang supports gradual typing with type specs and dialyzer. It's not as strong of a type system as ML, but it's pretty handy and not particularly cumbersome.
I think it's still fairly young, but Gleam is an ML family language that works with the BEAM. Specifically, it compiles to erlang.
Out of curiosity, what did you find clunky about the syntax? I think languages in the ML family have quite simple and minimal syntax.
The only thing I find clunky about SML syntax are infix operators, since fixity specifications aren't exported.
http://mlton.org/InfixingOperators
Otherwise, I love SML syntax, and would be curious to see the answer to this, too. I find it refreshingly simple and consistent. Is it that it uses 'let ... in ... end' and such rather than whitespace or brackets?
http://mlton.org/InfixingOperators
Otherwise, I love SML syntax, and would be curious to see the answer to this, too. I find it refreshingly simple and consistent. Is it that it uses 'let ... in ... end' and such rather than whitespace or brackets?
What's the problem with the module system and functors?
Few years ago I took a course by prof. Dan Grossman on Coursera, there was a part about SML and I so liked it (the language and the course). Now I want to read Okasaki's "Purely Functional Data Structures" book and try to reproduce the code examples in SML.
As far as I remember PFDS is actually written with SML code.
Somehow I have an impression that I tried something and could not repeat it in SML/NJ. I can recall it was about streams and lazy evaluations, but now I think that I just misused Lazy lib since I haven't used SML for a while. So this is getting easier, great, thanks! :)
Programming Languages by Dan Grossman, I took it too. Pretty good course, and a nice intro to static typing and FP with SML. Also nice: the DrRacket part, I wasn't familiar with lisp/scheme-like languages. Also also nice: how you can tell he doesn't really like Ruby ;)
Oh yes, and I can remember the episode when he jumped while explaining some idea in order to make this moment unforgettable. Shame on me, I forgot what idea it was but still remember his jumps :)
As someone with absolutely zero experience with ML languages of any kind, would this be the best intro for me to get into it? Or would I be better off with OCaml?
Eventually I would learn Ocaml, as it's the more sensible language for most production code (community, tooling, ecosystem, etc.). But there's nothing wrong with learning SML first. 90% of what you learn will be transferable to Ocaml. Starting with SML might help you focus on the "essence" of ML languages rather than getting overwhelmed by the impressive range of options that Ocaml opens up.
The MLton implementation of SML -- while not necessarily the best ML to practice on -- is particularly interesting because it's a whole-program optimizing compiler. It has a reputation for producing very compact, efficient machine code. Having said that, Ocaml is still a comparatively simple language -- compared to say, Haskell or C++ -- and its native compiler is well known for turning out decent and very predictable code (predictable in the sense that you can read some source code and have a decent understanding of what kind of machine code it will get compiled into).
If you decide to learn Ocaml first, but want to stick to "essential ML", I would recommend Jason Hickey's "Introduction to Ocaml" [1] over the more modern "Real World Ocaml" [2], as the latter book introduces every bell and whistle that Ocaml offers, and has a much more ecosystem-dependent focus (third party libraries, third party tooling, etc.). Still a fine book, but I think it emphasizes advanced Ocaml features a bit too much for an introductory text.
[1] http://courses.cms.caltech.edu/cs134/cs134b/book.pdf [2] https://realworldocaml.org/
The MLton implementation of SML -- while not necessarily the best ML to practice on -- is particularly interesting because it's a whole-program optimizing compiler. It has a reputation for producing very compact, efficient machine code. Having said that, Ocaml is still a comparatively simple language -- compared to say, Haskell or C++ -- and its native compiler is well known for turning out decent and very predictable code (predictable in the sense that you can read some source code and have a decent understanding of what kind of machine code it will get compiled into).
If you decide to learn Ocaml first, but want to stick to "essential ML", I would recommend Jason Hickey's "Introduction to Ocaml" [1] over the more modern "Real World Ocaml" [2], as the latter book introduces every bell and whistle that Ocaml offers, and has a much more ecosystem-dependent focus (third party libraries, third party tooling, etc.). Still a fine book, but I think it emphasizes advanced Ocaml features a bit too much for an introductory text.
[1] http://courses.cms.caltech.edu/cs134/cs134b/book.pdf [2] https://realworldocaml.org/
Great comment, I'll bookmark those!
Absolutely recommend following gps advice on starting with sml - ocaml has some... Bumps. But the other option would be to just start with the reasonml dialect of ocaml:
https://reasonml.github.io/
And just FYI, reasonml "is-a" ocaml, so you can also build binaries with the regular compiler back-end - you're not "locked" to targeting js.
https://reasonml.github.io/
And just FYI, reasonml "is-a" ocaml, so you can also build binaries with the regular compiler back-end - you're not "locked" to targeting js.
> And just FYI, reasonml "is-a" ocaml, so you can also build binaries with the regular compiler back-end - you're not "locked" to targeting js.
The full isomorphism is great. I started with the Reason syntax and when I decided I preferred standard syntax[1], I just use formatting tools to convert my codebases in O(1) effort.
1: Because of tool maturity, and the ecosystem around the standard syntax specifically. I wanted to be able to run `dune utop`, but getting that working with Reason was a WIP; and then there's syntax extensions... And docs are in the OCaml syntax, except the BS ecosystem, which is conveniently bilingual
The full isomorphism is great. I started with the Reason syntax and when I decided I preferred standard syntax[1], I just use formatting tools to convert my codebases in O(1) effort.
1: Because of tool maturity, and the ecosystem around the standard syntax specifically. I wanted to be able to run `dune utop`, but getting that working with Reason was a WIP; and then there's syntax extensions... And docs are in the OCaml syntax, except the BS ecosystem, which is conveniently bilingual
Cornell has a book too that's updated every semester https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/
Start with this: https://www.coursera.org/learn/programming-languages
Free online course that teaches statically-typed functional programming using SML as a teaching language. Lecture videos are short and to the point. Prof. Dan Grossman is widely recognized as a great lecturer and he gets the ideas across really well.
From there learn OCaml, which is the ML with the widest industry adoption.
Free online course that teaches statically-typed functional programming using SML as a teaching language. Lecture videos are short and to the point. Prof. Dan Grossman is widely recognized as a great lecturer and he gets the ideas across really well.
From there learn OCaml, which is the ML with the widest industry adoption.
I think that Ullman's 'Elements of Standard ML' remains one of the best introductions to functional programming in general. Wonderful little book...
If you want to learn a bit and check out OCaml.
https://try.ocamlpro.com/
https://try.ocamlpro.com/
Honestly the book Purely Functional Data Structures opened my eyes to the different approach functional languages supply. The concept of pattern matching is so pervasive in ML and I would say that in tandem with creating data structures using types is the central idea of ML that you put to use when using it.
Ah, Standard ML. That brings back great memories of my compiler class at University. This was the first functional language that I was truly comfortable with, and a great tool to write our toy compiler.
[deleted]
Note that despite the origin of the link the book seems to use SML/NJ, not MLTon.
Nothing against MLTon, but SML/NJ seems to be in more common use based on my experience with the [SML] tag on StackOverflow.
I like to use SML/NJ for development and experimentation, and MLton for final compilation.
SML/NJ is a really nice development environment, and using a different compiler like MLton or Poly/ML for the final compilation forces you to use the more common, standard subset of ML rather than implementation-specific features.
SML/NJ is a really nice development environment, and using a different compiler like MLton or Poly/ML for the final compilation forces you to use the more common, standard subset of ML rather than implementation-specific features.
Definitely. That's why I got excited and thought that there's something specific about MLTon that's used for systems programming here (the capabilities of the "Standard" MLs vary a bit).
A similar, nicely written book for Ocaml:
https://ocaml.github.io/ocamlunix/
https://ocaml.github.io/ocamlunix/
The only thing holdong sml back in my eyes is somewhat clunky syntax and the module system—which is great at first but quickly becomes tricky once you start having to use functors.
A modern, reimagined sml that keeps its core while adopting some of the nicer syntactic improvements from other langs in the family and improving the module system would be a god send