Functional Programming

Distance Course (2AD200)
in the Maths & Natural Sciences programme (MN)
at Uppsala University, Sweden

Coding Convention

Good software development companies have coding conventions, hence so can programming courses and software development courses. The requirements in this coding convention have been devised to be tools to guide and facilitate your thinking before and while programming, but not additional obstacles after the already difficult task of programming.

They also ease the communication of your programs to others, such as the instructor and assistants who grade them.

Shedding these good habits after this course would be doing yourself a great disservice. A competent programmer can of course do the specification and verification (or verification outline, as in this course) in her brain only, but that will be of no help if she herself reconsiders the program a few weeks later, or if somebody else has to call or modify or verify it. No engineer takes on a well-defined task without a specification.


Every function, whether declared globally or locally, whether named or anonymous, whether curried or not, whether commissioned in the exercise or invented by you as a help function, shall be commented with its specification, as follows:
(* functionIdentifier argument
   TYPE: argumentType -> resultType
   PRE:  ... pre-condition on the argument ...
   POST: ... post-condition on the result ...
   SIDE EFFECTS: ... if any, including exceptions ...
   EXAMPLES: ... especially if useful to highlight delicate issues; also include counter-examples ...
where the function identifier is unnecessary for anonymous functions. The only exception to the necessity of specifications is for an anonymous function that is passed as an argument to another function: you need not specify it if and only if it is very simple.

The names of the components of the argument need not be consistent between the specification and the program.

Under PRE, be careful not to require any accumulator to be equal to some constant. Indeed, this may be the case at the first call, but any recursive call will almost certainly be for a value different from that constant, and would thus violate such a pre-condition.

Under PRE and POST, there is no need to repeat the types of the argument and result, as they are already indicated under TYPE.

Under POST, it is sufficient to give the returned expression e, so that the actual post-condition implicitly is "the returned expression is equal to e". Under this convention, writing "this function returns e" is also unnecessarily long.

A function specification can only be useful if all its argument components appear in the post-condition or side effects.

Every value in an abstract datatype or module shall be commented with its specification, as follows:

(* valueIdentifier
   TYPE:  type
   VALUE: ... description of the provided value ...

Everything shall be in English. Specifications are usually written independently of the programming language, to the extent possible. A suitable combination of natural language and rather standard mathematical notation is usually best. Hence write 0 instead of 0.0, prefer ≠ over <>, use · rather than ∗ for multiplications, etc, to the extent possible.

An exercise solution, whether for an assignment or an exam, where at least one function or value is not specified as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct (with respect to the missing specification)!


Every function identifier shall be descriptive of the performed function. Every value identifier shall be descriptive of the provided value.



Recursive Functions

Every recursive function shall be commented with the chosen numeric variant, as follows:
(* VARIANT: ... *)

Like the pre- and post-conditions, the variant must refer to the parameter names in the specification, but not to the possibly different parameter names in the program. The reason for this is that the variant reflects a decision made before the program was written, according to the design methodology. Also, the variant is not part of the specification, but rather part of the verification outline of why the program is believed correct. For a given specification, many programs can be written, and the recursive ones usually have different variants.

An exercise solution, whether for an assignment or an exam, where at least one recursive function is not commented as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct!

Representation Conventions and Invariants

Every (abstract) datatype shall be commented with its representation convention and invariant, as follows:
(* REPRESENTATION CONVENTION: ... description of how the modelled objects are represented by values of the type ...
   REPRESENTATION INVARIANT:  ... property, if any, that must always hold (as an implicit pre-condition and post-condition) ...

An exercise solution, whether for an assignment or an exam, where at least one (abstract) datatype is not commented as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct!


(* fact n
   TYPE: int -> int
   PRE:  n ≥ 0
   POST: the factorial of n
   EXAMPLES: fact 0 = 1
             fact 3 = 6
(* VARIANT: n *)
fun fact 0 = 1
  | fact n = n * fact (n-1)

(* select n L
   TYPE: int -> int list -> int list
   PRE:  (none)
   POST: the list of the elements in L that are larger than n,
         in the same order as they occur in L
   EXAMPLES: select 2 [1,3,2,4,3] = [3,4,3]
             select 3 [1,3,1]     = []
             select 0 []          = []
(* VARIANT: the length of L *)
fun select _ [] = []
  | select n (x::L) =
      val L' = select n L
      if x>n then x::L' else L'

abstype 'b bsTree = Void
                  | Bst of (int * 'b) * 'b bsTree * 'b bsTree
   a binary search tree with key-value pair (k,s) in the root,
   left subtree L, and right subtree R is represented by Bst((k,s),L,R)
   for Bst((k,s),L,R):
    - every element of L has a key smaller than k
    - every element of R has a key  larger than k
  (* emptyBsTree
     TYPE:  'b bsTree
     VALUE: the empty binary search tree
  val emptyBsTree = Void
  (* exists k T
     TYPE: int -> 'b bsTree -> bool
     PRE:  (none)
     POST: true if T contains a node with key k, and false otherwise
  (* VARIANT: the number of nodes of T *)
  fun exists k Void = false
    | exists k (Bst((key,s),L,R)) =
      if k = key then
	  if k < key then
	      exists k L
	      exists k R

Last modified: Thu Oct 27 10:25:23 CEST 2016