# Functional Programming and Specification: Examples from the lectures

Short cuts:

• ML core: lecture 1, 2, 3, 4, 5, 6, 7, 8, 9, 17
• ML modules: lecture 9, 10, 11, 12, 13
• Specification and proof: lecture 14, 15, 16

## Lecture 1

Insertion sort in Java: notice nested iteration, array, assignment, counters to keep track of array positions:
```   class Sort {
static void insertionsort( int[] a) {
int n = a.length - 1 ;
for (int i=2; i<=n; i++) {
int key = a[i] ;
int j = i-1;
while (j>0 && a[j] > key) {
a[j+1] = a[j];
j-- ;
}
a[j+1] = key;
}
}
}
```
Insertion sort in ML: notice recursion, lists, pattern matching for list decomposition and case discrimination:
```   fun insert(a,nil) = [a]
| insert(a,b::l) = if a < b then a::b::l else b::insert(a,l);

fun sort nil = nil
| sort(h::t) = insert(h,sort t);
```

## Lecture 2

Examples of bindings:
```    val m = 3+2
val pi = 3.14
val n = m+1
type count = int
```
Examples of compound declarations:
```    val pi = 3.14 ; val n = m+1

val pi = 3.14 and n = m+1
```
Reusing variables:
```    val n = 2
(* other stuff *)
val n = 3.1
```
(By the way, anything of the form (* blah blah blah *) is a comment in ML.)

Local declarations and scope:

```    val n = 3.1
val m = 2
val r = (let val m = 3 and n = 6 in m*n end) + m
```
To use Math.sqrt, which appears in the following examples, first type
```    load "Math"
```
Fourth root:
```    (fn x => Math.sqrt (Math.sqrt x))
```
Fourth root, applied to 16.0:
```    (fn x => Math.sqrt (Math.sqrt x)) 16.0
```
Naming the fourth root function using a value binding:
```    val fourthroot = fn x => Math.sqrt (Math.sqrt x)
```
allows it to be applied to 16.0 without repeating the definition:
```    fourthroot 16.0
```
A more compact syntax for defining a function and giving it a name:
```fun fourthroot x = Math.sqrt (Math.sqrt x);
```

## Lecture 3

Some more functions:
```    fun srev s = implode(rev(explode s))
fun palindrome s = s ^ (srev s)
fun square n = n*n
fun is_even n = (n mod 2 = 0)
```
Binding and scope in function expressions:
```    val x = 2.0
fun f(x:real) = x + x
fun g y = x + y
fun h x = (let val x = 2.0 in x + x end) * x
```
Examples of tuples:
```    val pair = (2,3)
val triple = (2, 2.0, "2")
val quadruple = (2, 3, 2.0, 3.0)
val pair_of_pairs = ((2, 3), (2.0, 3.0))
```
Using pattern matching to extract components of data structures:
```    val ((_,_),(r,_)) = pair_of_pairs
val ((n,m),(r,s)) = pair_of_pairs
val (_,(r,s)) = pair_of_pairs
val (p,(r,s)) = pair_of_pairs
```
Valid value bindings:
```    val (m,n) = (7+1, 4 div 2)
val (m,r,s) = (7, 7.0, "7")
val ((m,n),(r,s)) = ((4, 5), (3.1, 2.7))
val (m,n,r,s) = (4, 5, 3.1, 2.7)
```
Invalid value bindings:
```    val (m,n,r,s) = ((4, 5), (3.1, 2.7))
val (m:int, r:real) = (7+1, 4 div 2)
val (m,r) = (7, 7.0, "7")
```
```    val dist = fn (x,y) => Math.sqrt(x*x + y*y)
```
or equivalently
```    fun dist(x,y) = Math.sqrt(x*x + y*y)
```
A function with multiple arguments and multiple results:
```    fun dist2(x,y) = (Math.sqrt(x*x + y*y), abs(x-y));
```
Pattern matching can fail:
```    val (2,x) = (3,6)
```
Based on this fact, we can write clausal function definitions:
```    val iszero = fn 0 => true
| n => false
```
or equivalently
```    fun iszero 0 = true
| iszero n = false
```
But the following is NOT equivalent -- order matters!
```    fun iszero n = false
| iszero 0 = true
```

## Lecture 4

The last definition is an example of a redundant sequence of clauses. Here is another one:
```    fun not True = false
| not False = true
```
The following is non-exhaustive:
```    fn #"0" => "zero"
| #"1" => "one"
| ...
| #"9" => "nine"
```
Maybe what was meant was the following, with a catchall at the end:
```    fn #"0" => "zero"
| #"1" => "one"
| ...
| #"9" => "nine"
| _    => "dunno"
```
An example of a recursive algorithm (informal, not in ML):
To search all web pages starting at URL for a string S:
1. if S is on the page at URL, return TRUE.
2. for each link URL' on that page, search all web pages starting at URL' for S.
3. If S hasn't been found yet, return FALSE.
A simple recursive function in ML:
```    fun factorial 0 = 1
| factorial n = n * factorial(n-1)
```
The above definition of factorial is not equivalent to the following:
```    val factorial = fn 0 => 1
| n => n * factorial(n-1)
```
Rather, to the following:
```    val rec factorial = fn 0 => 1
| n => n * factorial(n-1)
```
Here's another way to define the same function. The helper function, using an "accumulator", is tail-recursive.
```    local
fun helper(0,r) = r
| helper(n,r) = helper(n-1,n*r)
in
fun factorial n = helper(n,1)
end
```
Another example of a recursive function:
```    fun fib 0 = 1
| fib 1 = 1
| fib n = fib(n-1) + fib(n-2)
```
Mutually recursive functions:
```    fun even 0 = true
| even n = odd(n-1)
and odd 0 = false
| odd n = even(n-1)
```
Functions on lists:
```    fun length nil = 0
| length(_::t) = 1 + length t

fun append(nil,l) = l
| append(h::t,l) = h :: append(t,l)
```

## Lecture 5

