REVISION NOTES

- logical programming (Prolog)
- functional programming (ML)

- values and types
**YES** - variables and assignments
**NO** - functions are "first-class" like values (return or pass functions)
- strong but flexible type system
- polymorphism (functions can take different types of values)

- concise and elegant
- easy to reason about
- more compile-time error checking
- portable and high-level code (no pointers or memory (de)allocation)

Example:

val x = 3 val x:int = 3

Limited scope of declarations; an expression is evaluated in the context of an *environment*.

localdeclindeclend

letdeclinexprend

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: t

g f vis ambiguous

g (f v)is correct

(g f) vis ill-typed

Type of a function is determined bottom-up:

fn x => x + 1 x:int |- x + 1:int

- Anonymous functions must use
`fn` - Named functions use
`fun`(or`val f = fn ...`)

Tuples are fixed in length.

`(val1, val2, ..., valn)` is an *n-tuple* with type `typ1 * typ2 * ... * typn`

Special cases:

- n = 0:
`()`has type`unit` - n = 1:
`(val)`is equivalent to`val`(NOT a tuple!)

Example:

val pair_pairs = ((2, 3), (2.0, 3.0))

Patterns may contain:

- variables
`x` - constants
`2` - tuples
`(x, 2)` - typed patterns
`x:int` - don't care (or
*wildcards*)`_`

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

- exhaustive
- no overlapping
- clauses are evaluated in order

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

caseexprofpat1=>exp1|pat2=>exp2... |patn=>expn

Example:

fun not b = case b of true => false | false => true

If/else is a special case of *case*:

ifcondcasecondthenexp1of true =>exp1elseexp2| false =>exp2

Lazy and/or are provided *(cf operators && and || in Java/C)*. Equivalent to the following:

exp1andalsoexp2ifexp1thenexp2else falseexp1orelseexp2ifexp1then true elseexp2

Example (both equivalent):

fun factorial 0 = 1 | factorial n = n * factorial (n-1) valrecfactorial = 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)andodd 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 -> 'bfn (a, x) => x + 1'a * int -> int

- can grow or shrink
- ordered
- all elements must be same type

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(n^{2})):

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

- type constructor
- value constructor(s)

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 branchand`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 b2andbranchsize (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 yf: 'a * 'b -> 'c g: 'a -> 'b -> 'c x: 'a y: 'b curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'cg = 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:

exceptionFactorial fun checked_factorial n = if n < 0 thenraiseFactorial else if n = 0 then 1 else n*checked_factorial (n-1)

Exceptions may also carry a value:

exception SyntaxErrorof string... handle SyntaxError msg => ...

expr0handlepat1=>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 endhandleFactorial => 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 ;

- core language
- module language
- signatures (interface specifications)
- structures (program units/modules)
- functors ("functions" returning a structure)

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*):

structureQueue : 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`):

`Str`may define more components than required (but not less)- Types in
`Str`may be more general than required - Order does not matter
`Str`may provide a datatype where`SIG`only requires a type

*opaque*: only information in signature is externally visible*transparent*: details of type representation are also visible

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 structurePrioQueue :> 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 = PQwhere type elem = stringstructure PrioQueue :>STRING_PQ= struct ... end PrioQueue.insert("abc", PrioQueue.empty)

Example:

signature ORDERED = sig type t val lt: t * t -> bool end signature DICT = sigstructure Key : ORDEREDtype '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 = DICTwhere 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 = sigsharing typePoint.point = Sphere.Point.pointsharing typePoint.Vector.vector = Sphere.Vector.vector ... end signature SPHERE = sigsharing typePoint.Vector.vector = Vector.vector ... end

Alternatively, we can use *structure sharing constraints*:

signature SPHERE = sigsharingPoint.Vector = Vector ... end

Functors are like functions which return a structure.

Example (with parameter called `K`):

functorDictFun (structure K : ORDERED) :> DICT where typeKey.t = K.t= struct structure Key : ORDERED = K ... Key.t ... end

Equivalent example (use `K` directly in structure body):

functorDictFun (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 : POINTsharing 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):
we don't care
Assume |

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