PolyPolymorphism and Higher-Order Functions


Require Export Lists.

Polymorphism

Polymorphic Lists

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

Inductive boollist : Type :=
  | bool_nil : boollist
  | bool_cons : bool → boollist → boollist.

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

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

list itself is a function from types to (inductively defined) types.
Notice how the types of the constructors change:

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

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

(We've gone back to writing 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 (or generic) versions of some functions we've already seen...

Fixpoint length (X:Type) (l:list X) : nat :=
  match l with
  | nil ⇒ 0
  | cons h t ⇒ S (length X t)
  end.

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

Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity. Qed.

Polymorphic versions of a few more functions that we'll need later:

Fixpoint app (X : Type) (l1 l2 : list X)
                : (list X) :=
  match l1 with
  | nil ⇒ l2
  | cons h t ⇒ cons X h (app X t l2)
  end.

Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
  match l with
  | nil ⇒ cons X v (nil X)
  | cons h t ⇒ cons X h (snoc X t v)
  end.

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

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) No type can be assigned.

Recall the definition of app:
      Fixpoint app (X : Type) (l1 l2 : list X)
                      : (list X) :=
        match l1 with
        | nil      ⇒ l2
        | cons h t ⇒ cons X h (app X t l2)
        end.
What is the type of app?
(1) list nat → list nat → list nat
(2) list X → list X → list X
(3) ∀ (X Y:Type), list X → list Y → list Y
(4) ∀ (X:Type), list X → list X → list X
(5) No type can be assigned.

What is the type of app nat [1;2] [3;4]?
(1) list nat
(2) ∀ (X:Type), list X → list X → list X
(3) list bool
(4) No type can be assigned.

Type Annotation Inference

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

Fixpoint app' X l1 l2 : list X :=
  match l1 with
  | nil ⇒ l2
  | cons h t ⇒ cons X h (app' X t l2)
  end.

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

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

Coq has used type inference to deduce the proper types for X, l1, and l2.

Type Argument Synthesis

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

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

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

Implicit Arguments

If fact, we can go further. To avoid having to sprinkle _'s throughout our programs, we can tell 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.

Arguments nil {X}.
Arguments cons {X} _ _. (* use underscore for argument position that has no name *)
Arguments length {X} l.
Arguments app {X} l1 l2.
Arguments rev {X} l.
Arguments snoc {X} l v.

(* note: no _ arguments required... *)
Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
Check (length list123'').

Alternatively, we can declare arguments implicit by surrounding them with curly braces in the definition:

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

We prefer to tell Coq to always try to infer type arguments. But, occasionally this can cause a problem:

(* 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 assignment

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?
   [@nil 3]
(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 bool
(3) list (list nat)
(4) No type can be assigned

Polymorphic Pairs

Similarly...

Inductive prod (X Y : Type) : Type :=
  pair : X → Y → prod X Y.

Arguments pair {X} {Y} _ _.

As with lists, we make the type arguments implicit and define the familiar concrete notation.

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

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

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

(The annotation : type_scope tells Coq that this abbreviation should 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.

Note that the pair notation can be used both in expressions and in patterns...

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

Similarly...

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

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

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

Example test_index1 : index 0 [4;5;6;7] = Some 4.
Proof. reflexivity. Qed.
Example test_index2 : index 1 [[1];[2]] = Some [2].
Proof. reflexivity. Qed.
Example test_index3 : index 2 [true] = None.
Proof. reflexivity. Qed.

Functions as Data

Higher-Order Functions

Functions in Coq are first class.
For example, here is a function that applies another function three times.

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.

Partial Application

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.

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 :=
  beq_nat (length l) 1.

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

filter (along with other similar sorts of functions we'll see later, such as map and fold) enables a convenient, high-level 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.

Example test_filter2':
    filter (fun l ⇒ beq_nat (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 (plus 3) [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

Recall that evenb has type nat → bool.
What is the type of map evenb?
(1) ∀ X Y : Type, (X → Y) → list X → list Y
(2) list nat → list bool
(3) list nat → list Y
(4) ∀ Y : Type, list nat → list Y

A mapping function for options:

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.

Fold

The "reduce" in map/reduce...

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.

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 For Constructing 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.

Definition override {X: Type} (f: nat→X) (k:nat) (x:X) : nat→X:=
  fun (k':nat) ⇒ if beq_nat k k' then x else f k'.

Definition fmostlytrue := override (override ftrue 1 false) 3 false.

Example override_example1 : fmostlytrue 0 = true.
Proof. reflexivity. Qed.

Example override_example2 : fmostlytrue 1 = false.
Proof. reflexivity. Qed.

Example override_example3 : fmostlytrue 2 = true.
Proof. reflexivity. Qed.

Example override_example4 : fmostlytrue 3 = false.
Proof. reflexivity. Qed.

We'll use function overriding heavily in parts of the rest of the course, and we will end up needing to know quite a bit about its properties. To prove these properties, though, we need to know about a few more of Coq's tactics; developing these is the main topic of the next chapter. For now, though, let's introduce just one very useful tactic that will also help us with proving properties of some of the other functions we have introduced in this chapter.

The unfold Tactic

Coq doesn't always automatically expand definitions:

Theorem unfold_example_bad : ∀m n,
  3 + n = m →
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
(* At this point, we'd like to do rewrite → H, since 
     plus3 n is definitionally equal to 3 + n.  However, 
     Coq doesn't automatically expand plus3 n to its 
     definition. *)
  Abort.

We can use the unfold tactic to get unstuck.

Theorem unfold_example : ∀m n,
  3 + n = m →
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  unfold plus3.
  rewrite → H.
  reflexivity. Qed.

A simple property of override:
(First, recall this fact, which was an exercise in an early Chapter...)

Lemma beq_nat_refl : ∀n : nat,
  true = beq_nat n n.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Theorem override_eq : ∀{X:Type} x k (f:nat→X),
  (override f k x) k = x.
Proof.
  intros X x k f.
  unfold override.
  rewrite ← beq_nat_refl.
  reflexivity. Qed.

(* $Date: 2013-07-30 12:24:33 -0400 (Tue, 30 Jul 2013) $ *)