More functions on lists:
```    fun add nil = 0

fun front nil = nil
| front(a::nil) = nil
| front(a::b::t) = a :: front(b::t)
```
Another example of a function on lists is list reversal:
```    fun rev nil = nil
| rev(h::t) = (rev t) @ [h]
```
Another version of rev; this is a more efficient algorithm, using an accumulator, as well as being tail-recursive.
```    local
fun helper(nil,a) = a
| helper(h::t,a) = helper(t,h::a)
in
fun rev' l = helper(l,nil)
end
```
A simple non-recursive datatype, and a function that uses it:
```    datatype suit = Spades | Hearts | Diamonds | Clubs

| outranks(Hearts, Hearts) = false
| outranks(Hearts, _) = true
| outranks(Diamonds, Clubs) = true
| outranks(Diamonds, _) = false
| outranks(Clubs, _) = false
```
Another simple datatype (this one is built in):
```    datatype 'a option = NONE | SOME of 'a
```
A function with an optional parameter:
```    fun expt(NONE, n) = expt(SOME 2, n)
| expt(SOME b, 0) = 1
| expt(SOME b, n) =
if n mod 2 = 0 then expt(SOME(b*b), n div 2)
else b * expt(SOME b, n-1)
```
A function with an optional result:
```    fun divide(n, 0) = NONE
| divide(n, m) = SOME(n div m)
```
To use the result, you need to pattern match, for instance
```    fun f(n,m) =
case divide(n,m)
of NONE => 0
| SOME r => r+3
```
```    fun f(n,m) = divide(n,m) + 3
```
Here are binary trees with integer labels at each node. This is a recursive datatype.
```    datatype tree = Empty | Node of tree * int * tree
```
An example of a tree:
```    val t = Node(Node(Empty,
1,
Empty),
2,
Node(Node(Empty,
4,
Empty),
3,
Node(Node(Empty,
3,
Empty),
5,
Empty)))
```
A drawing of this tree might look like this:
```	2
/ \
/   \
1     3
/ \   / \
/   \
4     5
/ \   / \
/   \
3
/ \
```
Here is a function to compute the sum of the labels in a tree:
```    fun sum Empty = 0
| sum(Node(t1,n,t2)) = n + sum t1 + sum t2
```

## Lecture 6

Here is a function to count the number of occurrences of a given label in a tree:
```    fun occurrences(m,Empty) = 0
| occurrences(m,Node(t1,n,t2)) =
if m=n then 1 + occurrences(m,t1) + occurrences(m,t2)
else occurrences(m,t1) + occurrences(m,t2)
```
or equivalently:
```    fun occurrences(m,Empty) = 0
| occurrences(m,Node(t1,n,t2)) =
(if m=n then 1 else 0) + occurrences(m,t1) + occurrences(m,t2)
```
A variation on trees: leaves are a separate case, rather than just regarding trees of the form node(Empty,a,Empty) as leaves:
```    datatype tree = Empty | Leaf of int | Node of tree * int * tree
```
and an example of such a tree:
```    val t = Node(Leaf 1,
2,
Node(Leaf 4,
3,
Node(Leaf 3,
5,
Empty)))
```
Polymorphic binary trees, with values of any given type at each node:
```    datatype 'a tree = Empty | Node of 'a tree * 'a * 'a tree
```
And three recursive function on trees. First, the height of a tree is the length of the longest path from the root (type load "Int" first to get access to Int.max); then, the size of a tree is the number of nodes it contains:
```    fun height Empty = 0
| height(Node(t1,_,t2)) = 1 + Int.max(height t1,height t2)

fun size Empty = 0
| size(Node(t1,_,t2)) = 1 + size t1 + size t2
```
Pre-order traversal of a tree, yielding a list of its labels:
```    fun traverse Empty = nil
| traverse(Node(t1,a,t2)) = a :: (traverse t1) @ (traverse t2)
```
Trees where some nodes have two children and some have one:
```    datatype 'a tree = Empty
| Node1 of 'a tree
| Node2 of 'a tree * 'a * 'a tree
```
and an example of such a tree:
```    val t = Node2(Node1(1,Empty),
2,
Node2(Node1(4,Empty),
3,
Node1(5,
Node1(3,Empty))))
```
Trees with an arbitary number of children at each node:
```    datatype 'a tree = Empty | Node of 'a * 'a tree list
```
and an example of such a tree:
```    val t = Node(2,
[Node(1,[]),
Node(3,
[Node(4,[]),
Node(5,
[Node(3,[])])])]);
```
Binary trees with labels associated with branches rather than nodes, as a pair of mutually recursive datatypes:
```    datatype 'a tree = Empty | Node of 'a branch * 'a branch
and 'a branch = Branch of 'a * 'a tree
```
and an example of such a tree:
```    val t = Node(Branch(1,Empty),
Branch(3,Node(Branch(4,Empty),
Branch(5,Node(Branch(3,Empty),
Branch(0,Empty))))))
```
Mutually recursive functions using such trees:
```    fun treesize Empty = 0
| treesize(Node(b1,b2)) = branchsize b1 + branchsize b2
and branchsize(Branch(_,t)) = 1 + treesize t
```
If lists weren't built in, you'd be able to define them yourself:
```    datatype 'a list = nil | :: of 'a * 'a list
infix ::
```
A datatype representing the disjoint union of integers and strings:
```    datatype int_or_string = Int of int | String of string
```
We can do this in general:
```    datatype ('a,'b) union = First of 'a | Second of 'b
```
Abstract syntax for a small language of arithmetic expressions:
```    datatype expr = Numeral of int
| Plus of expr * expr
| Times of expr * expr
```
Notice how close this is to the BNF definition of (concrete) syntax:
```    expr ::= n | expr + expr | expr * expr
```
A function for evaluating expressions:
```    fun eval (Numeral n) = n
| eval (Plus (e1, e2)) = (eval e1) + (eval e2)
| eval (Times (e1, e2)) = (eval e1) * (eval e2)
```
BNF syntax for a language of expressions and commands with mutual recursion:
```    expr ::= n | x | expr + expr | expr * expr | (com; expr)
com ::= x:=expr | while expr do com
```
An ML representation of the abstract syntax:
```    datatype expr = Numeral of int
| Var of string
| Plus of expr * expr
| Times of expr * expr
| Comresult of com * expr
and com = Assign of string * expr
| While of expr * com
```
The skeleton of a function for evaluating expressions and executing commands (making reference to a store st, containing the values of variables):
```    fun eval(Numeral n) st = ...
| ...
| eval(Comresult(c,e)) st = ...  exec c ... eval e ...
and exec(Assign(s,e)) st = ... eval e ...
| exec(While(e,c)) st = ... eval e ... exec c ...
```

## Lecture 7

Function composition (this is built in as infix o):
```    fun compose(f,g) = (fn x => f(g x))
```
or alternatively:
```    fun compose(f,g) x = f(g x)
```
A function that takes a function and returns the result of composing the function with itself: fun twice f x = f(f x) or alternatively:
```    fun twice f = compose(f,f)
```
If succ is the function that increments an integer:
```    fun succ x = x+1
```
then twice succ adds two to an integer.

Generalising twice, here is a higher-order function which composes a function with itself n times:

```    fun iter(f,0) x = x
| iter(f,n) x = f(iter (f,n-1) x)
```
Alternatively, if we define the identity function
```    fun id x = x
```
then we can define the same thing as
```    fun iter(f,0) = id
| iter(f,n) = compose(f,iter(f,n-1))
```
In the following example, z will be bound to 6, not 7, since x in f will refer to the nearest syntactically enclosing declaration occurrence, even though x is re-declared before we call f:
```    val x = 2
fun f y = x + y
val x = 3
val z = f 4
```
This shows a difference between binding and assignment, and that "shadowed" bindings are not lost - the "old" binding for x is still available (through calls to f).

