Lecture 3.2: Higher-order Functions and Formal Specification

Higher-order Functions

In general, a higher-order function is a function that either returns a function or takes a function as an argument. We have already encountered the former, since OCaml handles multiple arguments simply by having a function taking the first argument return a function that takes the second argument, which in turn might return a function taking the third argument, and so on.

The latter, functions taking functions as arguments, is a powerful tool for abstracting behavior. In OCaml (and other languages with support for functions as values), this allows us to parametrize code not only by data (primitive values, tuples, lists, etc.), but also by behavior, i.e., other code. Let's look at an example.

Say, we are given a list of integers, and our task is to keep only integers that are greater than 3. Since we want to do this for an arbitrary list, this is a job for a function. We could write something like this.

let rec keep_gr_3 (xs : int list) : int list =
  match xs with
  | [] -> []
  | x :: xs' -> 
    if x > 3 then 
      x :: keep_gr_3 xs' 
    else keep_gr_3 xs'
  ;;

Here it is in action:

utop # keep_gr_3 [1; 2; 3; 4; 5; 6; 7; 8];;
- : int list = [4; 5; 6; 7; 8]

Now, let's say that we want to also be able to filter out non-even numbers (keeping only the even ones). We might implement something like this:

let rec keep_evens (xs : int list) : int list =
  match xs with
  | [] -> []
  | x :: xs' -> 
    if x mod 2 = 0 then 
      x :: keep_evens xs' 
    else keep_evens xs'
  ;;

utop # keep_evens [1; 2; 3; 4; 5; 6; 7; 8];;
- : int list = [2; 4; 6; 8]

We observe that the functions are pretty much the same. What is the same is the structure of recursively processing a list and either prepending an element to the result or skipping it. The only difference is the condition we use to decide whether we keep an element or skip it. The condition itself is dependent on the element of the list, which tells us that it can be abstracted away as a function:

let is_greater_3 (x : int) : bool = x > 3;;
let is_even (x : int) : bool = x mod 2 = 0;;

Since OCaml allows us to pass these two integer predicates as an argument, we can write a "generic" filter function that works for any list of integers and any condition we might want to filter on.

let rec filter_ints (pred : int -> bool) (xs : int list) : int list = 
  match xs with
  | [] -> []
  | x :: xs' -> 
    if pred x then 
      x :: filter_ints pred xs' 
    else filter_ints pred xs'

Note, we can also rewrite the above function using pattern guards. A pattern guard is a boolean condition which restricts when a pattern applies:

let rec filter_ints (pred : int -> bool) (xs : int list) : int list = 
  match xs with
  | [] -> []
  | x :: xs' when pred x -> x :: filter_ints pred xs' 
  | _ :: xs' -> filter_ints pred xs'

Specifications

A specification of a program is a description which allows us to decide whether a particular implementation is correct or not. To make this more formal, a specification defines a set $S$ of correct implementations.

A very basic and straightforward type of specification is simply a comment describing what the expected behavior of a program (function, module, class, ...) is. For example,

(* Return the larger of the two numbers *)
let max (i : int) (j : int) : int = ...

defines a set of correct programs:

\[ S = \{ P\ |\ P \text{ implements "Return the larger of the two numbers"} \} \]

However, we need to ask ourself: how well is the set $S$ defined? The description is vague. We may tend to agree that the following implementation belongs to the set:

let max (i : int) (j : int) : int = 
  if i > j then i else j

On the other hand, we might not fully agree on the membership of the following one:

let max (i : int) (j : int) : int = 
  if i > j then i else
  if i < j then j else
  failwith "There is no larger number"

A specification like this may be enough in many cases, such as, when specifying a subsystem of a video game. If we are tasked with designing and implementing a critical application, such as banking software or an autopilot for an airplane, we might reach for a more precise language and tools.

Another example: Sorting

Let's look at another example: sorting lists. Here's a specification:

(* Sort the list *)
let rec sort (xs : int list) : int list = ...

We should ask ourselves two questions: 1. Can we implement sort following this specification? - We should be able to. There are many algorithms to choose from: insertion sort, quicksort, merge sort, ... 2. Given an implementation of sort can we decide if it satisfies the specification? - Are ascending and descending versions both correct?

How about the following spec?

type row = {
  name : string;
  global_id : string;
  local_id : string;
};;

(* Sort the rows *)
let rec sort_rows (xs : row list) : row list = ...

What are the possible implementations?

For a precise description of the set of possible implementations, we need to turn to specifications written in a formal language with unambiguous meaning, such as mathematics, logic or a programming language.

Formal Specifications

A formal specification is a description of the set of possible implementations using a formal language.

Types are specifications

The types in a language like OCaml are a precise specification of programs. The type checker can unambiguously decide if a program satisfies its specification (type) or not. For example,

let sort (xs : int list) : int list = ...

specifies the set

\[ S = \{ P\ |\ P \text{ has type }\texttt{int list -> int list} \} \]

This is precise but too general to be useful on its own.

There are two approaches to make this set $S$ smaller: use logical properties (like what we have seen in week 1) to constrain the implementation; or use more sophisticated types that can express more properties. We will focus now on the first approach, but later on in this class we will see how polymorphic and abstract types can allow us express tight (as opposed to loose) specifications with types alone.

Using Properties as Specifications

Another way to define a specification is by a set of properties, which are formulas that should be true about your specification. For example, let's think about sorting again. let's make a more precise specification for sort : int list -> int list:

Whenever sort(xs) = ys $$ \forall 0 \le i \le j \le |ys|. ys[i] \le ys[j] $$
Whenever sort(xs) = ys $$ \forall i. \text{count}(xs, i) = \text{count}(ys, i) $$

Note

There are number of other specs that feel right on first glance, but aren't strong enough. For example, what about this one:

\[ \forall i, i \in xs \iff i \in ys.\]

Tomorrow we will demonstrate how to make this computable.