Applicative Programming and Specification: Examples from the lectures

Lecture 2

val succ = fn x => x+1;

val f = succ o (fn s => (size s)+3);
(* takes a string and returns its length + 4 *)


val day = fn 0 => "Monday"
           | 1 => "Tuesday"
           | 2 => "Wednesday"
           | 3 => "Thursday"
           | 4 => "Friday"
           | 5 => "Saturday"
           | _ => "Sunday";
(* convert a number into a day of the week *)

val day' = fn 0 => "Monday"
              | 1 => "Tuesday"
              | 2 => "Wednesday"
              | 3 => "Thursday"
              | 4 => "Friday"
              | 5 => "Saturday"
              | 6 => "Sunday";
(* same thing, but without a catch-all clause *)

val floor = Real.floor;
val real = Real.fromInt;
val zc =
  fn (d,m,y,c) =>
    (floor(2.61 * real m - 0.2) + d + y + y div 4 + c div 4 - 2 * c) mod 7;
val zeller = fn (d,1,y) => zc(d, 11, (y-1) mod 100, (y-1) div 100 + 1)
              | (d,2,y) => zc(d, 12, (y-1) mod 100, (y-1) div 100 + 1)
              | (d,m,y) => zc(d, m-2, y mod 100, y div 100 + 1);
(* day(zeller(d,m,y)) calculates the day of the week of the date d/m/y *)


local
  val floor = Real.floor
  val real = Real.fromInt
  val zc =
    fn (d,m,y,c) =>
      (floor(2.61 * real m - 0.2) + d + y + y div 4 + c div 4 - 2 * c) mod 7
in
  val zeller = fn (d,1,y) => zc(d, 11, (y-1) mod 100, (y-1) div 100 + 1)
                | (d,2,y) => zc(d, 12, (y-1) mod 100, (y-1) div 100 + 1)
                | (d,m,y) => zc(d, m-2, y mod 100, y div 100 + 1)
end;
(* same, but using local declarations *)


val sumformula = fn n => (n * (n+1)) div 2;
(* sum of the numbers from 1 to n *)

val rec sum = fn 1 => 1
               | n => sum(n - 1) + n;
(* the same thing as a recursive function *)

val three = 3 and four = 4;
(* simultaneous bindings *)

val rec
        f = fn x => g(x+1)
        and
        g = fn y => f(y-1);
(* a silly example of mutual recursion *)

Lecture 3

fun radix(n,base) =
  let
    val b = size base
    fun digit m = str(String.sub(base,m))
    fun radix'(true,m) = digit m
      | radix'(false,m) = radix(m div b,base) ^ digit(m mod b)
  in
    radix'(n<b, n)
  end
(* converts a non-negative integer into a string in a given base, represented
   as a string of digits, e.g. decimal = "0123456789" *)

fun length nil = 0
    | length(a::l) = 1 + length l;
(* length of a list *)

fun add nil = 0
  | add(a::l) = a + add l;
(* sum of the numbers in a list *)

fun tail nil = nil
  | tail(a::l) = l;
(* remove first element from a list *)

fun front nil = nil
  | front(a::nil) = nil
  | front(a::b::l) = a::(front(b::l));
(* remove last element from a list *)

fun zip nil l = nil
  | zip l nil = nil
  | zip (a::la) (b::lb) = (a,b)::(zip la lb);
(* turns a pair of lists into a list of pairs *)