Here is a "curried" version of +: it takes its arguments one at a time instead of as a pair:

```    fun plus x y = x+y
```
or equivalently
```    fun plus x = fn y => x+y
```
We can apply this function to just one argument, giving a function:
```    val succ = plus 1;
```
A function to take the nth power of a number:
```    fun pow(x,0) = 1
| pow(x,n) = pow(x,n-1) * x
```
A curried version:
```    fun pow' x =
fn 0 => 1
| n => (pow' x (n-1)) * x
```
or equivalently
```    fun pow' x 0 = 1
| pow' x n = (pow' x (n-1)) * x
```
A function that turns an uncurried version of a function into a curried version:
```    fun curry f x y = f(x,y)
```
or equivalently
```    fun curry f = fn x => (fn y => f(x,y))
```
Then:
```    val plus = curry(op +)
```
Converting a curried function to an uncurried one:
```    fun uncurry f (x,y) = f x y
```
or equivalently
```    fun uncurry f = fn (x,y) => f x y
```
Applying a function to all the elements in a list (this is built in):
```    fun map f nil = nil
| map f (h::t) = (f h)::(map f t)
```
Using this to square all the elements in a list:
```    map (fn x => x*x) [1,2,3,4,5,6]
```
Accumulating a result by applying a function to pairs consisting of an element of a list and the result of a recursive application -- "folding" to the right (this is built in):
```    fun foldr f e nil = e
| foldr f e (h::t) = f(h,foldr f e t)
```
As a picture:
```      ::                   f
/  \                 / \
1    ::       =>     1   f
/  \                / \
2    ::             2   f
/  \               / \
3   nil            3   e
```
We can use this to compute length of a list:
```    fun length l = foldr(fn (x,y) => 1 + y) 0 l
```
Or sum of the integers in a list:
```    fun add l = foldr (op +) 0 l
```
Consider insertion sort:
```    fun insert(a,nil) = [a]
| insert(a,b::l) = if a < b then a::b::l else b::insert(a,l)

fun sort nil = nil
| sort(h::t) = insert(h,sort t)
```
We can implement sort using foldr:
```    val sort = foldr insert nil
```
Now, folding to the left (this is built in):
```    fun foldl f e nil = e
| foldl f e (h::t) = foldl f (f(h,e)) t
```
Foldr and foldl are similar but not the same:
```    val id = foldr (op ::) nil

val rev = foldl (op ::) nil
```

## Lecture 8

Suppose
```    fun loop(x) = loop(x+1)
```
then the following will terminate:
```    fn x => loop(17)
```
This shows that the fn construct is not strict. But despite the fact that if-then-else not strict, defining it as a function gives a strict function:
```    fun cond(x,y,z) = if x then y else z
```
The following can be used to explicitly delay and force computation:
```    type 'a delayed = unit -> 'a
fun force d = d()
```
We would like to define:
```    fun delay exp = fn () => exp
```
but since delay is then a function it will evaluate its argument which is wrong. So we have to write
```    fn () => exp
```
and think of it as delay(exp).

Now we can make any ML function into a lazy function. Suppose we have

```    fun f x = ... x ... x ...
```
where f : s -> t. Replace this by
```    fun f x = ... (force x) ... (force x) ...
```
which gives f : (s delayed) -> t, and replace each call f(exp) anywhere in the program by f(fn () => exp).

Lazy lists can be defined as follows:

```    datatype 'a llist = lnil | lcons of 'a * ('a llist) delayed
```
A function that produces an infinite list of ones:
```    fun lones() = lcons(1,lones)
```
A function that produces the infinite list of integers starting from the given one:
```    fun lfrom n = lcons(n,fn () => lfrom(n+1))
```
To access the components of such lists, we can define:
```    fun lhd(lcons(n,_)) = n

fun ltl(lcons(_,l)) = force l

fun lnth(0,l) = lhd l
| lnth(n,l) = lnth(n-1,ltl l)
```
We can use these functions to compute the infinite list of prime numbers.
```    fun lfromto(n,m) =
if n>m then lnil
else lcons(n,fn () => lfromto(n+1,m))

fun lupto n = lfromto(2,n)

fun divides(n,m) = ((m mod n) = 0)

fun lforall(p,lnil) = true
| lforall(p,lcons(a,dll)) =
p(a) andalso lforall(p,force dll)

fun lisprime n =
lforall((fn m => not(divides(m,n))), lupto(n-1))

fun lprune(p,lnil) = lnil
| lprune(p,lcons(a,dll)) =
if p(a)
then lcons(a,fn () => lprune(p,force dll))
else lprune(p,force dll)

val primes = lprune(lisprime,lfrom 2)
```
To print it (type ^C to stop):
```    fun lprint(lnil) = ()
| lprint(lcons(a:int,dll)) =
(print(Int.toString a); print "\n"; lprint(force dll))
```

## Lecture 9

The following function does not have type 'a * 'a list -> bool:
```    fun member(x,nil) = false
| member(x,h::t) = (x=h) orelse member(x,t)
```
It has type ''a * ''a list -> bool, where ''a can be instantiated by any type that admits equality. The following types, and all other types that involve function types in some way, don't admit equality:
```    int->bool * string

(int->bool) list

int llist
```
where
```    datatype 'a llist = lnil | lcons of 'a * unit -> ('a llist);
```

Alternatively, we could pass the comparison function in as a parameter:

```    fun member'(x,p,nil) = false
| member'(x,p,h::t) = p(x,h) orelse member'(x,p,t)
```
A signature for polymorphic queues:
```    signature QUEUE =
sig
type 'a queue
exception Empty
val empty : 'a queue
val insert : 'a * 'a queue -> 'a queue
val remove : 'a queue -> 'a * 'a queue
end
```
```    signature QUEUE_WITH_ISEMPTY =
sig
include QUEUE
val is_empty : 'a queue -> bool
end
```
There's no difference between this and writing it out in full:
```    signature QUEUE_WITH_ISEMPTY =
sig
type 'a queue
exception Empty
val empty : 'a queue
val insert : 'a * 'a queue -> 'a queue
val remove : 'a queue -> 'a * 'a queue
val is_empty : 'a queue -> bool
end
```
```    signature QUEUE_AS_LISTS =
QUEUE where type 'a queue = 'a list * 'a list
```
You can't redefine a type that is already defined, so the following is illegal:
```    signature QUEUE_AS_LISTS_AS_LIST =
QUEUE_AS_LISTS where type 'a queue = 'a list
```
You have to go back to an "ancestor" where the type is not yet defined:
```    signature QUEUE_AS_LIST =
QUEUE where type 'a queue = 'a list
```
The equivalences given by type definitions extend to uses of these types in the signature. So the above signature is equivalent to the following:
```    signature QUEUE_AS_LIST =
sig
type 'a queue = 'a list
exception Empty
val empty : 'a list
val insert : 'a * 'a list -> 'a list
val remove : 'a list -> 'a * 'a list
end
```

