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)).