A Bluffer’s Guide to ml

Tobias Nipkow

May 2, 2000

This appendix assumes that the reader is familiar with the ideas and principles of functional programming and merely introduces (some of) their concrete syntax in ml. For a full exposition of ml see Paulson’s textbook.

To aid readability, we distinguish keywords from identifiers.

1 Types

ml is a strongly typed language. In the sequel, types are denoted by τ.

Basic types are bool, int and string. In addition to the basic types, there are type constructors for forming new types. Given a type constructor t of n arguments and types τ_{1}, …, τ_{n}, ml uses postfix syntax (τ_{1}, …, τ_{n})t to denote the compound type. If n = 1 we can write τ t instead of (τ)t. There are three predefined type constructors:

τ_{1} -> τ_{2} is the type of functions from τ_{1} to τ_{2}.

τ_{1} * ⋯ * τ_{n} is the Cartesian product τ_{1} × ⋯ × τ_{n}.

τ list is the type of lists whose elements have type τ.

Note that -> and * are infixes. To disambiguate the syntax, -> binds less tightly than *, which binds less tightly than postfix notation. Function arrows associate to the right. Therefore

int * int list -> bool -> string

is short for

(int * ((int)list)) -> (bool -> string)

Types may also contain type variables which we write α, β, etc.

2 Expressions

In the sequel, the letter e denotes an expression. If expression e has type τ we write e:τ.

2.1 Basic values

The type bool has two constants true and false. String constants are enclosed in double quotes, as in "ML".

The basic list constructors are [], the empty list, and the infix ::, which puts an element in front of a list. For example, 1::(2::[]) is the list [1,2]. A list of n elements is written [e_{1},...,e_{n}], where all elements need to have the same type, say τ, in which case the whole list has type τ list.

Tuples are written as usual: if e_{i}:τ_{i} for i = 1, …, n then (e_{1},…,e_{n}) is an expression of type τ_{1} * ⋯ * τ_{n}.

2.2 Compound expressions

Larger expressions are formed by function application. If f: τ_{1} -> τ_{2} and e:τ_{1} then f e (also written (f e) or f(e)) denotes the application of f to e and is of type τ_{2}. ml is an eager language: e is evaluated first and the result is passed to f.

If f is a function of type τ_{1} -> ⋯ -> τ_{n} -> τ we write the application of f to arguments e_{1}, …, e_{n} as f e_{1} … e_{n}. This is short for (… (f e_{1}) … e_{n}), which means that first f is applied to e_{1}, then the result to e_{2}, and so on: application associates to the left. We need not supply all of f’s arguments at once: (f e_{1}) is a perfectly legal expression of type τ_{2} -> ⋯ -> τ_{n} -> τ.

Complex expressions can be structured using the let-in-end syntax for local bindings, as in

     let val x = 42
         val y = x*x
     in y+y end

The evaluation of this expression proceeds as follows:

1. The value 42 is locally bound to x.

2. The value 1764 is locally bound to y.

3. The value of the whole expression is y+y, i.e. 3528.

This evaluation does not affect the bindings of x or y outside the expression.

3 Function declarations

Functions are declared with the keyword fun and the following syntax:

fun f x_{1} … x_{n} = e

This defines a curried function of n arguments. Its type is

τ_{1} -> ⋯ -> τ_{n} -> τ

where τ_{i} is the type of x_{i} and τ the type of e.

ml’s type system allows to deduce the type of a function automatically from its definition, so the user is not required to annotate it with types. For example, the ml system infers from the definition

     fun add1 x y = x+y+1;

that add1: int -> int -> int. You can now evaluate add1 5 7, which yields 13, or apply add1 to only one argument: add1 5 is a well-formed expression of type int -> int. In fact, you can treat add1 5 like any other function. For example,

     let val add6 = add1 5 in (add6 10) + (add6 20) end;

evaluates to 42.

Parentheses may be required to disambiguate an expression. For example, add1 add1 2 3 4 means (((add1 add1) 2) 3) 4, which is a nonsense, and should have been add1 (add1 2 3) 4.

The function add1 may only be applied to integers. ml functions can also be polymorphic, in which case they can be applied to arguments of different types. A simple example is

     fun id x = x;

where id is assigned the type α -> α because it can take arguments of an arbitrary type α and return a result of the same type. Another simple example is

     fun swap (x,y) = (y,x);

of type α * β -> β * α. At this point we have already used pattern matching, an extended form of function definition. In general, the arguments of the function being defined need not be individual variables but could be arbitrary patterns, for example

     fun perm ((x,y),z) = (z,y,x);

which has type (α * β) * γ -> γ * β * α.

Patterns are expressions which contain only variables and constructors. Standard constructors are tuples and the list constructors [] and ::. Pattern matching allows functions to be defined by a list of clauses instead of just a single one. A simple example is

