Standard ML

These are the easiest to visualize and explain. Values are named constants.

val pi = 3.14159; (* A declaration without a type annotation *)
val tau : real = 6.28318; (* An annotated declaration *)

There are two styles to declaring functions, the curried approach and the uncurried approach. The uncurried approach declares the function to take a tuple and produce a value.

fun cylinder_volume(r,h) = pi*r*r*h;

We can optionally annotate each parameter with its type:

fun cyl_vol2(r : real, h : real) = pi*r*r*h;

We can optionally annotate the result

fun cyl_vol3(r,h) : real = pi*r*r*h;

We can use curried versions:

fun cyl_vol4 r h = pi*r*r*h;

To have a type annotated curried function definition, we must parenthetize each argument to declare its type:

fun cyl_vol5 (r : real) (h : real) = pi*r*r*h;

This makes the line really long when we have more than a couple arguments to a function; I suspect this is one reason people use signatures and modules. We stick the declaration in the signature and the definition in the module, but we'll tackle that later.

Besides the usual arithmetic expressions, we have a few more worth mentioning:

• let-in-end expressions for local definitions
• if-then-else expressions for conditional flow
• case expressions for pattern matching

Care must be taken, since in Standard ML the boolean operators provided are:

• andalso for short-circuiting conjunction
• orelse for short-circuiting disjunction
• not for negation

The and keyword has a technical meaning for simultaneous definitions.

We test for equality using = and inequality using <>, but this only works on "equality types" (unit, int, word, char, string, array, vector, ref).

The built-in types include: bool, int, real (for floating point), char, string, and unit (analogous to void in C-like languages). We can build tuples using the Cartesian product, written T1*T2 for the product of type T1 with type T2. Function types are built using arrows T1 -> T2, like in Haskell or OCaml.

There are two ways to introduce types: one is to make an alias of an existing type, the other is to construct an algebraic data type.

type Identifier = string;

datatype Expr = Var of Identifier
              | Abs of (Expr*Expr)
              | App of (Expr*Expr);

It's important to note the constructor is separated from the rest of the row by an "of" keyword.

CAUTION: Unlike Haskell, Standard ML writes parametrized types "backwards"; e.g., in Haskell we have a List int, but in Standard ML we have int list.

Standard ML provides the ability to have mutable variables, by making them references to memory locations. Basically, we dereference the ref using an exclamation point, and assign it a value using :=. For example:

val iref : int ref;

iref := 3; (* initialize the ref *)

iref := !iref - 1; (* update the ref *)

val foo : int = (!iref)*7; (* use the ref *)

We should think of ref as a parametrized type, 'a ref.

We are given some initial functions and type declarations in the "initial basis". The types given:

• eqtype unit which has a single value, ()
• eqtype int
• eqtype word
• type real for floating point numbers
• eqtype char, characters are indicated by #"a" for 'a', or #"\n" for a newline character, or #"\uxxxx" where xxxx are 4 hexadecimal constants
• eqtype string for strings (double quoted, "foo")
• type substring
• type exn for exceptions
• eqtype 'a array
• eqtype 'a vector
• eqtype 'a ref
• datatype bool = false | true
• datatype 'a option = NONE | SOME of 'a
• datatype order = LESS | EQUAL | GREATER
• datatype 'a list = nil | ​:​: of ('a * 'a list)

There are about a dozen primitive exceptions defined:

exception Bind
exception Chr
exception Div
exception Domain
exception Empty
exception Fail of string
exception Match
exception Option
exception Overflow
exception Size
exception Span
exception Subscript

The non-overloaded functions provided at the top-level:

