PolyPolymorphism and Higher-Order Functions

Polymorphic Lists

Instead of defining new lists for each type, like this...

Inductive boollist : Type :=
| bool_nil
| bool_cons (b : bool) (l : boollist).

...Coq lets us give a polymorphic definition that allows list elements of any type:

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

list itself is a function from types to (inductively defined) types.

Check list.
(* ===> list : Type -> Type *)

The parameter X in the definition of list becomes a parameter to the list constructors.

Check (nil nat).
(* ===> nil nat : list nat *)

Check (cons nat 3 (nil nat)).
(* ===> cons nat 3 (nil nat) : list nat *)

Check nil.
(* ===> nil : forall X : Type, list X *)

Check cons.
(* ===> cons : forall X : Type, X -> list X -> list X *)

Notation: In .v files, the "forall" quantifier is spelled out in letters. In the generated HTML files, it is usually typeset as the usual mathematical "upside down A."

Check (cons nat 2 (cons nat 1 (nil nat))).

(We've written nil and cons explicitly here because we haven't yet defined the [] and :: notations for the new version of lists. We'll do that in a bit.)

We can now define polymorphic versions of the functions we've already seen...

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.

Example test_repeat2 :
repeat bool false 1 = cons bool false (nil bool).
Proof. reflexivity. Qed.

Recall the types of cons and nil:

nil : ∀X : Type, list X
cons : ∀X : Type, X → list X → list X

What is the type of cons bool true (cons nat 3 (nil nat))?

(1) nat → list nat → list nat

(2) ∀ (X:Type), X → list X → list X

(3) list nat

(4) list bool

(5) Ill-typed

Recall the definition of repeat:

    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.

What is the type of repeat?

(1) nat → nat → list nat

(2) X → nat → list X

(3) ∀ (X Y: Type), X → nat → list Y

(4) ∀ (X:Type), X → nat → list X

(5) Ill-typed

What is the type of repeat nat 1 2?

(1) list nat

(2) ∀ (X:Type), X → nat → list X

(3) list bool

(4) Ill-typed

Type Annotation Inference

Let's write the definition of repeat again, but this time we won't specify the types of any of the arguments. Will Coq still accept it?

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

Indeed it will. Let's see what type Coq has assigned to repeat':

Check repeat'.
(* ===> forall X : Type, X -> nat -> list X *)
Check repeat.
(* ===> forall X : Type, X -> nat -> list X *)

Coq has used type inference to deduce the proper types for X, x, and count.

Type Argument Synthesis

Supplying every type argument is also boring, but Coq can usually infer them:

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 Arguments

We can go further and even avoid writing _'s in most cases by telling Coq always to infer the type argument(s) of a given function.

The Arguments directive specifies the name of the function (or constructor) and then lists its argument names, with curly braces around any arguments to be treated as implicit. (If some arguments of a definition don't have a name, as is often the case for constructors, they can be marked with a wildcard pattern _.)

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.

Now, we don't have to supply type arguments at all:

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

Alternatively, we can declare arguments implicit by surrounding them with 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.

Here are polymorphic versions of a few more functions that we'll need later:

Fixpoint app {X : Type} (l₁ l₂ : list X)
             : (list X) :=
  match l₁ with
  | nil ⇒ l₂
  | cons h t ⇒ cons h (app t l₂)
  end.

Fixpoint rev {X:Type} (l:list X) : list X :=
  match l with
  | nil ⇒ nil
  | cons h t ⇒ app (rev t) (cons h nil)
  end.

Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil ⇒ 0
  | cons _ l' ⇒ S (length l')
  end.

Example test_rev1 :
rev (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity. Qed.

Example test_rev2:
rev (cons true nil) = cons true nil.
Proof. reflexivity. Qed.

Example test_length1: length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity. Qed.

Supplying Type Arguments Explicitly

We prefer to tell Coq to always try to infer type arguments. But, occasionally this can lead to problems:

Fail Definition mynil := nil.

We can fix this with an explicit type declaration:

Definition mynil : list nat := nil.

Alternatively, we can force the implicit arguments to be explicit by prefixing the function name with @.

Check @nil.

Definition mynil' := @nil nat.

Using argument synthesis and implicit arguments, we can define concrete notations that work for lists of any type.

Notation "x :: y" := (cons x y)
(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
(at level 60, right associativity).

Definition list123''' := [1; 2; 3].

Which type does Coq assign to the following expression?

[1,2,3]

(1) list nat

(2) list bool

(3) bool

(4) No type can be assigned

What about this one?

[3 + 4] ++ nil

(1) list nat

(2) list bool

(3) bool

(4) No type can be assigned

What about this one?

andb true false ++ nil

(1) list nat

(2) list bool

(3) bool

(4) No type can be assigned

What about this one?

[1; nil]

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

What about this one?

[[1]; nil]

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

And what about this one?

[1] :: [nil]

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

This one?

@nil bool

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

This one?

nil bool

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

This one?

@nil 3

(1) list nat

(2) list (list nat)

(3) list bool

(4) No type can be assigned

Polymorphic Pairs

Similarly...

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

Arguments pair {X} {Y} _ _.

Notation "( x , y )" := (pair x y).

We can also use the Notation mechanism to define the standard notation for product types:

Notation "X * Y" := (prod X Y) : type_scope.

(The annotation : type_scope tells Coq that this abbreviation should only be used when parsing types. This avoids a clash with the multiplication symbol.)

Be careful not to get (X,Y) and X*Y confused!

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with
  | (x, y) ⇒ x
  end.

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with
  | (x, y) ⇒ y
  end.

What does this function do?

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match lx, ly with
  | [], _ ⇒ []
  | _, [] ⇒ []
  | x :: tx, y :: ty ⇒ (x, y) :: (combine tx ty)
  end.

Polymorphic Options

Module OptionPlayground.

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

Arguments Some {X} _.
Arguments None {X}.

End OptionPlayground.

Fixpoint nth_error {X : Type} (l : list X) (n : nat)
                   : option X :=
  match l with
  | [] ⇒ None
  | a :: l' ⇒ if n =? O then Some a else nth_error l' (pred n)
  end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.

Proof. reflexivity. Qed.

Example test_nth_error2 : nth_error [[1];[2]] 1 = Some [2].

Proof. reflexivity. Qed.

Example test_nth_error3 : nth_error [true] 2 = None.

Proof. reflexivity. Qed.

Functions as Data

Higher-Order Functions

Functions in Coq are first class.

Definition doit3times {X:Type} (f:X→X) (n:X) : X :=
f (f (f n)).

Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)

Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.

Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.

Filter

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.

Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.

Definition length_is_1 {X : Type} (l : list X) : bool :=
(length l) =? 1.

Example test_filter2:
    filter length_is_1
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

The filter function — together with some other functions we'll see later — enables a powerful collection-oriented programming style.

Definition countoddmembers' (l:list nat) : nat :=
length (filter oddb l).

Example test_countoddmembers'1: countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2: countoddmembers' [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3: countoddmembers' nil = 0.
Proof. reflexivity. Qed.

Anonymous Functions

Functions can be constructed "on the fly" without giving them names.

Example test_anon_fun':
doit3times (fun n ⇒ n * n) 2 = 256.
Proof. reflexivity. Qed.

The expression (fun n ⇒ n * n) can be read as "the function that, given a number n, yields n * n."

Example test_filter2':
    filter (fun l ⇒ (length l) =? 1)
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

Map

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_map1: map (fun x ⇒ plus 3 x) [2;0;2] = [5;3;5].
Proof. reflexivity. Qed.

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

Example test_map3:
map (fun n ⇒ [evenb n;oddb n]) [2;1;2;5]
= [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity. Qed.

Recall the definition of map:

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

What is the type of map?

(1) ∀ X Y : Type, X → Y → list X → list Y

(2) X → Y → list X → list Y

(3) ∀ X Y : Type, (X → Y) → list X → list Y

(4) ∀ X : Type, (X → X) → list X → list X

Lists are not the only inductive type for which map makes sense. Here is a map for the option type:

Definition option_map {X Y : Type} (f : X → Y) (xo : option X)
                      : option Y :=
  match xo with
    | None ⇒ None
    | Some x ⇒ Some (f x)
  end.
(* /HIDEFROMHTML *)

Fold

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.

This is the "reduce" in map/reduce...

Check (fold andb).
(* ===> fold andb : list bool -> bool -> bool *)

Example fold_example1 :
fold mult [1;2;3;4] 1 = 24.

Proof. reflexivity. Qed.

Example fold_example2 :
fold andb [true;true;false;true] true = false.

Proof. reflexivity. Qed.

Example fold_example3 :
fold app [[1];[];[2;3];[4]] [] = [1;2;3;4].

Proof. reflexivity. Qed.

Here is the definition of fold again:

     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.

What is the type of fold?

(1) ∀ X Y : Type, (X → Y → Y) → list X → Y → Y

(2) X → Y → (X → Y → Y) → list X → Y → Y

(3) ∀ X Y : Type, X → Y → Y → list X → Y → Y

(4) X → Y→ X → Y → Y → list X → Y → Y

What is the type of fold plus?

(1) ∀ X Y : Type, list X → Y → Y

(2) nat → nat → list nat → nat → nat

(3) ∀ Y : Type, list nat → Y → nat

(4) list nat → nat → nat

(5) ∀ X Y : Type, list nat → nat → nat

What does fold plus [1;2;3;4] 0 simplify to?

(1) [1;2;3;4]

(2) 0

(3) 10

(4) [3;7;0]

Functions That Construct Functions

Here are two more functions that return functions as results.

Definition constfun {X: Type} (x: X) : nat→X :=
fun (k:nat) ⇒ x.

Definition ftrue := constfun true.

Example constfun_example1 : ftrue 0 = true.

Proof. reflexivity. Qed.

Example constfun_example2 : (constfun 5) 99 = 5.

Proof. reflexivity. Qed.

A two-argument function in Coq is actually a function that returns a function!

Check plus.
(* ==> nat -> nat -> nat *)

Definition plus3 := plus 3.
Check plus3.

Example test_plus3 : plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' : doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' : doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.