(* zip: α list * β list -> (α * β) list *)

     fun zip ([], [])      = []
       | zip (x::xs, y::ys) = (x,y) :: zip(xs,ys);

Clearly zip([x_{1},...,x_{n}], [y_{1},...,y_{n}]) is [(x_{1},y_{1}),…,(x_{n},y_{n})]. The first clause takes care of the case where both lists are empty, and the second clause of the case where both lists are nonempty. Pattern matching automatically decomposes the lists into their first elements x and y and the remainders xs and ys. Note that zip is not defined if the two lists are of different lengths. In that case the execution stops with an exception at the point where zip is called with one empty and one nonempty list.

In the definition of zip, the order of the two clauses does not matter. In general, it does.

fun length (x::xs) = 1 + length(xs)

| length xs = 0

The function length has type α list -> int and computes the length of a list. The second clause is used only if the argument does not match the first clause. Reversing the order of the clauses results in a function which is 0 everywhere. Fortunately, in that case the ml system would at least issue a warning that the second clause is redundant. Variables which are not used on the rhs can be replaced by “_”:

fun length (_::xs) = 1 + length(xs)

| length _= 0

The above definition of length is not very elegant because one can write the second lhs more clearly as length [], which also removes the dependence on the order.

The generalized form of function definition is

fun f patterns_{1} = e_{1}

| f patterns_{2} = e_{2}
⋮
| f patterns_{n} = e_{n}

The declaration of mutually recursive functions uses the keyword and to separate the functions:

fun even 0 = true

| even n = odd(n-1) and odd 0 = false

| odd n = even(n-1);

Not every function must have a name. The keyword fn introduces an anonymous function: fn x => e is the function which takes an argument x and returns the result e. For example, add6 above could also be written as fn x => x+6. Pattern matching is allowed as well:

fn pattern_{1} => e_{1} | … | pattern_{n} => e_{n}

Pattern matching is also allowed in case expressions:

case e of pattern_{1} => e_{1} | … | pattern_{n} => e_{n}

The above can be regarded as a shorthand for

(fn pattern_{1} => e_{1} | … | pattern_{n} => e_{n})(e)

4 Standard functions

4.1 Booleans

The two infix operations andalso and orelse realize conditional “and” and “or”:

b_{1} andalso b_{2} is equivalent to if b_{1} then b_{2} else false;
b_{1} orelse b_{2} is equivalent to if b_{1} then true else b_{2}.

4.2 Lists

The following is a collection of standard functions from the literature, some of which are part of ml already.

(* null: α list -> bool *) fun null [] = true

       | null (_::_) = false;

(* map: (α -> β) -> α list -> β list *)

     fun map f []      = []

| map f (x::xs) = f(x) :: map f xs;

(* exists: (α -> bool) -> α list -> bool *)

fun exists p [] = false | exists p (x::xs) = p(x) orelse exists p xs;

(* forall: (α -> bool) -> α list -> bool *)

fun forall p [] = true | forall p (x::xs) = p(x) andalso forall p xs;

(* concat: α list list -> α list *)

     fun concat []      = []

| concat (x::xs) = x @ (concat xs);

The infix @ appends two lists: [x_{1}, …, x_{m}] @ [y_{1}, …, y_{n}] evaluates to [x_{1}, …, x_{m}, y_{1}, …, y_{n}].

5 Datatypes

ml offers a datatype definition facility which is strongly related to the concept of a term algebra: roughly speaking, the elements of a datatype correspond to the terms over a given signature. For example, binary trees with integer labels can be introduced as follows:

datatype btree = Mt | Node of btree * int * btree

This says that a value of type btree is either the constant Mt or of the form Node(t_{1},i,t_{2}), where i:int and t_{1}, t_{2}:btree. The functions Mt: btree and Node: btree * int * btree -> btree are called constructors because they construct the values of the datatype.

In general, a datatype definition of the form

     datatype t = C_{1} of τ_{1} | . . . | C_{n} of τ_{n}

introduces a new type t and constructor functions C_{i}: τ_{i} -> t. If C_{i} is a constant, of τ_{i} is omitted.

6 Exceptions

Exceptions arise naturally because inbuilt functions, e.g. division, but also userdefined ones, e.g. zip above, are undefined (as opposed to nonterminating) for certain arguments. In that case the function raises an exception, which interrupts the current evaluation. However, exceptions can also be handled, i.e. the interruption can be caught before it propagates to the top level. Hence there are three ml constructs dealing with exceptions:

exception E;

declares a user-defined exception named E.

raise E

is an expression which has no value but raises exception E.

e_{1} handle E => e_{2}

is an expression which is evaluated as follows. If e_{1} evaluates to a normal value, then this is the value of the whole expression. If the evaluation of e_{1} raises exception E, handle that exception by evaluating e_{2} instead. If the evaluation of e_{1} raises some other exception, the whole expression raises that exception.