Predicate Functionals

Predicates and functionals

A predicate is a boolean-valued function (type 'a -> bool). Three key functionals transform predicates:

exists: stop on first true

let rec exists p = function
  | [] -> false
  | x::xs -> (p x) || (exists p xs)
(* val exists : ('a -> bool) -> 'a list -> bool = <fun> *)

Returns true if at least one element satisfies p. The lazy || ensures short-circuit evaluation: as soon as a match is found, the rest of the list is not examined. Without this laziness, exists would always traverse the entire list.

all: stop on first false

let rec all p = function
  | [] -> true
  | x::xs -> (p x) && all p xs
(* val all : ('a -> bool) -> 'a list -> bool = <fun> *)

Returns true if every element satisfies p. The lazy && stops at the first counterexample.

filter: return matching elements

let rec filter p = function
  | [] -> []
  | x::xs -> if p x then x :: filter p xs
            else filter p xs
(* val filter : ('a -> bool) -> 'a list -> 'a list = <fun> *)

Returns the list of all elements satisfying the predicate.

Applications

Membership

let member y xs = exists (fun x -> x = y) xs
(* val member : 'a -> 'a list -> bool = <fun> *)

member tests whether y appears in xs using exists with an anonymous equality predicate.

Intersection

let inter xs ys = filter (fun x -> member x ys) xs
(* val inter : 'a list -> 'a list -> 'a list = <fun> *)

inter filters xs, keeping only those elements that also appear in ys.

Disjointness

let disjoint xs ys = all (fun x -> all (fun y -> x <> y) ys) xs
(* val disjoint : 'a list -> 'a list -> bool = <fun> *)

Returns true if the two lists share no common elements. The inner all checks that x is different from every element of ys; the outer all checks this for every x in xs.

Historical context

Alonzo Church’s λ-calculus gave a simple syntax (λ-notation) for expressing functions. It is the direct precursor of OCaml’s fun-notation. Church’s thesis states that λ-definable functions are precisely the effectively computable ones, equivalent in power to Turing machines.

Peter Landin (Queen Mary College, London) sketched the main features of functional programming languages in 1966. McCarthy’s Lisp, while historically important, initially interpreted variable binding incorrectly - an error that persisted for about twenty years. The λ-calculus has had a profound influence on the design of modern functional languages.