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 = 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);
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
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: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)
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)
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
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 ...
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
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))
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
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.
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
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:
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
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.
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
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
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
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
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()