SML Example

Following Code contains solutions in part to the excercises (traverse) and the exam from the Summersemester 2022 (print). It is meant to serve as a small guide to SML syntax and data types.

(* Helper function to recursively concatenate a list*)
fun concat list1 list2 = foldr (fn (head, tail) => head::tail) list1 list2;

(* Define the tree datatype *)
datatype 'a tree = empty | node of 'a * 'a tree * 'a tree;

(* Declare a tree for demonstration purporses *)
val t = node(1,node(2,node(3,empty,node(4,empty,empty)),empty),node(5,empty,empty));

(* Recursively count nodes of a tree *)
fun nodes (empty) = 0
| nodes (node (_, t1, t2)) = 1 + nodes t1 + nodes t2;

(* Recursively traverse a tree, appending values to the list *)
fun traverse (empty) = []
  | traverse (node (v, t1, t2)) = concat (concat (traverse t2) (traverse t1)) [v];

(* Recurse the tree, printing nodes in a human-readable form *)
fun print (empty) = "_"
  | print (node (v, t1, t2)) = "(" ^ (print t1) ^ ", " ^ (Int.toString v) ^ ", " ^ (print t2) ^ ")";

traverse t;
print t;

The outputs of traverse t; and print t; respectively yield

Types

Type systems help to apply and check for a syntactically consistent interpretation. They rule out programs that do not make any sense and allow certain operations while disallowing others.

Typing Relations

The Typing Relation for arithmetic expressions is the smallest binary relation between terms and types satisfying all instances of the typing rules.

A term \(t\) is typable or well-typed if there is some \(T\) such that \(t:T\).

Soundness

If \(K \vdash P\) then \(K \vDash P\) in \(T\).

If the conclusion is provable from the premise, then the premise logically entails the conclusion.

Progress

A well-typed term \(t\) is not stuck.

If \(t : T\) then either \(t\) is a value or \(t \to t^\prime\) for some \(t^\prime\)

Preservation

Types are preserved by one-step evaluation

If \(t:T\) and \(t \to t^\prime\) then \(t^\prime : T\)

Simply-Typed Lambda Calculus

Annotating terms

\(x\) is of type \(T\) is denoted as \begin{equation} \lambda x:T.t \end{equation} The type depends on the context.

Lambda Calculus

Formal system introduced by Alonzo Church in 1930. One of the two approaches that lead to the notion of an Algorithm, the other being the Turing Machine.

Variable

\(x\)

Abstraction

\(\lambda x . t\)

Application

\(t~t\)

Currying

Lambda calculus permits only functions with a single argument. \begin{align} f:(X \times Y) \mapsto Z && \text{curry}(f): X \mapsto Y \mapsto Z \end{align} Currying allows for Partial Application, which fixes the number of arguments of a function, yielding a new function with smaller arity. Example for \(f(x, y) = \lambda x . \lambda y . (x * y)\): \begin{align} (\lambda x . \lambda y . (x * y))~2 &= \lambda y . (2 * y) \end{align} By only applying one argument, to a multiplication function, you receive a function that performs a constant operation on one argument.