## Lecture 10

A structure implementing polymorphic queues:
```    structure Queue =
struct
type 'a queue = 'a list * 'a list
exception Empty
val empty = (nil,nil)
fun insert (x, (bs,fs)) = (x::bs, fs)
fun remove (nil, nil) = raise Empty
| remove (bs, nil) = remove (nil, rev bs)
| remove (bs, f::fs) = (f, (bs, fs))
end
```
If you get tired of writing things like
```    val q = Queue.insert(2,Queue.insert(1,Queue.empty))
```
you can introduce a shorter structure identifier
```    structure Q = Queue
```
then
```    val q = Q.insert(2,Q.insert(1,Q.empty))
```
Alternatively, write
```    open Queue
```
then
```    val q = insert (2, insert (1, empty))
```
But note that this is almost always poor style and so is better avoided.

Consider the signatures QUEUE, QUEUE_WITH_ISEMPTY and QUEUE_AS_LISTS above.

1. QUEUE_WITH_ISEMPTY matches QUEUE but not vice versa, since QUEUE doesn't contain is_empty.
2. QUEUE_AS_LISTS matches QUEUE but not vice versa, since QUEUE doesn't satisfy 'a queue = 'a list * 'a list.
The signature
```    signature MERGEABLE_QUEUE =
sig
include QUEUE
val merge : 'a queue * 'a queue -> 'a queue
end
```
matches the signature
```    signature MERGEABLE_INT_QUEUE =
sig
include QUEUE
val merge : int queue * int queue -> int queue
end
```
because the type of merge in MERGEABLE_INT_QUEUE is an instantiation of its type in MERGEABLE_QUEUE.

A datatype specification matches a signature that specifies that type and ordinary values corresponding to the constructors:

```    signature RBT_DT =
sig
datatype 'a rbt =
Empty |
Red of 'a rbt * 'a * 'a rbt |
Black of 'a rbt * 'a * 'a rbt
end
```
matches the signature
```    signature RBT =
sig
type 'a rbt
val Empty : 'a rbt
val Red : 'a rbt * 'a * 'a rbt -> 'a rbt
end
```

## Lecture 11

Queues as pairs of lists, with opaque ascription:
```    signature QUEUE =
sig
type 'a queue
exception Empty
val empty : 'a queue
val insert : 'a * 'a queue -> 'a queue
val remove : 'a queue -> 'a * 'a queue
end

structure Queue :> QUEUE =
struct
type 'a queue = 'a list * 'a list
exception Empty
val empty = (nil, nil)
fun insert (x, (bs,fs)) = (x::bs, fs)
fun remove (nil, nil) = raise Empty
| remove (bs, nil) = remove (nil, rev bs)
| remove (bs, f::fs) = (f, (bs, fs))
end
```
An implementation of priority queues, which maintains a representation invariant (queues are ordered with respect to lt):
```    signature PQ =
sig
type elt
val lt : elt * elt -> bool
type queue
exception Empty
val empty : queue
val insert : elt * queue -> queue
val remove : queue -> elt * queue
end

structure PrioQueue :> PQ =
struct
type elt = string
val lt : string * string -> bool = op <
type queue = string list
val empty = nil
fun insert(x,nil) = [x]
| insert(x,y::l) =
if lt(x,y) then x::y::l else y::insert(x,l)
exception Empty
fun remove nil = raise Empty
| remove(x::l) = (x,l)
end
```
To check that the invariant always holds, we just have to check:
1. empty produces an ordered queue: Ord(empty)
2. insert maintains this property: Ord(q) => Ord(insert(x,q))
3. so does remove: Ord(q) and q<>empty => let val (x,q') = remove q in Ord(q') end
where Ord(q) means that elements in q are kept in order according to lt.

PQ is too abstract; the following is ill-typed:

```    PrioQueue.insert("abc",PrioQueue.empty)
```
We can fix the problem by augmenting PQ with a definition for elt:
```    signature STRING_PQ = PQ where type elt = string

structure PrioQueue :> STRING_PQ = ... as before ...
```
A signature for a type together with an order relation:
```    signature ORDERED =
sig
type t
val lt : t * t -> bool
end
```
and some structures with this signature ascribed transparently:
```    structure String : ORDERED =
struct
type t = string
val clt = Char.<
fun lt(s,t) = ... clt ...
end

structure IntLt : ORDERED =
struct
type t = int
val lt = (op <)
end

structure IntDiv : ORDERED =
struct
type t = int
fun lt (m, n) = (n mod m = 0)
end
```
Suppose we are building a system, and we need to use dictionaries having strings as search keys:
```    signature MY_STRING_DICT =
sig
type 'a dict
val empty : 'a dict
val insert : 'a dict * string * 'a -> 'a dict
val lookup : 'a dict * string -> 'a option
end

structure MyStringDict :> MY_STRING_DICT = ...
```
Later on, we need something similar but with integers as search keys:
```    signature MY_INT_DICT =
sig
type 'a dict
val empty : 'a dict
val insert : 'a dict * int * 'a -> 'a dict
val lookup : 'a dict * int -> 'a option
end

structure MyIntDict :> MY_INT_DICT = ...
```
To avoid repetition, we abstract out the key type:
```    signature MY_GEN_DICT =
sig
type key
type 'a dict
val empty : 'a dict
val insert : 'a dict * key * 'a -> 'a dict
val lookup : 'a dict * key -> 'a option
end
```
Then we can obtain specific instances using "where type":
```    signature MY_STRING_DICT =
MY_GEN_DICT where type key = string

signature MY_INT_DICT =
MY_GEN_DICT where type key = int
```
Now suppose that we need two different dictionaries with integers as keys. The first is this:
```    structure MyIntDict :> MY_INT_DICT =
struct
type key = int
datatype 'a dict =
Empty |
Node of 'a dict * key * 'a * 'a dict
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if k < l then Node(insert(dl, k, v'), l, v, dr)
else if l < k then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if k < l then lookup(dl, k)
else if l < k then lookup(dr, k)
else SOME v
end
```
For the other, we need to order keys according to divisibility:
```    structure MyIntDivDict :> MY_INT_DICT =
struct
type key = int
datatype 'a dict =
Empty |
Node of 'a dict * key * 'a * 'a dict
fun divides (k, l) = (l mod k = 0)
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if divides(k, l) then Node(insert(dl, k, v'), l, v, dr)
else if divides(l, k) then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if divides(k, l) then lookup(dl, k)
else if divides(l, k) then lookup(dr, k)
else SOME v
end
```

## Lecture 12