• List functions
  • val app : ('a -> unit) -> 'a list -> unit, so app f lst applies f to lst ("from left to right")
  • val @ : ('a list * 'a list) -> 'a list for concatenating lists
  • val foldl : ('a*'b->'b)-> 'b -> 'a list -> 'b, interpreted as foldl f init x1::xs = foldl f f(x1,init) xs, and foldl f init [] = init.
  • val foldr : ('a*'b->'b)-> 'b -> 'a list -> 'b, interpreted as foldr f init x::xs = f(x, foldr f init xs), and foldr f init [] = init.
  • val hd : 'a list -> 'a produces the first element in a list hd x::xs = x, raises error if operating on empty list hd [] = raise Empty
  • val length : 'a list -> int for the length of a list
  • val map : ('a -> 'b) -> 'a list -> 'b list produces a new list by applying a function to each element of the supplied list
  • val null : 'a list -> bool, tests if the list is empty
  • val rev : 'a list -> 'a list reverses the list
  • val tl : 'a list -> 'a list gives the rest of the list tl x::xs = xs, raises error if operating on empty list tl [] = raise Empty
• Characters
  • val chr : int -> char produces a character from a "code point" integer
  • val ord : char -> int produces the "code point" for a given integer
• Options
  • val getOpt : ('a option * 'a) -> 'a
  • val isSome : 'a option -> bool
  • val valOf : 'a option -> 'a gives the value of the option (i.e., valOf (SOME x) = x)
• Reals
  • val ceil : real -> int
  • val floor : real -> int
  • val real : int -> real produces a real for a given int
  • val round : real -> int rounds a real to its nearest integer
  • val trunc : real -> int truncates a real (i.e., "throws away the fractional part")
• References
  • val ref : 'a -> 'a ref primitive
  • val ! : 'a ref -> 'a
  • val := : 'a ref * 'a -> unit
• Strings
  • val ^ : string * string -> string, an inline string concatenation s ^ t
  • val concat : string list -> string concatenates together a list of strings (concat s::strs = foldr ^ s strs | [] = "")
  • val explode : string -> char list produces the list of characters in a string
  • val implode : char list -> string creates a string from a list of characters, should be the same as concat o (map str).
  • val size : string -> int gives the size of the string
  • val str : char -> string turns a character into a string, e.g., str #"a" = a
  • val substring : string * int * int -> string will produce the substring starting at the first number taking a specific number of characters, e.g., substring (s,i,j) returns s[i..i+(j-1)]; it raises an exception if i < 0 or j < 0 or |s| < i+j
• Miscellaneous
  • val not : bool -> bool, negation (not true = false, not false=true)
  • val before : 'a * unit -> 'a, an infixed operation, a before b returns a. It provides a notational shorthand for evaluating a, then b, before returning the value of a.
  • val exnMessage : exn -> string, get the message for an exception
  • val exnName : exn -> string, get the name for an exception
  • val ignore : 'a -> unit, ignore a returns (). The purpose of ignore is to discard the result of a computation, returning () instead. This is useful, for example, when a higher-order function, such as List.app, requires a function returning unit, but the function to be used returns values of some other type.
  • val o : ('a->'b) * ('c->'a) -> 'c->'b composes functions, like Haskell's dot operator, (g o f)(x) = g(f(x)).
  • val use : string -> unit will load a file (compiler/system dependent)
  • val print : string -> unit, prints a given string to the screen
  • val vector : 'a list -> 'a vector produces a vector from a list

There are also about a dozen "overloaded identifiers" which programmers may not overload:

• val + : num * num -> num addition (defaults to num=int)
• val - : num * num -> num, subtraction
• val * : num * num -> num, multiplication
• val div : wordint * wordint -> wordint, takes the quotient of integers (or word-sized integers)
• val mod : wordint * wordint -> wordint, i mod j returns i-j*floor((i/j))
• val / : real * real -> real divides two real numbers
• val ~ : num -> num negation, equivalent to multiplying by -1
• val abs : realint -> realint, the absolute value of either a real or an int
• val < : numtext * numtext -> bool, compares two number (or two strings lexicographically)
• val > : numtext * numtext -> bool, compares two number (or two strings lexicographically)
• val <= : numtext * numtext -> bool, compares two number (or two strings lexicographically)
• val >= : numtext * numtext -> bool, compares two number (or two strings lexicographically)

The top-level environment has the following infix identifiers and associated precedence levels:

• infix 7 *, /, div, mod
• infix 6 +, -, ^
• infixr 5 ::, @
• infix 4 =, <>, >, >=, <, <=
• infix 3 :=, o
• infix 0 before

So we would parse a*b + i/j as (a*b) + (i/j) since the precedence for multiplication is higher than addition, and division is higher than addition.

Signatures specify a minimum necessary for a structure. Each entry in a signature is interpreted as a specification.

signature QUEUE = sig
    type 'a t; (* type of queues *)
    exception E; (* for errors *)
    val empty : 'a t; (* the empty queue *)
    val enq : 'a t * 'a -> 'a t; (* add to end *)
    val null : 'a t -> bool; (* test for empty queue *)
    val hd : 'a t -> 'a; (* return the front of the queue *)
    val deq : 'a t -> 'a t; (* remove the front of the queue *)
end;

This seems to be the naming convention most Standard ML programmers use: signatures are ALL_UPPER_CASE, structures are PascalCased.

Also, for something like this QUEUE signature, where the signature specifies a single type, it seems to be convention to call it "t" (presumably short for "type").

We can "implement" a queue by making the types declared in the signature "transparent" (accessible outside the structure) or "opaque" (inaccessible outside the structure). For example:

structure Q1 : QUEUE = struct
    type 'a t = 'a list;
    exception E;

    val empty = [];

    fun enq (q, x) = q@[x];

    fun null(x::q) = false
      | null _     = true;

    fun head(x::q) = x
      | head _     = raise E;

    fun deq(x::q) = q
      | deq _     = raise E;
end;

structure Q2 :> QUEUE = struct
    type 'a t = 'a list;
    exception E;

    val empty = [];

    fun enq (q, x) = q@[x];

    fun null(x::q) = false
      | null _     = true;

    fun head(x::q) = x
      | head _     = raise E;

    fun deq(x::q) = q
      | deq _     = raise E;
end;

List.null Q1.empty; (* evaluates to "true" *)

List.null Q2.empty; (* ERROR!!! *)
(* In SML/NJ we get:

stdIn:7.1-7.19 Error: operator and operand do not agree [tycon mismatch]
  operator domain: 'Z list
  operand:         'Y Q3.t
  in expression:
    List.null Q3.empty

In HaMLet:

(input 2):1.0-1.18: type mismatch on application
*)

Since QUEUE had not defined its type 'a t, when we have structure Q2 opaquely ascribe to QUEUE, it hides the definition of type 'a t: its constructors are hidden from the user, and distinct from existing constructors.

• Implementations
  • SML/NJ (see also cvs)
  • HaMLet
  • PolyML

• Lawrence Paulson,
  ML for the Working Programmer. CUP, second ed., 1996; Online version
• M.Tofte, "Tips for Computer Scientists on Standard ML (Revised)". Eprint.

There is a precise definition of Standard ML (first published in 1990, later revised in 1997).

• The "initial basis" (top-level environment provided by Standard ML) is described here, and the Standard Basis documentation describes the libraries provided "out of the box".
  • Standard ML Basis documentation
• Robin Milner, Mads Tofte,
  Commentary on Standard ML.
  MIT Press, 1991; CiteSeerX
  • Anyone trying to read the formal definition should start with this commentary and the 1990 definition; although the 1997 revision is now the standard, it seems to have only modified the module portion of the definition.
• Daniel K. Lee, Karl Crary, Robert Harper,
  "Mechanizing the Metatheory of Standard ML".
  Tech. Report, PDF
  • Harper and friends have produced a mechanization in Twelf of the definition of Standard ML (amazing!)

A "dialect", I suppose we could call the "primordial Ur ML" (or "pre-Standard ML").

• Christoph Kreitz and Vincent Rahli, "Introduction to Classic ML". Eprint, dated 2011.

• Martin Hotzel Escardo, Introduction to Real PCF.
• John C Mitchell,
  Foundations for Programming Languages.
  MIT Press, 1996; Chapter 2 discusses PCF, using an ML-like syntax.
• Gilles Dowek,
  Introduction to the Theory of Programming Languages. Springer, 2011; chapter 2 introduces PCF.
• Ingmar Dasseville, Marc Denecker,
  "Transpiling Programmable Computable Functions to Answer Set Programs". arXiv:1808.07770, 15 pages.
• Catuscia Palamidessi,
  "The Language PCF".
  Lecture Notes, 1998, CSE520

One major unresolved issue, for me, is whether we can articulate Standard ML in terms of category theory. It's equally unclear to me if Haskell can be articulated in terms of genuine category theory (Hask is not a category).

• G. Bellè, C. B. Jay, E. Moggi, "Functorial ML". PLILP 1996: Programming Languages: Implementations, Logics, and Programs pp 32-46 eprint
• Edward Kmett, "On Hask". Youtube, 18 July 2014 (1 hr 2 min)
• Moggi, "An Abstract View of Programming Languages" PDF

Usually people don't do pure functional programming in Standard ML (or any eager functional language). The reason stems from a series of papers:

• Nicholas Pippenger,
  "Pure versus impure Lisp".
  Argues that purely functional Lisp is not as efficient as impure Lisp.
• Richard Bird, Geraint Jones, Oege de Moor,
  "More haste, less speed: lazy versus eager evaluation".
  PDF
  • A direct response to Pippenger, showing that lazy purely functional Lisp is competitive with the eager impure Lisp.
  • The "punch line" seems to be: purely functional languages ought to be lazy, not eager.
• Robin Milner,
  "Fully abstract models of typed lambda-calculi". Theoretical Computer Science 4, no.1 (1977) 1–22, Eprint
  • Arguably, any purely functional programming language should satisfy Milner's context lemmas