The article explores the popular two features in programming:

  • Polymorphism: abstracting functions over the types of the data they manipulate
  • Higher-order Functions: treating functions as data

Polymorphism

I also have an article about polymorphism in CPP in which the concept of polymorphism is discussed deeper. Check it out: Runtime-Polymorphism-CPP

Coq support polymorphic inductive type, which means we can define polymorphic datatype. Here is an example of polymorphic list:

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).


Check (cons nat 3 (nil nat)): list nat

In addition to parameters defined in argument list (x:X) and (l: list X), the polymorphic datatype takes an additional argument (X:type). In application, the X in the definition of list becomes a parameter to the constructors.

Similarly, functions can be defined polymorphically.

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.

Example test_repeat1 :
  repeat nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
Proof. reflexivity. Qed.

Type Inference

It’s could be sometime tedious to specify which type are using each time. To solve this, Coq supports type inference to guess the type from the context. For example, this definition is the same as the previous one.

Fixpoint repeat' X x count: list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat' X x count')
  end.

Coq can guess the information of types of X x count by the use of constructor nil and cons. But I don’t personally like this definition, since it scarifies the readability.

Another type inference feature is to use a “hole” _ to replace the type argument when invoking functions. It tells Coq “please guess the type and fill in the hole”:

Fixpoint repeat'' X x count : list X :=
  match count with
  | 0        => nil _
  | S count' => cons _ x (repeat'' _ x count')
  end.

Definition list123' :=
  cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Implicit Type Arguments

In most cases, we can even avoid writing _s by telling Coq always to infer the type arguments. The first way to do this is to use Arguments directives:

Arguments nil {X}.
Arguments cons {X}.
Arguments repeat {X}.

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

After executing Arguments, we don’t have to supply the type arguments for the functions anymore. It is by default to let Coq guess it.

A more convenient way to make implicit type arguments is to use curly braces instead of parens:

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0        => nil
  | S count' => cons x (repeat''' x count')
  end.

I think this definition meet my aesthetic: every parameter has type notations, and the type parameter X is by default implicitly given.

The prefix @ can be added to the front of a function to force the implicit arguments to be explicit.

Compute repeat''' 4 2.
Fail Compute @repeat''' 4 2.
Compute @repeat''' nat 4 2.

The Fail keyword make sure that the following command indeed fails

Proofs involving implicit type arguments do not nontrivially have more difficulty. Just remember the grammar rules. (Exercise poly_exercises)

Theorem app_nil_r : forall (X:Type), forall l:list X,
  l ++ [] = l.
Proof.
  intros X l. induction l as [| X' l' iHl]. (* extra type argument: X' *)
  - simpl. reflexivity.
  - simpl. rewrite -> iHl. reflexivity.
Qed.

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n. induction l as [| A' l' iHl].
  - simpl. reflexivity.
  - simpl. rewrite iHl. reflexivity.
Qed.

Theorem rev_app_distr: forall X (l1 l2 : list X),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros X l1 l2.
  Print app.
  induction l1.
  - simpl. rewrite app_nil_r. reflexivity.
  - simpl. rewrite IHl1.  rewrite app_assoc. reflexivity.
  Qed.

More Polymorphic Datatypes

Polymorphic pairs and options defined as

Inductive prod (X Y : Type) : Type :=
	| pair (x : X) (y : Y).

Inductive option (X:Type) : Type :=
  | Some (x : X)
  | None.

An example of using them is the exercise split:

(* X Y are both implicitly defined *)

Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y):=
  match l with
    | nil => (nil, nil)
    | (x,y)::[] => ([x],[y])
    | (x,y)::t =>(x :: fst (split t), y :: snd (split t))
  end.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof. reflexivity. Qed.

Functions as Data

Like many other modern programming languages, Coq treats functions as first-class citizens, allowing them to be passed as arguments to other functions.

Functions that manipulate other functions are referred as higher-order functions.

Filter

The most simple non-trivial case to use higher-order functions is arguably the filter function, which takes a list and a predicate on the list, “filtering” the list by the predicate. (exercise filter_even_gt7)

Fixpoint filter {X:Type} (test: X->bool) (l:list X) : list X :=
  match l with
  | [] => []
  | h :: t =>
    if test h then h :: (filter test t)
    else filter test t
  end.

(* keep the item which is even and bigger than 7 *) 
Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun n => andb (even n) (blt_nat 7 n)) l.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
Proof. simpl. reflexivity. Qed.

The expression (fun l => (length l) =? 1) is an anonymous function.

Map

Another commonly used higher-order function is map. (exercise map_rev)

Fixpoint map {X Y : Type} (f : X->Y) (l : list X) : list Y :=
  match l with
  | []     => []
  | h :: t => (f h) :: (map f t)
  end.

Example test_map2:
  map odd [2;1;2;5] = [false;true;false;true].
Proof. reflexivity. Qed.

Lemma map_tail: forall (X Y : Type) (f : X -> Y) (l : list X) (x: X),
  map f (l ++ [x]) = map f(l) ++ [f x].
Proof. 
intros. induction l.
- reflexivity.
- simpl. rewrite IHl. reflexivity.
Qed.

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
intros. induction l.
- reflexivity.
- simpl. rewrite <- IHl. rewrite map_tail. reflexivity.
Qed.

Fold

Fold is a fancy FP name for reduce in many other languages, which takes a accumulator, an initial value and a list to perform the “reduce” process:

Fixpoint fold {X Y: Type} (f : X->Y->Y) (l : list X) (b : Y)
                         : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Example fold_example1 :
  fold mult [1;2;3;4] 1 = 24. (* 1*2*3*4 *)
Proof. reflexivity. Qed.

Church Numerals

The Church Numerals or Church Encodings is s means of representing data and operators in the lambda calculus. Number n are represented by applying functions n times: \(f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}.\)

Definition cnat := forall X : Type, (X -> X) -> X -> X.

Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

Definition two : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

If we pass S (the constructor of nat) as the function f, we can reduce the Church Numerals to the unitary representation of numbers.

Example two_church_peano : two nat S O = 2.
Proof. reflexivity. Qed.

Functions that makes functions

Another kind of higher-order functions are those which construct another functions

Definition nat_manipulation (n: nat) (f: nat -> nat -> nat) :=
  fun (k:nat) => f n k.

Definition add_5 := nat_manipulation 5 plus.

Example add_t_test: (add_5 15) = 20.
Proof. reflexivity. Qed.

The function nat_manipulation receive a nat and a function which takes 2 nats to get a new nat.

In fact, coq supports partial application, which means supplying insufficient arguments to a function is acceptable, and this operation produces a new function with partial arguments bound. The most simple example is plus.

Check plus : nat -> nat -> nat.

Definition plus3 := plus 3. 
Check plus3 : nat -> nat.

Example test_plus3 : plus3 4 = 7.
Proof. reflexivity. Qed.

HM Type Notation

Coq use the HM type notation to describe functions. It is an classical type system originated from lambda calculus. It’s better to look at it.

As we saw the type of plus:

Check plus : nat -> nat -> nat.

Each -> in this expression as actually a binary operator on types. The operators are right-associative, which means it is a shorthand for nat -> (nat -> nat).

The power of HM type notation is that this expression has many ways to interpret. It can be read both

  • “plus is a one-argument function that takes a nat and returns a one-argument function” ,and,
  • “plus can take 2 nats, and returns a another nat”.

It is also legal to have quantifiers in the notation. The Church Numerals are:

Definition cnat := forall X : Type, (X -> X) -> X -> X.

The quantifier forall X: Type states that cnat type needs an explicit type argument.