String.explode "abc";
(* [  #"a", #"b", #"c" ] *)

String.implode [  #"a", #"b", #"c" ];
(* "abc" *)

Lecture 4

infixr 5 @;

fun nil @ l' = l'
  | (a::l) @ l' = a :: (l @ l');
(* append two lists *)

fun rev nil = nil
  | rev(a::l) = (rev l) @ [a];
(* reverse a list *)

local
    fun revapp(nil,l') = l'
      | revapp(a::l,l') = revapp(l,a::l')
in
    fun rev' l = revapp(l,nil)
end;
(* a variant on rev *)

fun insert(x,nil) = [x]
  | insert(x,h::t) = if x<=h then x::h::t
                     else h::insert(x,t);
(* insert elements into a sorted list
   insert : int * int list -> int (the function <= is defined on integers,
   reals, characters and strings, but "default overloading" picks int *)

fun sort nil = nil
  | sort(h::t) = insert(h,sort t);
(* sort a list of integers *)


fun compose(f,g) =  (fn x => f(g x));
(* function composition *)

fun compose(f,g) x = f(g x);
(* the same thing written slightly differently *)

fun twice f x = f(f x);
(* compose a function with itself *)

fun twice f = compose(f,f);
(* the same thing written differently *)

fun iter(f,0) x = x
  | iter(f,n) x = f(iter (f,n-1) x);
(* n-fold composition of a function with itself *)

fun id x = x;

fun iter'(f,0) = id
  | iter'(f,n) = compose(f, (iter'(f,n-1)));
(* the same thing written differently *)

Lecture 5

fun plus x y = x+y;
(* curried version of + *)

fun plus'(x,y) = x+y;
(* uncurried version of + *)

val succ = plus 1;

fun pow(x,0) = 1
  | pow(x,n) = pow(x,n-1) * x;
(* x to the nth power *)

fun pow' x 0 = 1
  | pow' x n = (pow' x (n-1)) * x;
(* curried version of pow *)

fun curry f x y = f(x,y);
(* turn an uncurried version of a function into a curried version *)

val plus = curry(op +);
(* same as plus above *)

fun uncurry f (x,y) = f x y;
+(* convert a curried function to an uncurried one *)


fun map f nil = nil
  | map f (h::t) = (f h)::(map f t);
(* map : ('a -> 'b) -> 'a list -> 'b list
   apply a function to every element of a list *)

fun reduce(g,f,m,n,e) =
     if m>n then e
     else g(reduce(g,f,m,n-1,e),f(n));
(* accumulate a result by applying a binary function g to a sequence of terms
   f(i) for i from a starting value m to an final value n *)

fun sq n = reduce(op +, fn x => 2 * x - 1, 1, n, 0);

fun sum n = reduce(op +, id, 1, n, 0);

fun pow(x,n) = reduce(op *, fn _ => x, 1, n, 1);

fun fac n = reduce(op *, id, 1, n, 1);

fun exp(x,n) =
      reduce(op +, fn y => real(pow(x,y))/real(fac y), 1, n, 1.0);
(* n-term approximation to e^x, using the formula
   e^x = 1 + x/1 + x^2/1*2 + x^3/1*2*3 + ... *)

Lecture 6

fun id x = x;
(* id : 'a -> 'a *)


fun uncurry f (x,y) = f x y;
(* uncurry : ('a -> 'b -> 'c) -> ('a * 'b -> 'c) *)

Lecture 7

val me = { initial = #"D", surname = "Sannella", age = 44 };
(* me : { initial:char, surname:string, age:int } *)

#surname(me);
(* "Sannella" *)


type person = { initial:char, surname:string, age:int };

type 'a set = 'a -> bool;

type ('a,'b) gadget = ('a->'b) list -> ('b->'a) list;


datatype colour = red | blue | green;
(* introduces a new type and constructors red:colour, etc. *)

fun favourite blue = true
  | favourite c = false;

datatype bool = true | false;
(* just like the built-in type *)


datatype inttree = empty | node of int * inttree * inttree;
(* binary trees of integers with constructors
  empty : inttree
  node : int * inttree * inttree -> inttree *)

datatype 'a tree = empty | node of 'a * 'a tree * 'a tree;
(* same thing, polymorphically *)

fun nodes empty = 0
  | nodes(node(a,t,t')) = 1 + (nodes t) + (nodes t');
(* count number of nodes in a tree *)

datatype 'a list = nil | :: of 'a * 'a list;
infixr 5 :: ;
(* just like the built-in type *)


datatype exp    = plus of term * term
                | minus of term * term
                | mkexp of term
     and term   = times of factor * factor
                | divide of factor * factor
                | mkterm of factor
     and factor = const of int
                | paren of exp;
(* mutually recursive datatype definitions *)

fun eval_exp(plus(t,t')) = (eval_term t) + (eval_term t')
  | eval_exp(minus(t,t')) = (eval_term t) - (eval_term t')
  | eval_exp(mkexp t) = (eval_term t)
and eval_term(times(f,f')) = (eval_factor f) * (eval_factor f')
  | eval_term(divide(f,f')) = (eval_factor f) div (eval_factor f')
  | eval_term(mkterm f) = (eval_factor f)
and eval_factor(const n) = n
  | eval_factor(paren e) = eval_exp e;
(* mutually recursive functions for computing with mutually recursive
   datatypes *)


datatype infintlist = cons of int * (unit->infintlist);
(* constructors can have functions as arguments *)


(* a version of Russell's paradox in ML *)

datatype set = mkset of set->bool;
(* a set is a collection of sets *)

fun russell(mkset f) = not(f(mkset f));
(* russell S is true iff S isn't a member of itself *)

(* Is mkset russell a member of mkset russell?  By expanding the
   definition of russell, we get
     russell(mkset russell) = not(russell(mkset russell))
   Why is this worrying?  Why is it not so very worrying? *)

Lecture 8

val error = fn 1 => 1
             | true => 1;
(* types of patterns don't match *)

val error = fn 1 => true
             | n => "true";
(* types of results don't match *)

val warning = fn false => 3;
(* inexhaustive patterns *)

fun warning false = true
  | warning true = false
  | warning false = false;
(* redundant patterns *)

val error = fn (x,x) => true
             | (x,y) => false;
(* repeated variables *)

fun error(~x) = x
  | error 0 = 0
  | error x = x;
(* ~ is a function, not a constructor *)

fun error(x + x) = true
  | error(x + x + 1) = false;
(* + is a function; repeated variables *))

fun error(fn x => x) = true
  | error f = false;
(* fn is not a constructor *)


let val Id = fn x => x in (Id 3, Id true) end;
(* this is well-typed *)

(fn Id =>(Id 3, Id true))(fn x => x);
(* this is not well-typed *)

Lecture 9

exception Empty;

fun tail nil = raise Empty
  | tail(a::l) = l;

fun front nil = raise Empty
  | front(a::nil) = nil
  | front(a::b::l) = a::(front(b::l));

(* tail(nil) and front(nil) raise an exception *)


fun tail' nil = NONE
  | tail'(a::l) = SOME l;

fun front' nil = NONE
  | front'(a::nil) = SOME nil
  | front'(a::b::l) =
      let val SOME l' = front'(b::l) in SOME(a::l') end;

(* tail',front' : type 'a list -> 'a list option
   tail'(nil) returns NONE, tail'(l) returns SOME(...) if l<>nil,
   and similarly for front' *)

fun tester f x = SOME(f x) handle Empty => NONE;
(* converts from form with exceptions to form with 'a list option *)

fun tester f x = SOME(f x) handle _ => NONE;
(* a variant which deals with all exceptions instead of just Empty *)


exception Div0 of int;

fun mydiv(x,0) = raise Div0 x
  | mydiv(x,y) = x div y;
(* Exceptions can carry data.  To handle such an exception:
   (...mydiv...) handle Div0 n => ...n... *)

Lecture 10

fun member(x,nil) = false
  | member(x,h::t) = (x=h) orelse member(x,t);
(* member : ''a * ''a list -> bool, where ''a can be instantiated by
   any type that admits equality *) 

fun member'(x,p,nil) = false
  | member'(x,p,h::t) = p(x,h) orelse member'(x,p,t);
(* member' : 'a * ('a * 'b -> bool) * 'b list -> bool
   the equality function is passed as a parameter: instead of writing
   member(a,l) we can write member'(a,op =,l) *)


fun exists(p,nil) = false
  | exists(p,h::t) = p h orelse exists(p,t);
(* check to see if there is a value that satisfies a predicate
   instead of writing member'(a,f,l) we can write exists(fn x=>f(a,x),l) *)

fun forall(p,nil) = true
  | forall(p,h::t) = p h andalso forall(p,t);


fun foldr f e nil = e
  | foldr f e (h::t) = f(h,foldr f e t);
(* foldr : ( 'a * 'b -> 'b ) -> 'b -> 'a list -> 'b
   foldr f e [1,2,3] = f(1,f(2,f(3,e))) *)

fun sort' l = foldr insert nil l;

fun length' l = foldr(fn (x,y) => 1 + y) 0 l;


fun foldl f e nil = e
  | foldl f e (h::t) = foldl f (f(h,e)) t;
(* foldl : ( 'a * 'b -> 'b ) -> 'b -> 'a list -> 'b
   foldl f e [1,2,3] = f(3,f(2,(f(1,e)))) *)

fun rev' l = foldl (op ::) nil l;


type 'a delayed = unit -> 'a;
(* if exp:t then fn () => exp : t delayed *)

fun force d = d();
(* force : 'a delayed -> 'a; force(fn () => exp) = exp *)

Rest of SML core language

SML module language

structure S =
  struct
    type t = int
    val x = 3
    fun f(z) = z * (z + 1)
  end;
(* a structure binding; the structure expression is just an encapsulated
   environment *)

structure T = S;
(* structure identifiers are structure expressions too *)

structure S =
  struct
    structure T =
      struct
        type t = int
        val x = 3
      end
    datatype colour = red | blue
    val y = 10
  end;
(* T is a substructure of S *)

S.T.x + S.y : S.T.t;
(* qualified names for referring to components of structures *)

fun nice(S.red) = true
  | nice(S.blue) = false;
(* ditto *)

local
  open S
in
  val a = T.x + y
end;
(* opening up a structure *) 


signature SIG =
  sig
    type t
    val x : int * t
  end;
(* a signature binding *)

signature SIG' = SIG;
(* signature identifiers are signature expressions too *)


signature SIG' = SIG where type t=bool;
(* adding information about a type in an existing signature *)

signature SIG' =
  sig
    include SIG
    val f : t -> t
  end;
(* defining a signature by expanding another signature *)


signature SIG =
  sig
    type t
    val x : t
    val b : bool
  end;

structure S : SIG =
  struct
    type t = int
    val x = 3
    val s = "abc"
    val b = (x = size s)
  end;
(* SIG doesn't mention s so S.s is hidden *)


signature SIG =
  sig
    type ty
    type 'a tycon
    val x : ty
    val y : (int->ty) tycon
  end;

structure S : SIG =
  struct
    type ty = bool
    type 'a tycon = 'a * string
    val x = true
    val y = (fn x => x=3, "abc")
  end;
(* S matches SIG because:
     - S.ty is a type
     - S.tycon is a unary type constructor
     - S.x has type S.ty (= bool)
     - S.y has type (int->ty) tycon (i.e. (int->bool) * string) *)


signature SIG =
  sig
    datatype 'a Dat = N | X of 'a * 'a | C of 'a * 'a Dat
  end;
(* a structure matching SIG must define a unary type constructor Dat
   with constructors N, X, C and no further constructors *)


signature SIG =
  sig
    type 'a Dat
    val N : 'a Dat
    val C : 'a * 'a Dat -> 'a Dat
  end;

structure S : SIG =
  struct
    datatype 'a Dat = N | X of 'a * 'a | C of 'a * 'a Dat
  end;
(* the signature constraint hides X, and it hides the fact that N and
   C are constructors *)


signature SIGT =
  sig
    type t
    val y : bool
  end;

signature SIGS =
  sig
    structure T : SIGT
    val x : T.t
  end;

structure T : SIGT =
  struct
    type t = int
    val y = true
  end;

structure S : SIGS =
  struct
    structure T : SIGT = T
    val x = 17
  end;
(* in signatures specifying substructures, the definition of signature
   matching is applied recursively *)


structure Colour =
  struct
    datatype colour = blend of int * int * int
    val white = blend(0,0,0)
    val red = blend(15,0,0)
    val blue = blend(0,15,0)
    val yellow = blend(0,0,15)
    fun mix(parts:int,  blend(r,b,y),
            parts':int, blend(r',b',y')) =
        blend(parts*r+parts'*r', parts*b+parts'*b', parts*y+parts'*y')
  end;
(* colours are represented as triples of integers (amount of red,
   amount of blue, amount of yellow); "blend" is a constructor *)


signature COLOUR =
  sig
    type colour
    val white : colour
    val red : colour
    val blue : colour
    val yellow : colour
    val mix : int * colour * int * colour -> colour
  end

structure Colour : COLOUR =
  struct
    datatype colour = blend of int * int * int
    val white = blend(0,0,0)
    val red = blend(15,0,0)
    val blue = blend(0,15,0)
    val yellow = blend(0,0,15)
    fun mix(parts:int,  blend(r,b,y),
            parts':int, blend(r',b',y')) =
        blend(parts*r+parts'*r', parts*b+parts'*b', parts*y+parts'*y')
  end;
(* blend is hidden, but the colour will still admit equality *)

structure Colour' : COLOUR =
  struct
    type colour = int * int * int
    val white = (0,0,0)
    val red = (15,0,0)
    val blue = (0,15,0)
    val yellow = (0,0,15)
    fun mix(parts:int,  (r,b,y),
            parts':int, (r',b',y')) =
        (parts*r+parts'*r', parts*b+parts'*b', parts*y+parts'*y')
  end;
(* a transparent signature constraint: the representation of colour is
   revealed and colour admits equality *)


structure Colour'' :> COLOUR =
  struct
    type colour = int * int * int
    val white = (0,0,0)
    val red = (15,0,0)
    val blue = (0,15,0)
    val yellow = (0,0,15)
    fun mix(parts:int,  (r,b,y),
            parts':int, (r',b',y')) =
        (parts*r+parts'*r', parts*b+parts'*b', parts*y+parts'*y')
  end;
(* an opaque signature constraint: the information that colour = int*int*int
   is available inside the structure body but not outside, and colour admits
   equality inside the structure body but not outside *)


signature PO =
  sig
    type t
    val le : t * t -> bool
  end;

functor ReverseOrder(P : PO) : PO =
  struct
    type t = P.t
    fun le(x,y) = P.le(y,x)
  end;

(* ReverseOrder takes any structure P matching PO and returns another
   structure matching PO. *)

structure IntPO =
  struct
    type t = int
    fun le(x:int,y:int) = x <= y
  end;

structure IntPO' = ReverseOrder(IntPO);
structure IntPO'' = ReverseOrder(ReverseOrder(IntPO));


functor Id(P : SIG) : SIG = P;

(* Id is (almost) the identity function on structures matching SIG. *)


fun rev [] = []
  | rev(x::xs) = (rev xs)@[x];

signature TRIVIAL =
  sig
    type t
  end;

functor Rev(A:TRIVIAL) =
  struct
    fun rev [] = []:A.t list
      | rev(x::xs) = (rev xs)@[x]
  end;

(* Polymorphic functions are a lot like functors having TRIVIAL as
   parameter signature *)


signature SORT =
  sig
    structure OBJ : PO
    val sort : OBJ.t list -> OBJ.t list
  end;

functor Sort(X : PO) : SORT =
  struct
    structure OBJ = X

    fun partition(a,[]) = ([],[])
      | 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 [] = []
      | sort(a::l) = let
                       val (l1,l2) = partition(a,l)
                     in
                       (sort l1)@(a::(sort l2))
                     end
  end;

(* This is a "quicksort" program.  Partition is an auxiliary function. *)

structure S = Sort(IntPO);

S.sort [3,6,12,7,2,3,17,8];


functor Lexicographic(structure X : PO
                      structure Y : PO) : PO =
  struct
      type t = X.t * Y.t
      fun le((x,y),(x',y')) =
          if X.le(x,x')
          then if X.le(x',x) then Y.le(y,y') else true
          else false
  end;
(* functors can have multiple parameters *)

structure A = Lexicographic(structure X = IntPO
                            structure Y = IntPO');


functor Rev(type t) =
  struct
    fun rev [] = []:t list
      | rev(x::xs) = (rev xs)@[x]
  end;
(* a functor parameter can be just a type or just a value *)


(* A SCHEMATIC EXAMPLE OF THE NEED FOR SHARING SPECIFICATIONS

   structure Sym : SYM =
     struct
       type symbol = ...
       ...
     end;

  functor AbsSyn(Sym : SYM) : ABSSYN =
    struct
      structure S:SYM
      type var = ...
      val idname:var->S.symbol = ...
      ...
    end;

  functor SymTab(Sym : SYM) : SYMTAB =
    struct
      structure S:SYM
      type table = ...
      val lookup:S.symbol*table->bool = ...
      ...
    end;

  functor Parser(structure SymTab : SYMTAB
                 structure AbsSyn : ABSSYN) : PARSER =
    struct
      ...
      ... if SymTab.lookup(AbsSyn.idname(v), t) then ...
      ...
    end;

Won't typecheck: we don't know that AbsSyn.S.symbol=SymTab.S.symbol
The following is okay though:

  functor Parser(structure SymTab : SYMTAB
                 structure AbsSyn : ABSSYN
                 sharing SymTab.S = AbsSyn.S) : PARSER =
    struct
      ...
      ... if SymTab.lookup(AbsSyn.idname(v), t) then ...
      ...
    end;

or

  functor Parser(structure SymTab : SYMTAB
                 structure AbsSyn : ABSSYN
                 sharing type SymTab.S.symbol = AbsSyn.S.symbol) : PARSER =
    struct
      ...
      ... if SymTab.lookup(AbsSyn.idname(v), t) then ...
      ...
    end;
*)


functor Sort(X : PO) : SORT where type OBJ.t=X.t =
  struct
    structure OBJ = X

    fun partition(a,[]) = ([],[])
      | 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 [] = []
      | sort(a::l) = let
                       val (l1,l2) = partition(a,l)
                     in
                       (sort l1)@(a::(sort l2))
                     end
  end;
(* the result is required to be related to the parameter, and to
   include sort : X.t list -> X.t list *)

functor Sort(X : PO) : SORT =
  struct
    structure OBJ = struct
                      type t = unit
                      fun le(x,y) = false
                    end
    fun sort l = []
  end;
(* the functor heading doesn't specify that the result has to have
   anything to do with the parameter *)

Specifications in EML

val sqrt : real -> real = ?;

axiom forall a:real => sqrt(a) * sqrt(a) = a;


(* Let's assume that matrices, matrix multiplication and the identity matrix
   have been previously defined.  I will just give their types.  We implement
   matrix as (int list) list to sidestep an issue with equality that will be
   explained later *)

type matrix = (int list) list;
val ** : matrix * matrix -> matrix = ?;
infix 7 **;
val I : matrix = ?;

val inv : matrix -> matrix = ?;

axiom inv(A) ** A = I;
axiom A ** inv(A) = I;


(* pre-conditions need to be added to the above specifications as follows *)

axiom a >= 0.0 implies sqrt(a) * sqrt(a) = a;

axiom exists B => (B ** A = I andalso A ** B = I)
      implies
      inv(A) ** A = I andalso A ** inv(A) = I;

(* nothing above here will work in EML because quantification must be explicit *)

axiom forall A => (exists B => B ** A = I andalso A ** B = I
                   implies
                   inv(A) ** A = I andalso A ** inv(A) = I);


fun member(a,[]) = false
  | member(a,b::l) = (a=b) orelse member(a,l);

val maxelem : int list -> int = ?;

axiom forall l => l<>[] implies member(maxelem l, l);
axiom forall (a,l) => member(a,l) implies (maxelem l) >= a;


val before : string * string -> string = ?;
val after : string * string -> string = ?;

(* in the lecture, I referred to the library function String.isPrefix.
   This isn't available in EML as currently defined, so let me just give its type *)

val isPrefix : string -> string -> bool = ?;

axiom forall (s,r) => before(s,r) ^ s ^ after(s,r) = r;
axiom forall (s,r) => forall (t1,t2) => t1^s^t2=r implies isPrefix (before(s,r)) t1;
(* before("i","specification") = "spec" and after("i","specification") = "fication" *)

val substring : string * string -> bool = ?;

axiom forall (s,r) => substring(s,r) implies before(s,r) ^ s ^ after(s,r) = r;
axiom forall (s,r) => substring(s,r) = (exists (t1,t2) => t1^s^t2=r);


axiom forall a => a >= 0.0 implies                   
		  sqrt(a) * sqrt(a) >= 0.99*a
		  andalso                    
		  sqrt(a) * sqrt(a) <= 1.01*a;
(* sqrt is allowed to produce any result within the specified interval *)


fun maxelem nil = 0
  | maxelem([a]) = a
  | maxelem(a::b::l) = if a>maxelem(b::l) then a
                       else maxelem(b::l);
(* We can use structural induction on lists to prove that this satisfies the
   specification given above *)


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;

(* This implements an unbounded array of integers indexed starting from 0,
   using a list of integers to represent the array. *)

  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)

(* These five axioms specify the functions Array.retrieve and Array.put and the
   value Array.empty *)

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;

(* This signature combines SML-style type information with axioms.  But it is not
   quite correct -- see below. *)

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;

(* Since array does not admit equality, we need to use EML's "logical" equality ==
   rather than SML's "computational" equality = . *)


structure Array :> ARRAY = ?;

(* Specifying a structure without providing an implementation *)

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;

(* Providing a partial implementation *)

(* Structure/functor bindings that use opaque signature constraints written with :>
   will not be accepted by EML as currently defined because this was not in SML'90.
   Changing :> to : will give the desired effect because all signature constraints
   are opaque in EML. *) 


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 = ?;

(* A specification of a structure containing functions for creating, updating and
   displaying a histogram. *)

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;

(* An implementation of the above specification *)

structure Histogram :> HISTOGRAM where type A.array = Array.array = ?;

(* We can require that the type of array produced by display is the same
   type as used elsewhere in the system. *)

(* This will not be accepted by EML as currently defined both because of :> and
   because of the "where ..." form.  Here is how to get the same effect:

structure Histogram : sig include HISTOGRAM
                          sharing type A.array = Array.array
                      end = ?;

*)


(* To prove that Histogram satisfies HISTOGRAM we have to:
1. show that Array satisfies ARRAY
2. show that the code in Histogram satisfies the "visible" axiom in
   HISTOGRAM, assuming that count is defined by the "hidden" axioms in
   HISTOGRAM, and that A satisfies ARRAY. *)


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;

fun count(a,[]) = 0
  | count(a,b::l) = if a==b then 1+count(a,l) else count(a,l);

signature SORT =
  sig
    structure OBJ : PO
    local
      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 =
		   (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 = ?;


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 OBJ.le(a,c)
		andalso
		forall d => member(d,l) iff member(d,l1) orelse member(d,l2)
	    end

    fun sort [] = []
      | sort(a::l) = let val (l1,l2) = partition(a,l)
		     in  (sort l1)@(a::(sort l2))
		     end
  end;

(* This supplies code for sort but only specifies partition.  The axiom for
   partition assumes that member has been defined earlier. *)