Datatypes

A datatype (Def 3.1 in the slides, Chapter 5 section 3) is SML's mechanism for defining algebraic / inductive types. A datatype declaration lists constructors that build values of the type.

Simple example — enumeration:
datatype day = mon | tue | wed | thu | fri | sat | sun;

This creates seven nullary constructors; day is a type with exactly seven values. Functions over an enumeration use complete pattern matching:

Constructors with arguments:

This is the geometric-shapes example. Circle r is a value, Triangle(3.0, 4.0, 5.0) is a value, etc.

Computing on a datatype — area:

The Maybe pattern:
datatype 'a option = NONE | SOME of 'a;

This is the standard way to handle partial functions: NONE when there is no result, SOME x when there is. Pattern-matching on the constructor forces you to handle both cases. (This is exactly how SML's library represents results of TextIO.input1 and similar partial operations.)

An inductively defined set (Def 2.8) on a family of sets $N_1, \ldots, N_k$ has the form

• Closure: Every $c_i(t)$ for $t \in T_i$ is in $S$.
• No internal confusion (injectivity): Different inputs $t_1 \neq t_2$ give $c_i(t_1) \neq c_i(t_2)$ — within the same constructor.
• No inter-constructor confusion: Images of different constructors are disjoint: $\text{im}(c_i) \cap \text{im}(c_j) = \emptyset$ for $i \neq j$.
• No junk: Every element of $S$ is reachable via the constructors.

Example: $\mathbb{N}_1 = \langle \mathbb{N}, \{s, o\} \rangle$ with $o = 0$ and $s(n) = n+1$. The four conditions are exactly the Peano axioms (Def 1.6).

In SML, this is exactly what datatype declarations provide:

The 'no confusion' rules mean pattern matching is sound: case e of zero => ... | suc n => ... covers all elements exactly once.

Just as $\mathbb{N}$ is inductively defined by $\{o, s\}$, lists over $N$ are inductively defined by the constructors nil and :: (cons). The 'List Peano axioms' LP1-LP5 are:

• LP1: $\text{nil}$ is a list.
• LP2: If $a \in N$ and $l$ is a list, then $a :: l$ is a list.
• LP3 (injectivity of ::): if $a :: l_1 = a' :: l_2$ then $a = a'$ and $l_1 = l_2$.
• LP4 (disjointness): $\text{nil} \neq a :: l$ for any $a, l$.
• LP5 (induction): A property $P$ holds for all lists if (a) $P(\text{nil})$ and (b) for all $a, l$: $P(l) \Rightarrow P(a :: l)$.

Together these say lists are freely generated by nil and cons — same shape as the Peano naturals.

On the unary naturals (Peano) we can derive total functions. The same is true on lists:

Definition 2.18 (Append).
- $\text{nil} \mathbin{@} r = r$
- $(a :: l) \mathbin{@} r = a :: (l \mathbin{@} r)$

Lemma 2.20. @ is total — it terminates on all inputs.
Proof. By induction on $l$: base case $l = \text{nil}$ is trivial. Step case: $l = a :: l'$, by induction hypothesis $l' \mathbin{@} r$ terminates, then $(a :: l') \mathbin{@} r = a :: (l' \mathbin{@} r)$ terminates by construction of ::. $\square$

Corollary 2.21. (l1 @ l2) @ l3 = l1 @ (l2 @ l3) — append is associative.

Definition 2.22 (Length).
- $\lambda(\text{nil}) = o$
- $\lambda(a :: l) = s(\lambda(l))$

Definition 2.23 (Reverse).
- $\rho(\text{nil}) = \text{nil}$
- $\rho(a :: l) = \rho(l) \mathbin{@} (a :: \text{nil})$

SML's compiler emits two useful warnings on incomplete or inconsistent patterns:

• Match non-exhaustive: a case or fun does not cover all constructors.

• Match redundant: a clause is subsumed by an earlier clause.

These are not errors (SML will still produce a function — possibly raising Match at runtime for missing cases) but should be heeded.

A binary tree is defined by the recursive datatype:

Or with named leaves:

The flip function swaps the left and right subtrees of every node:

Trace. flip (Node (1, Node (2, Empty, Empty), Node (3, Empty, Empty))):
1. Outer: $x=1, l = Node(2, Empty, Empty), r = Node(3, Empty, Empty)$.
2. Inner left: flip Empty = Empty. Inner right: flip Empty = Empty. So flipped left = Node(3, Empty, Empty). Flipped right = Node(2, Empty, Empty).
3. Result: Node(1, Node(3, Empty, Empty), Node(2, Empty, Empty)).

Termination. flip terminates by structural recursion on the tree: each recursive call is on a strictly smaller subtree.

Used in assignment 5.5.