We can abstract out the type of keys together with the way that they are being interpreted using substructures. We start with the notion of an ordered type:
```    signature ORDERED =
sig
type t
val lt : t * t -> bool
end

structure String : ORDERED =
struct
type t = string
val lt = (op <)
end

structure IntLt : ORDERED =
struct
type t = int
val lt = (op <)
end

structure IntDiv : ORDERED =
struct
type t = int
fun lt(m, n) = (n mod m = 0)
end
```
Then we use this for the signature of dictionaries:
```    signature DICT =
sig
structure Key : ORDERED
type 'a dict
val empty : 'a dict
val insert : 'a dict * Key.t * 'a -> 'a dict
val lookup : 'a dict * Key.t -> 'a option
end

signature STRING_DICT =
DICT where type Key.t=string

signature INT_DICT =
DICT where type Key.t=int
```
Then we have the implementation:
```    structure StringDict :> STRING_DICT =
struct
structure Key : ORDERED = String
datatype 'a dict =
Empty |
Node of 'a dict * Key.t * 'a * 'a dict
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if Key.lt(k, l) then Node(insert(dl, k, v'), l, v, dr)
else if Key.lt(l, k) then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if Key.lt(k, l) then lookup(dl, k)
else if Key.lt(l, k) then lookup(dr, k)
else SOME v
end

structure IntLtDict :> INT_DICT =
struct
structure Key : ORDERED = IntLt
... as with StringDict ...
end

structure IntDivDict :> INT_DICT =
struct
structure Key : ORDERED = IntDiv
... as with StringDict ...
end
```
Here's the above example again, with STRING_DICT replaced by its definition:
```    structure StringDict :> DICT where type Key.t=string =
struct
structure Key : ORDERED = String
datatype 'a dict =
Empty |
Node of 'a dict * Key.t * 'a * 'a dict
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if Key.lt(k, l) then Node(insert(dl, k, v'), l, v, dr)
else if Key.lt(l, k) then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if Key.lt(k, l) then lookup(dl, k)
else if Key.lt(l, k) then lookup(dr, k)
else SOME v
end
```
We can make this into a functor that defines the implementation of dictionaries parametrically in the choice of keys:
```    functor DictFun
(structure K : ORDERED) :>
DICT where type Key.t = K.t =
struct
structure Key : ORDERED = K
datatype 'a dict =
Empty |
Node of 'a dict * Key.t * 'a * 'a dict
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if Key.lt(k, l) then Node(insert(dl, k, v'), l, v, dr)
else if Key.lt(l, k) then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if Key.lt(k, l) then lookup(dl, k)
else if Key.lt(l, k) then lookup(dr, k)
else SOME v
end
```
Instantiation is by application:
```    structure String : ORDERED =
struct
type t = string
val lt = (op <)
end

structure StringDict = DictFun (structure K = String)

structure IntLt : ORDERED =
struct
type t = int
val lt = (op <)
end

structure IntLtDict = DictFun (structure K = IntLt)

structure IntDiv : ORDERED =
struct
type t = int
fun lt(m, n) = (n mod m = 0)
end

structure IntDivDict = DictFun (structure K = IntDiv)
```
It is very natural to make the result of a functor include a copy of the argument. Look what happens when we try to avoid this. First, the code without the result signature:
```    functor DictFun
(structure K : ORDERED) :> ... =
struct
datatype 'a dict =
Empty |
Node of 'a dict * K.t * 'a * 'a dict
val empty = Empty
fun insert(Empty, k, v) = Node(Empty, k, v, Empty)
| insert(Node(dl, l, v, dr), k, v') =
if K.lt(k, l) then Node(insert(dl, k, v'), l, v, dr)
else if K.lt(l, k) then Node(dl, l, v, insert(dr, k, v'))
else Node(dl, l, v', dr)
fun lookup(Empty, _) = NONE
| lookup(Node (dl, l, v, dr), k) =
if K.lt(k, l) then lookup(dl, k)
else if K.lt(l, k) then lookup(dr, k)
else SOME v
end
```
The problem comes when we try to fill in the result signature. How do we express the types of insert and lookup if Key is not available? We can do it:
```    functor DictFun
(structure K : ORDERED) :>
sig
type 'a dict
val empty : 'a dict
val insert : 'a dict * K.t * 'a -> 'a dict
val lookup : 'a dict * K.t -> 'a option
end =
struct
...
end
```
but the result signature can't be defined outside the scope of the parameter.

## Lecture 13

Consider the following example:
```    signature GEOMETRY =
sig
structure Point : POINT
structure Sphere : SPHERE
end
```
To specify the signature POINT, we use another signature, VECTOR:
```    signature VECTOR =
sig
type vector
val zero : vector
val scale : real * vector -> vector
val add : vector * vector -> vector
val dot : vector * vector -> real
end
```
Then points are:
```    signature POINT =
sig
structure Vector : VECTOR
type point
val translate : point * Vector.vector -> point
val ray : point * point -> Vector.vector
end
```
Spheres are now given by:
```    signature SPHERE =
sig
structure Vector : VECTOR
structure Point : POINT
type sphere
val sphere : Point.point * Vector.vector -> sphere
end
```
Now suppose we use GEOMETRY in opaque signature ascriptions to create two versions of geometry, one for 2D and one for 3D:
```    structure Geom2D :> GEOMETRY = ...
structure Geom3D :> GEOMETRY = ...
```
With these two versions of geometry, there is a potential problem: we could easily get confused between the two different versions. But opaque ascription prevents this; consider
```    Geom3D.Sphere.sphere (p, Geom2D.Point.ray (p, q))
```
where p,q : Geom2D.Point.point This is ill-typed because there is nothing guaranteeing that Geom2D.Point.Vector.vector = Geom3D.Sphere.Vector.vector.

Unfortunately, opaque ascription also prevents us from using either version when we are not confused; consider

```    Geom2D.Sphere.sphere (p, Geom2D.Point.ray (p, q))
```
where p,q : Geom2D.Point.point -- this is also ill-typed, since there is nothing guaranteeing that Geom2D.Point.Vector.vector = Geom2D.Sphere.Vector.vector.

To get the different versions of points/vectors in Geom2D and in Geom3D to be the same, we use a type sharing constraint:

