Example:
val x = 3 val x:int = 3
Limited scope of declarations; an expression is evaluated in the context of an environment.
local decl in decl end
let decl in expr end
Example:
val m:int = 2
val r:int = (let m:int = 3 and n:int = 6 in m*n end) + m
Inner binding eclipses outer binding temporarily, calculation is r = 3 * 6 + 2.
Example:
f: t -> t'
g: t' -> t''
v: tg f v is ambiguous
g (f v) is correct
(g f) v is ill-typed
Type of a function is determined bottom-up:
fn x => x + 1 x:int |- x + 1:int
Tuples are fixed in length.
(val1, val2, ..., valn) is an n-tuple with type typ1 * typ2 * ... * typn
Special cases:
Example:
val pair_pairs = ((2, 3), (2.0, 3.0))
Patterns may contain:
Variables may NOT be repeated.
Example (assigns r = 2.0):
val ((_,_), (r, _)) = pair_pairs
{lab1=val1, lab2=val2, ..., labn=valn} has type
{lab1:typ1, lab2:typ2, ..., labn:typn}
Example:
type hyperlink = {protocol:string, address:string, display:string} val mailtodts:hyperlink = { protocol = "mailto", address = "dts@dcs.ed.ac.uk", display = "Don Sannella" }
Can extract values using a pattern:
val {protocol=prot, display=_, address=addr} = mailtodts
val {protocol=prot, address=addr, ... } = mailtodts
Can also use label names as functions:
val prot = #protocol mailtodts val addr = #address mailtodts
Tuples are simply a special case of records (the statements below are equivalent):
val v = ( 7, "abc" ) val v = { 1=7, 2="abc" } val letters = #2 v
Examples (equivalent):
val is_zero = fn 0 => true | n => false fun is_zero 0 = true | is_zero n = false
The following will always evaluate to false, because clauses are evaulated in order (it also generates a warning about redundant clauses):
fun is_zero n = false | is_zero 0 = true
case expr of pat1 => exp1 | pat2 => exp2 ... | patn => expn
Example:
fun not b = case b of true => false | false => true
If/else is a special case of case:
if cond case cond then exp1 of true => exp1 else exp2 | false => exp2
Lazy and/or are provided (cf operators && and || in Java/C). Equivalent to the following:
exp1 andalso exp2 if exp1 then exp2 else false exp1 orelse exp2 if exp1 then true else exp2
Example (both equivalent):
fun factorial 0 = 1 | factorial n = n * factorial (n-1) val rec factorial = fn 0 => 1 | n => n * factorial (n-1)
This uses a lot of stack space for pending calculations:
factorial 3 = 3 * factorial 2 = 3 * (2 * factorial 1) = 3 * (2 * (1 * factorial 0)) = 3 * (2 * (1 * 1)) = 3 * (2 * 1) = 3 * 2 = 6
A more efficient tail recursive approach is:
local fun helper (0, r) = r | helper (n, r) = helper (n-1, n*r) in fun factorial n = helper (n, 1) end
This version executes as follows:
factorial 3 = helper (3, 1) = helper (2, 3) = helper (1, 6) = helper (0, 6) = 6
Use and. Example:
fun even 0 = true | even n = odd (n-1) and odd 0 = false | odd n = even (n-1)
For some functions there are any number of possible type schemes. There is always a principal type scheme or most general type scheme, which can be computed automatically by solving a system of equations.
fn (a, x) => x 'a * 'b -> 'b fn (a, x) => x + 1 'a * int -> int
We use nil (type 'a list) for the empty list.
The "cons" function :: adds a single element to the head of a list. It has type 'a * 'a list -> 'a list.
Two equivalent ways to create a list:
a1::(a2::(a3::nil)) [a1, a2, a3]
The append function @ joins two lists (type 'a list * 'a list -> 'a list). Strings can be joined using ^.
[1, 2, 3] @ [4, 5, 6]
Example (calculate the length of a list):
fun length nil = 0 | length _::t = 1 + length t
Example (join two lists, as with @):
fun join (nil, l) = l | join (h::t, l) = h :: append (t, l)
Example (remove last element [1, 2, 3, 4] -> [1, 2, 3]). Note that removing the first element is trivial using ::.
fun front nil = nil | front (a::nil) = nil | front (a::b::t) = a::front(b::t)
Example (reverse list, runtime O(n2)):
fun rev nil = nil | rev (h::t) = (rev t) @ h
Example (reverse list, tail recursive, runtime O(n)):
local fun helper (nil, a) = a | helper (h::t, a) = helper (t, h::a) in fun rev l = helper (l, nil) end
Examples:
datatype suit = Spades | Hearts | Diamonds | Clubs datatype 'a option = NONE | SOME of 'a
NONE is a nullary type constructor, while SOME is a unary type constructor (because it has one argument). Think of SOME as a function with type 'a -> 'a option.
Example (division with divide-by-zero detection):
fun divide (n, 0) = NONE | divide (n, m) = SOME (n div m)
Function divide has type int * int -> int option.
Example (binary tree with labelled nodes):
datatype 'a tree = Empty | Node of 'a tree * 'a * 'a tree Node(Empty, 2, Node(Empty, 3, Empty))
Labels are of type 'a.
Example (calculate height of tree):
fun height Empty = 0 | height (Node(t1, a, t2)) = 1 + Int.max(height t1, height t2)
Example (built-in list datatype):
datatype `a list = nil | :: of `a * `a list infix ::
Example (binary tree with labelled branches):
datatype 'a tree = Empty | Node of 'a branch * 'a * 'a branch and `a branch = Branch of 'a * 'a tree
Mutually recursive datatypes can naturally lead to mutually recursive functions:
fun treesize Empty = 0 | treesize (Node(b1, b2)) = branchsize b1 + branchsize b2 and branchsize (Branch(_, t)) = 1 + treesize t
Example:
(* This is a comment * which can span multiple lines... *)
Functions which return other functions, etc.
Built-in o function (for composition):
(f o g) x equivalent to f (g x)
o has type ('b -> 'c) * ('a -> 'b) -> ('a -> 'c)
fun o (f, g) = (fn x => f (g x))
Example (do something twice):
fun twice f x = f (f x) fun inc x = x + 1
Then (twice inc) is a function to add two. Therefore (twice inc) 3 would give the value 5.
Function twice has the type ('a -> 'a) -> ('a -> 'a).
The -> is right-associative, so int -> int -> int means int -> (int -> int).
Any function taking two or more arguments can be curried.
Example (addition, not curried, type int * int -> int):
fun add (x, y) = x + y add (2, 3)
Example (addition, curried, type int -> int -> int):
fun add x y = x + y add 2 3
Example (powers, two possibilities for writing a curried function):
fun pow x 0 = 1 | pow x n = x * (pow x (n-1)) fun pow x = fn 0 => 1 | n => x * (pow x (n-1))
Example (function to curry a two-argument uncurried function, and vice versa):
fun curry f x y = f (x, y) fun uncurry g (x, y) = g x y f: 'a * 'b -> 'c g: 'a -> 'b -> 'c x: 'a y: 'b curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c g = curry f f = uncurry g
Higher-order functions can be used to perform an operation on a list or tree.
Example (use a function to map a list of arguments to a list of results):
fun map f nil = nil | map f (h::t) = (f h)::(map f t) map: ('a -> 'b) -> 'a list -> 'b list fun square x = x * x val squares_list = map square [1, 2, 3, 4, 5]
Example (use folding to sum a list):
fun foldr f e nil = e | foldr f e (h::t) = f (h, foldr f e t) :: foldr + / \ folding / \ a1 :: function a1 + / \ "+" / \ a2 :: -----> a2 + / \ / \ a3 :: a3 + / \ / \ a4 nil a4 0 (identity "e") :: foldl + / \ folding / \ a1 :: function + a4 / \ "+" / \ a2 :: -----> + a3 / \ / \ a3 :: + a2 / \ / \ a4 nil 0 a1 foldl/foldr: ('a * 'b -> 'b) -> 'b -> 'a list -> 'b fun sum l = foldr (op +) 0 l val sum = foldr (op +) 0 [better version]
Functions foldl/foldr keep a "running total" (type 'b). This can be given a specific starting value. The total is updated by calling the folding function for each element in the list.
Example (use folding to perform insertion sort):
fun insert (a, nil) = [a] | insert (a, b::t) = if a < b then a::b::t else b::(insert(a, t)) val sort = foldr insert nil
The insert function builds up a new list, inserting each element from the old list in the appropriate position.
Example (use foldl to reverse a list; foldr would not work):
val rev = foldl (op ::) nil
Standard ML performs eager evaluation, so each argument is evaulated first, before the function they are passed to.
Example:
fun loop n = loop (n + 1) fun f x = x f (loop 17)
This never terminates (because loop 17 is evaluated first), although the result is guaranteed to be 1.
To force lazy evaluation in Standard ML, we must write
fun f () = 2*3
While 'a can be replaced by any type, ''a can only be replaced by types which admit equality (those which can be compared using the = operator).
Example:
fun member (x, nil) = false | member (x, h::t) = (x = h) orelse member (x, t) member: ''a * ''a list -> bool
Example:
exception Factorial fun checked_factorial n = if n < 0 then raise Factorial else if n = 0 then 1 else n*checked_factorial (n-1)
Exceptions may also carry a value:
exception SyntaxError of string ... handle SyntaxError msg => ...
expr0 handle pat1 => expr1 | pat2 => expr2 ... | patn => exprn
The pattern may be replaced by _ for "don't care". All the expressions expr0,1,2,...,n must have the same type.
Example:
fun factorial_driver () = let val input = read_integer() val result = Int.toString(checked_factorial input) in print result end handle Factorial => print "Number out of range"
Use of references is not favoured in functional programming; it complicates reasoning about programs. It also breaks referential transparency (where the value of an expression is fixed by its environment).
References are useful for memoisation, which stores the result of function calls with a certain set of arguments.
References are created using ref. A value can be retrieved using !. Assignment to an existing reference uses :=.
Example:
val x = ref 3 x := 4 print !x [prints 4]
The ; can be used to evaluate two expressions, but return the result from the second expression only. It is defined as:
fun a ; b = b infix ;
Signature names are ALL CAPITALS by convention. Example:
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
Signatures can be extended by other signatures (inheritance):
signature QUEUE_WITH_ISEMPTY = sig include QUEUE val is_empty: 'a queue -> bool end
Signatures may also specify the types used to implement them. This queue is implemented as a pair of lists:
signature QUEUE_AS LISTS = QUEUE where type 'a queue = 'a list * 'a list
Structures may implement a signature (called signature ascription):
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
Structures may be used by writing (for example) Queue.insert(...). It is also possible to use open Queue followed by simply insert(...).
To shorten names, can write structure Q = Queue followed by Q.insert(...).
Rules (for structure Str which implements SIG):
Write Str : SIG for transparent or Str :> SIG for opaque.
Example:
signature PQ = sig type elem val lt : elem * elem -> bool type queue exception Empty val empty: queue val insert: elem * queue -> queue val remove: queue -> elem * queue end structure PrioQueue :> PQ = struct type elem = string val lt : string * string -> bool = op < type queue = string list exception Empty val empty = nil fun insert (x, nil) = nil | insert (x, y::l) = if lt (x,y) then x::y::l else y::insert(x, l) fun remove nil = raise Empty | remove (x::l) = (x, l) end PrioQueue.insert("abc", PrioQueue.empty)
The last line does not type-check, since the type of elem is hidden by the opaque ascription. We can fix this by making the type part of the signature:
signature STRING_PQ = PQ where type elem = string structure PrioQueue :> STRING_PQ = struct ... end PrioQueue.insert("abc", PrioQueue.empty)
Example:
signature ORDERED = sig type t val lt: t * t -> bool end 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
In a complex system with many modules, we must sometimes explicitly state that two types are the same, in order to allow modules to interact.
Example:
signature GEOMETRY = sig structure Point: POINT structure Sphere: SPHERE end signature SPHERE = sig structure Point: POINT structure Vector: VECTOR type sphere val create: Point.point * Vector.vector -> sphere end signature VECTOR = sig type vector val zero: vector ... end signature POINT = sig structure Vector: VECTOR type point val translate: point * Vector.vector -> point val ray: ... ... end structure Geom3D :> GEOMETRY = ... ... val p : Geom2D.Point.point val q : Geom2D.Point.point Geom3D.Sphere.create(p, Geom2D.Point.ray(p, q))
The last statement will NOT type-check, because Geom3D.Sphere.Point is not necessarily the same as Geom3D.Point.
We can add some type sharing constraints to ensure that this condition holds:
signature GEOMETRY = sig sharing type Point.point = Sphere.Point.point sharing type Point.Vector.vector = Sphere.Vector.vector ... end signature SPHERE = sig sharing type Point.Vector.vector = Vector.vector ... end
Alternatively, we can use structure sharing constraints:
signature SPHERE = sig sharing Point.Vector = Vector ... end
Functors are like functions which return a structure.
Example (with parameter called K):
functor DictFun (structure K : ORDERED) :> DICT where type Key.t = K.t = struct structure Key : ORDERED = K ... Key.t ... end
Equivalent example (use K directly in structure body):
functor DictFun (structure K : ORDERED) :> sig ... end = struct ... K.t ... end
Example (instantiating a functor):
structure LexString : ORDERED = struct ... end structure StringDict = DictFun (structure K = LexString)
Example (two parameters, type sharing is REQUIRED):
functor SphereFun ( structure V : VECTOR structure P : POINT sharing P.Vector = V ) : SPHERE = struct structure Vector = V structure Point = P ... end
EML extends SML with means of specifying properties which functions must obey. This is not applicable to the side-effecting parts of the language (references and I/O).
In this course, we ignore exceptions and non-termination (total functions only).
Software engineering is concerned (partly) with communications between a programming team and their client, through the requirements specification. This could be written in EML (with some additional explanation).
Programmers in a team need to communicate, to decide upon module interfaces and interactions. Together with the module language, EML is a useful tool for specifying the design. It can help programmers to develop a formal understanding of the problem.
EML statements might also assist in generating a test suite (automatically or manually).
EML statements are a formal part of the documentation for how a function should behave.
axiom forall X => | For every possible value of X |
axiom exists X => | For (at least) some possible value of X |
A implies B A andalso B A orelse B not X | Boolean logic |
= <> | Computationally equal / not equal (type ''a * ''a -> bool) |
== =/= | Logically equal / not equal (type 'a * 'a -> bool) For axioms, equality may not be computable in a finite time. |
Example (square root):
axiom forall a => a >= 0.0 implies sqrt (a) * sqrt (a) = a
The structure of the inductive proof generally follows the structure of the code. Example:
fun maxelem nil = 0 | maxelem [a] = a | maxelem (a::b::l) = if a > maxelem (b::l) then a else maxelem (b::l) maxelem: int list -> int member: 'a * 'a list -> bool
In this code there are two base cases. We assume the member function (provided) has already been shown to be correct.
To prove forall l => l <> nil implies member (maxelem l, l):
Base Case 0: P(nil): we don't care Base Case 1: P([a]): member (maxelem [a], [a]) = member (a, [a]) = true Inductive Step: Assume member (maxelem (b::l), b::l) = true [Inductive Hypothesis] |
In structural induction with trees, we generally have two inductive hypotheses (for a binary tree) in order to show the inductive step. We assume P(t1) and P(t2) in order to show P(Node(t1, label, t2)).