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")
    
    A function with multiple arguments (type load "Math" first to get access to Math.sqrt):
        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
          | add(h::t) = h + add t
    
        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
    
        fun outranks(Spades, Spades) = false
          | outranks(Spades, _) = true
          | outranks(Hearts, Spades) = false
          | 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
    
    instead of
        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
    
    Using signature inclusion to add an additional component:
        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
    
    Using signature specialization to add information about types that a signature already contains:
        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
    
    Doubly-linked lists, using references:
        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()
    

    Don Sannella. Please mail me if you have any comments on this page.
    Last modified: Fri Mar 18 12:21:37 GMT 2011