```    signature SPHERE =
sig
structure Vector : VECTOR
structure Point : POINT
sharing type Point.Vector.vector = Vector.vector
type sphere
val sphere : Point.point * Vector.vector -> sphere
end

signature GEOMETRY =
sig
structure Point : POINT
structure Sphere : SPHERE
sharing type Point.point = Sphere.Point.point
sharing type Point.Vector.vector = Sphere.Vector.vector
end
```
We can make this a little shorter using structure sharing constraints:
```    signature SPHERE =
sig
structure Vector : VECTOR
structure Point : POINT
sharing Point.Vector = Vector
type sphere
val sphere : Point.point * Vector.vector -> sphere
end

signature GEOMETRY =
sig
structure Point : POINT
structure Sphere : SPHERE
sharing Point = Sphere.Point
sharing Point.Vector = Sphere.Vector
end
```
These sharing constraints are constraints on the implementations of Geom2D and Geom3D:
```    structure Vector3D : VECTOR = ...

structure Point3D : POINT =
struct
structure Vector : VECTOR = Vector3D
...
end

structure Sphere3D : SPHERE =
struct
structure Vector : VECTOR = Vector3D
structure Point : POINT = Point3D
...
end

structure Geom3D :> GEOMETRY =
struct
structure Point = Point3D
structure Sphere = Sphere3D
end
```
For instance, we have Geom3D.Point.point = Geom3D.Sphere.Point.point because
```    Geom3D.Point.point = Point3D.point
Geom3D.Sphere.Point.point = Sphere3D.Point.point = Point3D.point
```
The following does not obey these constraints, and would not be accepted:
```    structure Geom3D' :> GEOMETRY =
struct
structure Point = Point3D
structure Sphere = Sphere2D
end
```
We don't have Geom3D'.Point.point = Geom3D'.Sphere.Point.point:
```    Geom3D'.Point.point = Point3D.point
Geom3D'.Sphere.Point.point = Sphere2D.Point.point = Point2D.point
```
and Point3D.point is different from Point2D.point.

We can implement various components in this system as functors:

```    functor PointFun (structure V : VECTOR) : POINT =
struct
structure Vector = V
...
end

functor SphereFun (structure V : VECTOR
structure P : POINT) : SPHERE =
struct
structure Vector = V
structure Point = P
...
end

functor GeomFun (structure P : POINT
structure S : SPHERE) : GEOMETRY =
struct
structure Point = P
structure Sphere = S
end
```
Then 2D geometry may be defined by instantiating these:
```    structure Vector2D : VECTOR = ...

structure Point2D : POINT =
PointFun (structure V = Vector2D)

structure Sphere2D : SPHERE =
SphereFun (structure V = Vector2D
structure P = Point2D)

structure Geometry2D : GEOMETRY =
GeomFun (structure P = Point2D
structure S = Sphere2D)
```
But now SphereFun and GeomFun aren't well-typed -- their result signatures require type equations that aren't necessarily true of their parameters!

The solution is to include sharing constraints in the parameter lists of these functors:

```    functor SphereFun (structure V : VECTOR
structure P : POINT
sharing P.Vector = V) : SPHERE =
struct
structure Vector = V
structure Point = P
...
end

functor GeomFun (structure P : POINT
structure S : SPHERE
sharing P.Vector = S.Vector
sharing P = S.Point) : GEOMETRY =
struct
structure Point = P
structure Sphere = S
end
```

## Lecture 14

Specification of the square root of a real number, first version:
```    sqrt : real -> real

sqrt(a) * sqrt(a) = a
```
Specification of matrix inversion (assuming that we have defined a datatype of matrices, matrix multiplication and the identity matrix), first version:
```    inv : matrix -> matrix

inv(A) * A = I
A * inv(A) = I
```
An improved version of the specification of square root, which only requires it to work for non-negative numbers:
```    a >= 0.0 implies sqrt(a) * sqrt(a) = a
```
An improved version of the specification of matrix inversion, which takes into account that some matrices are not invertible:
```    Exists B => (B*A=I andalso A*B=I)
implies
inv(A) * A = I andalso A * inv(A) = I
```
And with explicit universal quantification (required in Extended ML):
```    Forall A =>
(Exists B => (B*A=I andalso A*B=I)
implies
inv(A) * A = I andalso A * inv(A) = I)
```
Specification of the maximum element of an int list:
```    maxelem : int list -> int

Forall l => l<>nil implies member(maxelem l, l)
Forall (a,l) => member(a,l) implies (maxelem l) >= a
```
Specification of string searching, with before producing the part of the string before the first occurrence of the search key and after producing the part of the string after the first occurrence of the search key, first version:
```    before : string * string -> string
after : string * string -> string

Forall (s,r) =>
before(s,r) ^ s ^ after(s,r) = r

Forall (s,r) => Forall (t1,t2) =>
t1^s^t2=r implies String.isPrefix (before(s,r)) t1
```
An improved version of the specification of string searching, which allows that the search key may not be present in the string:
```    substring : string * string -> bool,

Forall (s,r) =>
substring(s,r) iff (Exists (t1,t2) => t1^s^t2=r)

before : string * string -> string
after : string * string -> string

Forall (s,r) =>
substring(s,r) implies before(s,r) ^ s ^ after(s,r) = r

Forall (s,r) => Forall (t1,t2) =>
t1^s^t2=r implies String.isPrefix (before(s,r)) t1
```
Another version of the specification of square root, which only requires it to be accurate to within 1%:
```    Forall a =>
a >= 0.0 implies
sqrt(a) * sqrt(a) >= 0.99*a
andalso
sqrt(a) * sqrt(a) <= 1.01*a
```

## Lecture 15

