Type Theory of SML

Standard ML appears to be prenex polymorphic typed-lambda calculus, but it is a Hindley-Milner system. But I'm skeptical whether this is a good intuition, since it seems algebraic data types match initial algebras for endofunctors.

I'm going to have to examine the definition in greater detail, but I do not know what the type theoretic structure of a datatype (algebraic data type) is, exactly. I suspect it is a iso-recursive variant type, if I may borrow the terminology of TAPL.

If we allow anything to appear in a reference type, then we can quickly run into problems when storing a function in a reference. Because of this, Standard ML restricts what values may be stored in a reference type. The 1997 definition calls them Non-Expansive Expressions and defines the in chapter 4 section 7.

These are precisely "values", in the sense of TAPL.

After desugaring an expression and performing the expansions defined in the parsing step, the grammar for them in quasi-EBNF:

nexp = scon              ; special constants = literal values
     | ["op"] longvid    ; identifiers
     | "{" [nexprow] "}" ; record types
     | "(" nexp ")"
     | conexp nexp       ; constructors applied to nexp
     | nexp ":" ty
     | "fn" match        ; anonymous functions

nexprow = lab "=" nexp ["," nexprow]

conexp = "(" conexp [":" ty] ")"
       | ["op"] longvid

The only constraints here are that within a conexp we require longvid is not ref, and is of \(C(longvid)\in\{\mathtt{c},\mathtt{e}\}\).

We should actually think of "non-expansive expressions" as "syntactic values". (If we compare them to semantic values found in chapter 6, then we're actually pretty close.)

Observe that ref NONE is not a non-expansive expression because we could do terrible things, like:

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

Also observe:

• Function applications are expansive expressions
• Let-expressions are expansive expressions
• Raising or handling exceptions are expansive expressions
• Conditionals and case-expressions are expansive expressions

Really, any expressions which can be evaluated further can create new reference cells or raise exceptions, which are expansive (in the sense that they expand memory usage).

The notion of the "closure" operation when elaborating an expression (the Clos operation defined in section 4.8) occurs in rule (15) of the definition of Standard ML and is responsible for transforming an expression into a polymorphic expression. This "Clos" operation enforces value restriction by preventing a declaration binding an identifier to an expansive expression from becoming polymorphic.

The comment to rule (15) is also worth pondering.

• Types and Type Checking SMLNJ documentation
• MLton documentation has a lot of gems
  • Value Restriction
  • Monomorphise seems to support the intuition of initial algebra semantics for algebraic data types
  • First-Class Polymorphism doesn't exist in Standard ML (alas)