polymorphism and impredicativity

logical verification week 10 2004 11 17

polymorphism

the course

propositional logic ↔ simple type theory

λ→

predicate logic ↔ type theory with dependent types

λP

2nd order propositional logic ↔ polymorphic type theory

λ2

the lambda cube

[figure: λω; λC; λ2; polymorphism; λP 2; λ\underline{ω}; λP \underline{ω}; λ→; dependence; λP]

polymorphism

we had functions & quantification over the elements of a type

\begin{matrix}λn : nat . · · · \\ ∀n : nat . · · · \end{matrix}

                    fun n : nat => . . .
                 forall n : nat, . . .

we now add functions & quantification over the types themselves

\begin{matrix}λA : ∗ . · · · \\ ∀A : ∗ . · · · \end{matrix}

                    fun A : Set => . . .
                 forall A : Set, . . .

dependent types versus polymorphism

• dependent types types can take terms as an argument

• polymorphism terms can take types as an argument

the polymorphic identity

natid

identity function on the natural numbers

λn : nat . n

Definition natid : nat -> nat :=
  fun n : nat => n.
Check (natid 0).
Eval compute in (natid 0).

boolid

identity function on the booleans

λb : bool . b

Definition boolid : bool -> bool :=
  fun b : bool => b.
Check (boolid true).
Eval compute in (boolid true).

polyid

polymorphic identity function

λA : ∗. λx : A. x : ΠA : ∗. A → A

Definition polyid : forall A : Set, A -> A :=
  fun A : Set => fun x : A => x.
Check (polyid nat 0).
Check (polyid bool true).
Eval compute in (polyid nat 0).
Eval compute in (polyid bool true).

Notation
Check (polyid nat 0).
Check (polyid _0).
Notation id := (polyid _).
Check (id 0).
Check (id true).
Eval compute in (id 0).
Eval compute in (id true).

lists

natlist
Inductive natlist : Set :=
  natnil : natlist
| natcons : nat -> natlist -> natlist.

3, 1, 4, 1, 5, 9, 2, 6

natlist_dep

generalizing natlist to a dependent type

Inductive natlist_dep : (nat -> Set) :=
  natnil_dep : (natlist_dep O)
| natcons_dep : forall n : nat,
    nat -> (natlist_dep n) -> (natlist_dep (S n)).

boollist
Inductive boollist : Set :=
  boolnil : boollist
| boolcons : bool -> boollist -> boollist.

F, T, F, F, F, T, T, F

polylist

generalizing natlist to a polymorphic type

Inductive polylist (A : Set) : Set :=
  polynil : (polylist A)
| polycons : A -> (polylist A) -> (polylist A).
polylist : forall A : Set, Set
polylist : Set -> Set
polynil  : forall A : Set, (polylist A)
polycons : forall A : Set, A -> (polylist A) -> (polylist A)

examples of polymorphic lists

3, 1

polycons nat 3 (polycons nat 1 (polynil nat))

F, T

polycons bool false (polycons bool true (polynil bool))

… and now in stereo!

Inductive polylist_dep (A : Set) : nat -> Set :=
  polynil_dep : (polylist_dep A O)
| polycons_dep : forall n : nat,
    A -> (polylist_dep A n) -> (polylist_dep A (S n)).

Notation
Notation ni := (polynil _).
Notation co := (polycons _).
Check (co 3 (co 1 ni)).
Check (co false (co true ni)).
Check (co 3 (co true ni)).

… and even more polymorphic

Inductive polylist' : Type :=
  polynil' : polylist'
| polycons' : forall A : Set, A -> polylist' -> polylist'.
polycons' nat 3 (polycons' bool true polynil')

length of a list

natlength
Fixpoint natlength (l : natlist) {struct l} : nat :=
match l with
  natnil => O
| natcons h t => S (natlength t)
end.
natlength : natlist -> nat

polylength
Fixpoint polylength
  (A : Set) (l : polylist A) {struct l} : nat :=
match l with
  polynil   => O