Remember the tail-recursive version of factorial:
```    local
fun helper(0,r) = r
| helper(n,r) = helper(n-1,n*r)
in
fun factorial n = helper(n,1)
end
```
Here is a proof that this definition computes the correct answer.
```    Theorem: for all n>=0, factorial n = n!

We prove this using the following lemma:

Lemma: for all n>=0, for all r, helper(n,r) = n!*r

Proof of the Theorem using the Lemma:
factorial n = helper(n,1) [by the definition of factorial]
= n!*1 [by the lemma]
= n!

Proof of the Lemma by induction on n:
Base case: n=0
helper(0,r) = r
= 0!*r

Step case: n=m+1 for m>=0
Inductive hypothesis (IH): for all r, helper(m,r)=m!*r
To prove: helper(m+1,r) = (m+1)!*r
helper(m+1,r) = helper(m,(m+1)*r) [by the definition of helper]
= m!*(m+1)*r  [by IH]
= (m+1)!*r [by the definition of !]
```
Another proof by induction (this was posed as an exercise in the lecture - try it before looking at the answer):
```  Define  sum n = 0 + 1 + ... + n-1 + n   for n>=0

Theorem: for all n>=0, sum n = n*(n+1)/2

Proof by induction on n:

Base case: n=0
sum 0 = 0
= 0*(0+1)/2

Step case: n=m+1 for m>=0
Inductive hypothesis (IH): sum m = m*(m+1)/2
To prove: sum(m+1) = (m+1)*((m+1)+1)/2
sum(m+1) = 0 + 1 + ... + m + (m+1)
= sum m + (m+1)
= m*(m+1)/2 + (m+1)  [by IH]
= (m^2 + 3*m + 2)/2
= (m+1)*(m+2)/2
= (m+1)*((m+1)+1)/2
```
A related proof method is structural induction on lists, which can be seen as induction as above but on the size of the list.
```    To prove Forall l. P(l)
1. Base case: Prove P(nil)
2. Step case: Assume P(t) [the inductive hypotheses]
and prove P(h::t)
```
Given the declaration
```    datatype 'a tree = Empty | Node of 'a tree * 'a * 'a tree
```
we get the following structural induction principle:
```    To prove Forall t. P(t)
1. Base case: Prove P(Empty)
2. Step case: Assume P(t) and P(t') [the inductive hypotheses]
and prove P(Node(t,x,t'))
```
Recall the functions:
```    fun height Empty = 0
| height(Node(t1,_,t2)) = 1 + Int.max(height t1,height t2)

fun size Empty = 0
| size(Node(t1,_,t2)) = 1 + size t1 + size t2
```
We can use structural induction on trees to prove a theorem about them:
```    Theorem: Forall t. size t >= height t

Proof: By induction on t.

Base case: t=Empty
size Empty = 0 = height Empty   OK

Step case: t=Node(t1,x,t2)
Inductive hypothesis 1: size t1 >= height t1
Inductive hypothesis 2: size t2 >= height t2
To prove: size(Node(t1,x,t2)) >= height(Node(t1,x,t2))

size(Node(t1,x,t2))
= 1 + size t1 + size t2
>= 1 + height t1 + size t2  [by IH1]
>= 1 + height t1 + height t2  [by IH2]
>= 1 + Int.max(height t1, height t2)  [property of Int.max]
= height(Node(t1,x,t2))   OK
```
Given the declaration
```    datatype 'a tree = Empty
| Leaf of 'a
| Node1 of 'a * 'a tree
| Node2 of 'a tree * 'a * 'a tree
```
we get the following structural induction principle:
```    To prove Forall t. P(t)
1. Base case for Empty: Prove P(Empty)
2. Base case for Leaf: Prove P(Leaf(x)) for all x
3. Step case for Node1: Assume P(t) and prove P(Node1(x,t))
4. Step case for Node2: Assume P(t) and P(t') and prove P(Node2(t,x,t'))
```
Things get more complicated with mutually recursive datatypes, or when one recursive datatype is used in the definition of another. Try to formulate structural induction principles for the following types:
```    datatype 'a tree = Empty | Node of 'a * 'a tree list

datatype expr = Numeral of int
| Var of string
| Plus of expr * expr
| Times of expr * expr
| Comresult of com * expr
and com = Assign of string * expr
| While of expr * com
```
Some user-defined types do not give rise to an induction principle, for instance
```    datatype D = Int of int | Fun of D->D
```

## Lecture 16

Here is a structure that implements an unbounded array of integers indexed starting from 0, using a list of integers to represent the array:
```    structure Array =
struct
type array = int list
val empty = nil
fun put(n,v,nil) = if n=0 then v::nil else 0::put(n-1,v,nil)
| put(n,v,w::l) = if n=0 then v::l else w::put(n-1,v,l)
fun retrieve(n,nil) = 0
| retrieve(n,v::l) = if n=0 then v else retrieve(n-1,l)
end
```
We can specify this just as if it were two independent functions Array.retrieve and Array.put and a value Array.empty, using the following axioms:
```    Forall (n,v,w,l) => Array.put(n,v,Array.put(n,w,l)) = Array.put(n,v,l)
Forall (n,m,v,w,l) => n<>m implies Array.put(n,v,Array.put(m,w,l)) = Array.put(m,w,Array.put(n,v,l))
Forall n => Array.retrieve(n,Array.empty) = 0
Forall (n,v,l) => Array.retrieve(n,Array.put(n,v,l)) = v
Forall (n,m,v,l) => n<>m implies Array.retrieve(n,Array.put(m,v,l)) = Array.retrieve(n,l)
```
The signature of Array is:
```    signature ARRAY =
sig
type array
val empty : array
val put : int * int * array -> array
val retrieve : int * array -> int
end
```
Adding the axioms to form a more complete interface gives:
```    signature ARRAY =
sig
type array
val empty : array
val put : int * int * array -> array
val retrieve : int * array -> int
axiom Forall (n,v,w,l) => put(n,v,put(n,w,l)) = put(n,v,l)
axiom Forall (n,m,v,w,l) => n<>m implies put(n,v,put(m,w,l)) = put(m,w,put(n,v,l))
axiom Forall n => retrieve(n,empty) = 0
axiom Forall (n,v,l) => retrieve(n,put(n,v,l)) = v
axiom Forall (n,m,v,l) => n<>m implies retrieve(n,put(m,v,l)) = retrieve(n,l)
end
```
In Extended ML, in addition to computational equality, we have logical equality == : 'a * 'a -> bool for comparing values of arbitrary type. A better version of ARRAY, using logical equality:
```    signature ARRAY =
sig
type array
val empty : array
val put : int * int * array -> array
val retrieve : int * array -> int
axiom Forall (n,v,w,l) => put(n,v,put(n,w,l)) == put(n,v,l)
axiom Forall (n,m,v,w,l) => n<>m implies put(n,v,put(m,w,l)) == put(m,w,put(n,v,l))
axiom Forall n => retrieve(n,empty) == 0
axiom Forall (n,v,l) => retrieve(n,put(n,v,l)) == v
axiom Forall (n,m,v,l) => n<>m implies retrieve(n,put(m,v,l)) == retrieve(n,l)
end
```
We can ascribe this signature to Array, using the usual syntax:
```    structure Array :> ARRAY =
struct
type array = int list
. . .
end
```
We can specify Array without providing an implementation by using a question mark in place of the structure body:
```    structure Array :> ARRAY = ?
```
Or we can provide a partial implementation by including some definitions but omitting others:
```    structure Array :> ARRAY =
struct
type array = int list
val empty = nil
fun put(n,v,nil) = if n=0 then v::nil else 0::put(n-1,v,nil)
| put(n,v,w::l) = if n=0 then v::l else w::put(n-1,v,l)
fun retrieve(n,nil) = 0
| retrieve(n,v::l) = ?
end
```
We haven't decided how to implement retrieve but we do know what properties it is supposed to satisfy, namely the ones from ARRAY that mention it. We can add these to the structure in place of the missing code:
```    structure Array :> ARRAY =
struct
type array = int list
val empty = nil
fun put(n,v,nil) = if n=0 then v::nil else 0::put(n-1,v,nil)
| put(n,v,w::l) = if n=0 then v::l else w::put(n-1,v,l)
fun retrieve(n,nil) = 0
| retrieve(n,v::l) = ?
axiom Forall (n,v,l) => retrieve(n,put(n,v,l)) == v
axiom Forall (n,m,v,l) => n<>m implies retrieve(n,put(m,v,l)) == retrieve(n,l)
end
```
Here is a specification of a structure containing functions for creating, updating and displaying a histogram:
```    signature HISTOGRAM =
sig
structure A : ARRAY
type histogram
val create : histogram
val incrementcount : int * histogram -> histogram
val display : histogram -> A.array
local
val count : int * histogram -> int
axiom Forall n => count(n,create) = 0
axiom Forall (n,h) => count(n,incrementcount(n,h)) = 1 + count(n,h)
axiom Forall (n,m,h) => n<>m implies count(n,incrementcount(m,h)) = count(n,h)
in
axiom Forall (n,h) => A.retrieve(n,display h) = count(n,h)
end
end

structure Histogram :> HISTOGRAM = ?
```
This specification can be implemented by representing histograms as arrays and using the identity function for display:
```    structure Histogram :> HISTOGRAM =
struct
structure A : ARRAY = Array
type histogram = A.array
val create = A.empty
fun incrementcount(n,h) = A.put(n, 1 + A.retrieve(n,h), h)
fun display h = h
end
```
If we want the result of display to be the same kind of arrays as used elsewhere in the system rather than allowing some other implementation of arrays, we need a sharing constraint:
```    structure Histogram :> HISTOGRAM where type A.array = Array.array = ?
```
Equivalently, we can add the sharing constraint to HISTOGRAM by writing
```    structure A : ARRAY sharing type A.array = Array.array
```
Now, suppose that we have already shown that Histogram.A (i.e. Array) satisfies ARRAY. To prove that Histogram satisfies HISTOGRAM, we then have to show that the functions and constants in Histogram (create, incrementcount and display), satisfy the axiom in HISTOGRAM:
```    Forall (n,h) => A.retrieve(n,display h) = count(n,h)
```
where count is defined by the "hidden" axioms in HISTOGRAM:
```    Forall n => count(n,create) = 0
Forall (n,h) => count(n,incrementcount(n,h)) = 1 + count(n,h)
Forall (n,m,h) => n<>m implies count(n,incrementcount(m,h)) = count(n,h)
```
and A satisfies ARRAY. A sorting functor is specified as follows:
```    signature PO =
sig
type t
val le : t * t -> bool
axiom Forall x => le(x,x)
axiom Forall (x,y,z) => le(x,y) andalso le(y,z) implies le(x,z)
axiom Forall (x,y) => le(x,y) andalso le(y,x) implies x=y
axiom Forall (x,y) => le(x,y) orelse le(y,x)
end

signature SORT =
sig
structure OBJ : PO
local
val count : 'a * 'a list -> int
axiom Forall a => count(a,nil) = 0
axiom Forall (a,l) => count(a,a::l) = 1+count(a,l)
axiom Forall (a,b,l) => a<>b implies count(a,b::l) = count(a,l)
val permutation : 'a list * 'a list -> bool
axiom Forall (l,l') =>
permutation(l,l') = (Forall x => count(x,l) = count(x,l'))
val ordered : OBJ.t list -> bool
axiom Forall l =>
ordered l iff
(Forall (a,b,c,x,y) =>
l=a@[x]@b@[y]@c implies OBJ.le(x,y))
in
val sort : OBJ.t list -> OBJ.t list
axiom Forall l => permutation(l,sort l)
axiom Forall l => ordered(sort l)
end
end

functor Sort(X : PO) :> SORT where type OBJ.t=X.t = ?
```
As before, we can provide a body that is partly executable:
```    functor Sort(X : PO) :> SORT where type OBJ.t=X.t =
struct
structure OBJ = X

val partition : OBJ.t * OBJ.t list -> (OBJ.t list * OBJ.t list) = ?
axiom Forall (a,l) =>
let val (l1,l2) = partition(a,l)
in  Forall b => member(b,l1) implies OBJ.le(b,a)
andalso
Forall c => member(c,l2) implies not(OBJ.le(c,a))
andalso
Forall d => member(d,l) iff member(d,l1) orelse member(d,l2)
end

fun sort nil = nil
| sort(a::l) = let val (l1,l2) = partition(a,l)
in  (sort l1)@(a::(sort l2))
end
end
```
A complete executable version is then:
```    functor Sort(X : PO) :> SORT where type OBJ.t=X.t =
struct
structure OBJ = X
fun partition(a,nil) = (nil,nil)
| partition(a,b::l) =
let val (l1,l2) = partition(a,l)
in  if OBJ.le(b,a) then (b::l1,l2) else (l1,b::l2)
end
fun sort nil = nil
| sort(a::l) = let val (l1,l2) = partition(a,l)
in  (sort l1)@(a::(sort l2))
end
end
```

