Poly/ML – A Standard ML Implementation

Join the discussion

• Hacker News
• "Standard ML is a functional programming language, in the sense that the full power of mathematical functions is present." From a Pdf linked on the repo (I didn't know what Standard ML was, I was hoping for a mark up language)
  by tingletech
• See SGML for a markup language.
  by nesarkvechnep
• StandardML is a rather nice modular high level functional programming language with algebraic datatypes, pattern matching, compile-time type checking and type inference etc. Poly/ML extends this with strong proven multi-core and cross platform support including Posix threads, parallel garbage collection, FFI etc. Poly/ML has been around a while, but it is still actively maintained by Dave Mathews et al (most recent release June 2026) has good windows and X11 support. Poly/ML is a great way to explore the world of StandardML and is used to build Isabelle and HOL theorem provers. Definitely worth a look!
  by ptrott2017
• For those interested in the Standard ML compilers, Mlton is another one worth checking out. Standard ML of New Jersey (smlnj) is another interesting one although it tends to be more of a research vehicle than polyml or mlton. If you are inclined toward verification, the cakeml project is quite cool as well. For those unfamiliar with standard ML, if you’ve heard of ocaml or F#, they’re relatives in the ML language family.
  by porcoda
• OCaml seems nice for doing real world app development (e.g) web backend, and not limited only for prog lang research.

  Hmmm....

  by anta40
• There is also MLKit which is pretty interesting in how it handles memory, it is region based with some fallback to garbage collection.

  https://elsman.com/mlkit/

  by erk__
• > Standard ML of New Jersey (smlnj) is another interesting one although it tends to be more of a research vehicle than polyml or mlton.

  This is interesting! My impression was that SML/NJ was the de facto "standard" Standard ML implementation (maybe analogous to SBCL in the Lisp world), and (FWIW) Gemini agrees, describing it as "the oldest and most widely used". So I'm surprised to see someone stick it in the rear behind Poly/ML and MLton.

  I don't really know what to make of that, except that I guess there's a surprisingly vibrant SML ecosystem and don't listen to any one person (myself included) about it: try them all and see which SML implementation is right for you :)

  by wk_end
• I've always felt that ML hit the sweet spot between functional and imperative programming. It affords conveniences such as algebraic data types and first-class functions, but unlike Haskell, it doesn't require monadic programming to use IO or mutable references.

  ML also has an interesting module system, which achieves similar goals as object-oriented programming, but in a very different way. While mainstream "class-based" OOP identifies the data type with the unit of encapsulation, ML has "modules," which are separate entities from types, and which may both define types and values as members. However, a downside of this approach is that you sacrifice late binding, as the module language and "core" language are stratified into different layers. Instead, dependency injection is achieved through module-level functions, called functors,

  A lesser-known fact is that ML originated as the scripting language for the LCF proof assistant (which is where the name "ML," or meta language, comes from). In the LCF tradition, the inferences rules of the logic are implemented in a trusted kernel, then clients use those inference rules to write tactic scripts that construct theorem objects. This design was supported by ML's module system: theorems were defined as an abstract type in a "kernel" module, and the inference rules were defined as functions inside the module. Here is a tutorial that explains the LCF design better than I can: https://www.cs.cmu.edu/~fp/courses/15317-f17/recitations/rec...

  by hutao
• and you get concurrentML. People get all wet in the pants by the actor model and CSP, but my god CML is much nicer in every way.

  I had a weird introduction to programming. I spent my first half year doing php, and them went all in on scheme and sml. Which is nice in many ways, but I do have a hard time accepting many of the completely braindead (subjective opinion, of course) choices of most of the popular languages.

  I do think clojure is a pretty nice compromise. Rich has good taste, obviously. Clojure's core.async could be less async and more CML in my taste. Wrapping a simpler async api in cml is easy. Implementing CML on top on core.async is either very hard or full of compromises.

  by bjoli
• Isabelle is still a very active LCF proof assistant, and it's still written in Poly/ML. It's pretty aggressively concurrent under the bonnet, and leverages Poly/ML well for that. There's still HOL4, which predates Isabelle and is still going, and it also recommends using Poly/ML.

  I mostly worked with HOL Light which started as a CAML project and now runs on OCaml.

  by momentoftop
• > a downside of this approach is that you sacrifice late binding, as the module language and "core" language are stratified into different layers

  https://people.mpi-sws.org/~rossberg/1ml/1ml-extended.pdf

  https://github.com/rossberg/1ml

  by sshine
• If only Microsoft had more love for F# instead of slowly copying its features into C#.

  At least it is still officially developed getting new features, unlike C++/CLI and VB that only get bug fixes and updates to keep running on top of recent .NET versions.

  by pjmlp