# FUNCTIONAL PROGRAMMING AND SPECIFICATION REVISION NOTES

## INTRODUCTION

• logical programming (Prolog)
• functional programming (ML)

### Functions Are Important

• 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
• more compile-time error checking
• portable and high-level code (no pointers or memory (de)allocation)

## DECLARATIONS

Example:

```val x     = 3
val x:int = 3
```

## LIMITED SCOPE

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.

## INTRODUCTION TO FUNCTIONS AND TYPES

Example:

f: t -> t'
g: t' -> t''
v: t

g 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
```
• Anonymous functions must use fn
• Named functions use fun (or val f = fn ...)

## TUPLES

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

## TUPLE PATTERN MATCHING

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
```

## RECORDS

{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",
display  = "Don Sannella" }
```

## RECORD PATTERN MATCHING

Can extract values using a pattern:

```val {protocol=prot, display=_, address=addr} = mailtodts
```

Can also use label names as functions:

```val prot = #protocol mailtodts
```

## TUPLES AS RECORDS

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
```

## PATTERNS IN FUNCTIONS

• 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
```

## CASE STATEMENT

```case expr
of pat1 => exp1
|  pat2 => exp2
...
|  patn => expn
```

Example:

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

## IF/ELSE STATEMENT

If/else is a special case of case:

```if cond          case cond
then exp1        of true  => exp1
else exp2        |  false => exp2
```

## LOGICAL AND/OR

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
```

## RECURSIVE FUNCTIONS

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
```

## MUTUALLY RECURSIVE FUNCTIONS

Use and. Example:

```fun even 0 = true
|   even n = odd  (n-1)
and odd  0 = false
|   odd  n = even (n-1)
```

## TYPE SCHEMES

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
```

## LISTS

• 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(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
```

## DATATYPES

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

## RECURSIVE DATATYPES

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

## MUTUALLY RECURSIVE DATATYPES

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

## HIGHER ORDER FUNCTIONS

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

## CURRIED FUNCTIONS

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

```

Example (addition, curried, type int -> int -> int):

```fun add x y = x + y

```

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
```

## MAPPING AND FOLDING

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
```

## LAZY AND EAGER EVALUATION

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
```

## SIDE-EFFECTS: RAISING EXCEPTIONS

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 => ...
```

## SIDE-EFFECTS: HANDLING EXCEPTIONS

```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 result = Int.toString(checked_factorial input)
in
print result
end
handle Factorial => print "Number out of range"
```

## SIDE-EFFECTS: REFERENCES

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]
```

## SIDE-EFFECTS: SEQUENTIAL PROGRAMMING

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 ;
```

## INTRODUCTION TO MODULES

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

## MODULE LANGUAGE: SIGNATURES

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
```

## MODULE LANGUAGE: STRUCTURES

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

• 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

## MODULE LANGUAGE: TRANSPARENT/OPAQUE

• 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

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

## MODULE LANGUAGE: SUBSTRUCTURES

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
```

## MODULE LANGUAGE: SHARING CONSTRAINTS

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

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: INTRODUCTION TO SPECIFICATION AND PROOF

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

### Means Of Communication

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

### Design Aid

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.

### Testing and Proof

EML statements might also assist in generating a test suite (automatically or manually).

### Documentation

EML statements are a formal part of the documentation for how a function should behave.

## EML: SPECIFICATION

 axiom forall X => For every possible value of X axiom exists X => For (at least) some possible value of X A implies BA andalso BA orelse Bnot 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
```

## EML: PROOF BY INDUCTION

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]

To prove member (maxelem (a::b::l), a::b::l)

 Case A: ```a > maxelem (b::l) member (maxelem (a::b::l), a::b::l) = member (a, a::b::l) = true ``` Case B: ```a <= maxelem (b::l) member (maxelem (a::b::l), a::b::l) = member (maxelem(b::l), a::b::l) = [by Inductive Hypothesis] true ```

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