## Lecture 17

#### Returning to the ML core language

The following raise built-in exceptions (Div and Overflow respectively):
```    3 div 0

1000000000 + 1000000000
```
If we define
```    fun hd(h::_) = h
```
then the following raises Match:
```    hd nil
```
The following raises Bind:
```    let val h::t = nil in ...anything... end
```
Users can define new exceptions and raise them in programs:
```    exception Factorial

fun checked_factorial n =
if n<0 then raise Factorial
else if n=0 then 1
else n * checked_factorial(n-1)
```
Alternatively, to avoid checking if n<0 on every recursive call and to take advantage of pattern matching:
```    exception Factorial

local
fun fact 0 = 1
| fact n = n * fact(n-1)
in
fun checked_factorial n =
if n<0 then raise Factorial
else fact n
end
```
It is possible to "catch" an exception and deal with it under program control:
```    fun recover_factorial n =
checked_factorial n handle Factorial => 0
```
Here's a more complicated version, involving several exceptions:
```    fun recover_factorial n =
checked_factorial n handle Factorial => 0
| Overflow => ~1
```
Exceptions can carry values:
```    exception Divide of int

fun divide(x,0) = raise Divide x
| divide(x,y) = x div y
```
A function for changing a quantity of money using a list of coin denominations, using exceptions to implement backtracking:
```    exception Change

fun change _ 0 = nil
| change nil _ = raise Change
| change (coin::coins) amt =
if coin > amt then change coins amt
else (coin :: change (coin::coins) (amt-coin))
handle Change => change coins amt
```
```    datatype 'a dllist = endmarker
| cell of 'a * ('a dllist) ref * ('a dllist) ref
```
An example showing the difference between references and ordinary ML variables:
```    val x = 1
fun f(y) = let val x=x+1 in x+y end
```
Now f(3)=5 and f(3) a second time gives 5 again.
```    val x = ref 1
fun f(y) = let val _ = x := !x + 1 in !x + y end
```
Now f(3)=5 and f(3) a second time gives 6.

Here is an iterative version of factorial:

```    fun ifac N =
let val n = ref N and i = ref 1
in
while !n <> 0 do
(i := !i * !n; n := !n - 1);
!i
end
```
Sharing private state between functions:
```    local
val counter = ref 0
in
fun reset() = (counter := 0)
fun tick() = (counter := !counter + 1; !counter)
end
```
A counter generator that produces new counters with reset/tick:
```    fun new_counter() =
let
val counter = ref 0
fun reset() = (counter := 0)
fun tick() = (counter := !counter + 1; !counter)
in
(reset, tick)
end
```
Now consider:
```    val (reset1, tick1) = new_counter()
val (reset2, tick2) = new_counter()
tick1()
tick1()
tick2()
```