Short cuts:
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);
val m = 3+2 val pi = 3.14 val n = m+1 type count = intExamples of compound declarations:
val pi = 3.14 ; val n = m+1 val pi = 3.14 and n = m+1Reusing 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) + mTo 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.0Naming 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.0A more compact syntax for defining a function and giving it a name:
fun fourthroot x = Math.sqrt (Math.sqrt x);
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) * xExamples 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_pairsValid 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 => falseor equivalently
fun iszero 0 = true | iszero n = falseBut the following is NOT equivalent -- order matters!
fun iszero n = false | iszero 0 = true
fun not True = false | not False = trueThe 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:A simple recursive function in ML:
- if S is on the page at URL, return TRUE.
- for each link URL' on that page, search all web pages starting at URL' for S.
- If S hasn't been found yet, return FALSE.
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) endAnother 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)
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) endA 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, _) = falseAnother simple datatype (this one is built in):
datatype 'a option = NONE | SOME of 'aA 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+3instead of
fun f(n,m) = divide(n,m) + 3Here are binary trees with integer labels at each node. This is a recursive datatype.
datatype tree = Empty | Node of tree * int * treeAn 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
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 * treeand 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 treeAnd 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 t2Pre-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 treeand 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 listand 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 treeand 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 tIf 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 stringWe can do this in general:
datatype ('a,'b) union = First of 'a | Second of 'bAbstract syntax for a small language of arithmetic expressions:
datatype expr = Numeral of int | Plus of expr * expr | Times of expr * exprNotice how close this is to the BNF definition of (concrete) syntax:
expr ::= n | expr + expr | expr * exprA 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 comAn 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 * comThe 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 ...
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+1then 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 = xthen 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 4This 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+yor equivalently
fun plus x = fn y => x+yWe 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) * xA curried version:
fun pow' x = fn 0 => 1 | n => (pow' x (n-1)) * xor equivalently
fun pow' x 0 = 1 | pow' x n = (pow' x (n-1)) * xA 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 yor equivalently
fun uncurry f = fn (x,y) => f x yApplying 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 eWe can use this to compute length of a list:
fun length l = foldr(fn (x,y) => 1 + y) 0 lOr sum of the integers in a list:
fun add l = foldr (op +) 0 lConsider 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 nilNow, folding to the left (this is built in):
fun foldl f e nil = e | foldl f e (h::t) = foldl f (f(h,e)) tFoldr and foldl are similar but not the same:
val id = foldr (op ::) nil val rev = foldl (op ::) nil
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 zThe 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 () => expbut since delay is then a function it will evaluate its argument which is wrong. So we have to write
fn () => expand 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) delayedA 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))
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 llistwhere
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 endUsing signature inclusion to add an additional component:
signature QUEUE_WITH_ISEMPTY = sig include QUEUE val is_empty : 'a queue -> bool endThere'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 endUsing signature specialization to add information about types that a signature already contains:
signature QUEUE_AS_LISTS = QUEUE where type 'a queue = 'a list * 'a listYou 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 listYou have to go back to an "ancestor" where the type is not yet defined:
signature QUEUE_AS_LIST = QUEUE where type 'a queue = 'a listThe 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
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)) endIf 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 = Queuethen
val q = Q.insert(2,Q.insert(1,Q.empty))Alternatively, write
open Queuethen
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.
signature MERGEABLE_QUEUE = sig include QUEUE val merge : 'a queue * 'a queue -> 'a queue endmatches the signature
signature MERGEABLE_INT_QUEUE = sig include QUEUE val merge : int queue * int queue -> int queue endbecause 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 endmatches the signature
signature RBT = sig type 'a rbt val Empty : 'a rbt val Red : 'a rbt * 'a * 'a rbt -> 'a rbt end
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)) endAn 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) endTo check that the invariant always holds, we just have to check:
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 endand 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) endSuppose 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 endThen 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 = intNow 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 endFor 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
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) endThen 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=intThen 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 ... endHere'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 endWe 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 endInstantiation 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 endThe 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 ... endbut the result signature can't be defined outside the scope of the parameter.
signature GEOMETRY = sig structure Point : POINT structure Sphere : SPHERE endTo 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 endThen points are:
signature POINT = sig structure Vector : VECTOR type point val translate : point * Vector.vector -> point val ray : point * point -> Vector.vector endSpheres are now given by:
signature SPHERE = sig structure Vector : VECTOR structure Point : POINT type sphere val sphere : Point.point * Vector.vector -> sphere endNow 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 endWe 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 endThese 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 endFor instance, we have Geom3D.Point.point = Geom3D.Sphere.Point.point because
Geom3D.Point.point = Point3D.point Geom3D.Sphere.Point.point = Sphere3D.Point.point = Point3D.pointThe following does not obey these constraints, and would not be accepted:
structure Geom3D' :> GEOMETRY = struct structure Point = Point3D structure Sphere = Sphere2D endWe don't have Geom3D'.Point.point = Geom3D'.Sphere.Point.point:
Geom3D'.Point.point = Point3D.point Geom3D'.Sphere.Point.point = Sphere2D.Point.point = Point2D.pointand 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 endThen 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
sqrt : real -> real sqrt(a) * sqrt(a) = aSpecification 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) = IAn 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) = aAn 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) = IAnd 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) >= aSpecification 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)) t1An 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)) t1Another 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
local fun helper(0,r) = r | helper(n,r) = helper(n-1,n*r) in fun factorial n = helper(n,1) endHere 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)/2A 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 treewe 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 t2We 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)) OKGiven the declaration
datatype 'a tree = Empty | Leaf of 'a | Node1 of 'a * 'a tree | Node2 of 'a tree * 'a * 'a treewe 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 * comSome user-defined types do not give rise to an induction principle, for instance
datatype D = Int of int | Fun of D->D
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) endWe 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 endAdding 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) endIn 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) endWe can ascribe this signature to Array, using the usual syntax:
structure Array :> ARRAY = struct type array = int list . . . endWe 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) = ? endWe 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) endHere 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 endIf 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.arrayNow, 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 endA 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
3 div 0 1000000000 + 1000000000If we define
fun hd(h::_) = hthen the following raises Match:
hd nilThe following raises Bind:
let val h::t = nil in ...anything... endUsers 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 endIt is possible to "catch" an exception and deal with it under program control:
fun recover_factorial n = checked_factorial n handle Factorial => 0Here's a more complicated version, involving several exceptions:
fun recover_factorial n = checked_factorial n handle Factorial => 0 | Overflow => ~1Exceptions can carry values:
exception Divide of int fun divide(x,0) = raise Divide x | divide(x,y) = x div yA 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 amtDoubly-linked lists, using references:
datatype 'a dllist = endmarker | cell of 'a * ('a dllist) ref * ('a dllist) refAn example showing the difference between references and ordinary ML variables:
val x = 1 fun f(y) = let val x=x+1 in x+y endNow 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 endNow 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 endSharing private state between functions:
local val counter = ref 0 in fun reset() = (counter := 0) fun tick() = (counter := !counter + 1; !counter) endA 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) endNow consider:
val (reset1, tick1) = new_counter() val (reset2, tick2) = new_counter() tick1() tick1() tick2()