| polycons   h t => S (polylength A t)
end.
polylength : forall A : Set, polylist A -> nat

polylength
Fixpoint polylength' (l : polylist') {struct l} : nat :=
match l with
  polynil' => O
| polycons' A h t => S (polylength' t)
end.
polylength' : polylist' -> nat

applying a function to each element of a list

natmap
Fixpoint natmap
    (f : nat -> nat) (l : natlist) {struct l} : natlist :=
  match l with
    natnil => natnil
  | natcons h t => natcons (f h) (natmap f t)
  end.
natmap : (nat -> nat) -> natlist -> natlist

natmap (λn. n + 10) (3, 1, 4, 1, 5, 9, 2, 6) = (13, 11, 14, 11, 15, 19, 12, 16)

polymap
Fixpoint polymap (A : Set)
  (f : A -> A) (l : polylist A) {struct l} : polylist A :=
match l with
  polynil => polynil A
| polycons h t => polycons A (f h) (polymap A f t)
end.
polymap :
forall A : Set, (A -> A) -> polylist A -> polylist A

… and even more polymorphic

Fixpoint polymap' (A B : Set)
  (f : A -> B) (l : polylist A) {struct l} : polylist B :=
match l with
  polynil => polynil B
| polycons h t => polycons B (f h) (polymap' A B f t)
end.
polymap' :
forall A B : Set, (A -> B) -> polylist A -> polylist B

iterating an operation over a list

natfold
Fixpoint natfold (f : nat -> nat -> nat) (z : nat)
  (l : natlist) {struct l} : nat :=
match l with
  natnil => z
| natcons h t => f h (natfold f z t)
end.
natfold : (nat -> nat -> nat) -> nat -> natlist -> nat

natfold f z (3, 1, 4, 1) = f 3 (f 1 (f 4 (f 1 z)))
natfold ∗ z (3, 1, 4, 1) = 3 ∗ 1 ∗ 4 ∗ 1 ∗ z

sum
Definition sum := natfold plus O.
sum : natlist -> nat
Eval compute in
  sum (natcons 3 (natcons 1 (natcons 4 (natcons 1 natnil)))).

natfold (+) 0 (3, 1, 4, 1) = 3 + 1 + 4 + 1 + 0 = 9

polyfold
Fixpoint polyfold (A B : Set) (f : A -> B -> B) (z : B)
  (l : polylist A) struct l : B :=
match l with
  polynil => z
| polycons h t => f h (polyfold A B f z t)
end.
polyfold :
forall A B : Set, (A -> B -> B) -> B -> polylist A -> B

sum defined with polyfold
Definition sum' := polyfold nat nat plus O.
Definition sum' := polyfold __plus O.
sum' : polylist nat -> nat
Eval compute in sum' (co 3 (co 1 (co 4 (co 1 ni)))).

impredicativity

Russell’s paradox

Cantor: power set is bigger than the set itself naive set theory

P(Set) ⊆ Set
{x | x ∉ x} ∈ {x | x ∉ x}
⇕
{x | x ∉ x} ∉ {x | x ∉ x}

inconsistent

impredicativity

λ2 is impredicative

bool : ∗ ⊢ ∗ → bool : ∗
P(Set) ∈ Set

⊢ (ΠA : ∗. A) : ∗

Coq Prop is impredicative, Set is predicative

                (forall A : Prop, A) : Prop
                (forall A : Set , A) : Type

λ2 is inconsistent with classical mathematics

bool : ∗ ⊢ ΠA : ∗. (A → bool) : ∗

‘set of functions that map each set into a subset of that set’

U := ∏_{A∈Set} P(A) ∈ Set

U = P(U) × …

the paradox

U := ∏_{A∈Set} P(A) ∈ Set

if u ∈ U then for each A ∈ Set holds that u(A) ∈ P(A) in particular u(U) ∈ P(U)

X := {u ∈ U | u ∉ u(U)} ∈ P(U)

take some x ∈ U such that x(U) = X

x ∈ x(U) ⇔ x ∈ X ⇔ x ∉ x(U)