David MacQueen on his Ideas for Successor ML

See https://github.com/dmacqueen/NewFrontEnd and https://standardml.zulipchat.com.

9:33 On disallowing static declarations within expressions: from MLFW2025.txt:

1.3. [Core] No static (type/module) declarations within expressions

  Moto: "Keep the core and module levels separate", or "no static declarations within
  dynamic expressions".

  What does it, or should it, mean to have a (statically generative) datatype declaration
  in the body of a recursive function.

  [Karl Crary (and Bob Harper?) won't like this, since definition of modules within
  expressions is a feature of his dialect of (S)ML. It also appears to be supported in
  Moscow ML. The CMU (Harper, Crary, etc.) view of the static semanatics of (S)ML seems to
  base on some fundamental "type theoretic" notion of a _module_ that seems to be
  different from my own intuitive understanding of the module system of (S)ML. Their ideas
  are described in papers such as Harper-Stone and Sterling-Harper (?). In their view,
  modules are fundamental and the Core constructs are secondary or definable.
  
  Crary talks about "old" and "new" type theoretic definitions of the semantics of (S)ML,
  but I don't yet know what he is referring to.] 

I suspect this is because Bob Harper has big plans for generalising the notion of phase distinction and perhaps then it applies in some dynamical contexts. See System Fω And ML Module Semantics and Bob Harper's Course on Principles of Programming Languages.

See also his ideas about data types as modules in his 2021 OPLSS talk on the ML Module System (first mentioned at 1:03:17). 

The playlist of ML language talks is here.

I don't think this scheme for smart deconstructors meets Bob Harper's criteria for datatype totality/productivity but it is a nice example of what data abstraction should be. There is some interesting use of continuations in the compiler. 

See A Core Language for Extended Pattern Matching and Binding Boolean Expressions.

I think the answer is to go all the way and represent all data using coroutines. If you need static concrete representations then you can still have them, you just need to wrap them in trivial processes and leave it to the compiler to optimise them away. I wrote about this idea in the comments in some serializing code somewhere in 2014.

Another excellent talk was by Mizuki Arata implementing a transpiler from Standard ML to lua and JavaScript.

This is written in Standard ML and is self-hosting. See https://github.com/minoki/LunarML. This is much closer to my idea, which was to take seriously the idea of a Standard Metalanguage and see how far you can get by using Standard ML '97 to define various successor MLs. Then the ideas of meta-programming runtime environments and eventually the whole Operating System can be bootstrapped from there. See On Getting Machines to do Stuff and A New Kind of Science.

CakeML is a formally verified fragment of Standard ML. See https://cakeml.org/ 

See The CakeML Project’s Quest for Ever Stronger Correctness Theorems.

See Running the CakeML Compiler:

So your hyper-verified stack sits on top of what? A random Linux distribution and whatever make program is on your PATH, and whatever C compiler your CC environment variable to, and whatever binary that finds on your PATH. At best I think you end up with GNU cpp and as the latter being, I think, just about the jankiest piece of software in widespread use ever!  And the file cake.S (containing nearly half a million lines) came from a git repository via GNU tar through gzip. But that's OK, this is not meant to actually be anything, it's just to represent a way to say something.

Subscribe to ACM SIGPLAN.