The critical new ideas are polymorphism (abstracting functions over the types of the data they manipulate) and higher-order functions (treating functions as data).
Until today, We were living in the monomorphic world of Coq. So if we want a list, we have to define it for each type:
Inductive boollist : Type :=
| bool_nil
| bool_cons (b : bool) (l : boollist).
But of course Coq supports polymorphic type. So we can abstract things over type
Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X).
Check list.
(* ===> list : Type -> Type *)
Recall from PLT course, this is exacly Parametric Polymorphism
and it’s SystemFω. the list
here is a type-level small lambda, or type operators
Another things I’d love to mention is the concrete syntax of list X
,
it didn’t choose the SML/OCaml order but the Haskell order.
nil
and cons
?Both having forall
type
Check nil.
(* ===> nil : forall X : Type, list X *)
Check cons.
(* ===> nil : forall X : Type, X -> list X -> list X *)
list nat
? Why not Type
but weird Set
?Check nat.
(* ===> nat : Set *)
Check list nat.
(* ===> list nat : Set *)
Check Set.
(* ===> Set: Type *)
Check Type.
(* ===> Type: Type *)
Check (cons nat 2 (cons nat 1 (nil nat))).
we can make polymorphic versions of list-processing function:
Btw, Pierce follows the TAPL convention where type is written in capital letter but not greek letter, less clear in first look but better for typing in real programming.
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.
This is SystemF.
Check repeat.
(* ===> repeat : forall X : Type, X -> nat -> list X *)
forall X : Type, X -> nat -> list X
list nat
X
must be a Type
since nil
expects an Type
as its first argument.
Fixpoint repeat' X x count : list X := (* return type [:list X] can be omitted as well *)
match count with
| 0 ⇒ nil X
| S count' ⇒ cons X x (repeat' X x count')
end.
Check repeat'.
(* ===> forall X : Type, X -> nat -> list X *)
We can write _
(hole) in place of X
and Coq will try to unify all local information.
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 _))).
Same underlying mechanisms:
repeat' X x count : list X :=
repeat' (X : _) (x : _) (count : _) : list X :=
Using Arguments
directives to tell if an argument need to be implicit (i.e. omitted and always to infer) or not.
Implicitly convert to
_
(synthesis) by frontend.
Arguments nil {X}.
Arguments cons {X} _ _. (* data constructor usually don't specify the name *)
Arguments repeat {X} x count. (* fun definition usually do *)
The even more convenient syntax is that we can declare them right in our function definition. Just surrounding them with curly braces.
Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
match count with
| 0 ⇒ nil
| S count' ⇒ cons x (repeat''' x count')
end.
Inductive
Inductive list' {X:Type} : Type :=
| nil'
| cons' (x : X) (l : list').
Doing this will make X
implicit for even list'
, the type constructor itself…
No difference but add implicit type argument {X : Type}
.
Fail Definition mynil := nil.
Definition mynil : list nat := nil.
Check @nil. (* ===> @nil : forall X : Type, list X *)
Definition mynil' := @nil nat.
First thought: Existential Second thought: A wait to be unified Universal. (after being implicit and require inference)
Check nil.
nil :
list ?X
where ?X : [ |- 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).
Same with before thanks to the implicit argument
;
not ,
!!list nat
list (list nat)
list (list nat)
(tricky in first look)list bool
Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).
Arguments pair {X} {Y} _ _. (* omit two type var **)
Notation "( x , y )" := (pair x y).
Notation "X * Y" := (prod X Y) : type_scope. (* only be used when parsing type, avoids clashing with multiplication *)
Be careful of (X,Y)
and X*Y
. Coq pick the ML way, not haskell way.
Combine
or Zip
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.
Guess type?
Check @combine.
@combine
: forall X Y : Type,
list X -> list Y -> list (X * Y)
(* A special form of `forall`? *)
Check combine.
combine
: list ?X -> list ?Y -> list (?X * ?Y)
where
?X : [ |- Type]
?Y : [ |- Type]
Inductive option (X:Type) : Type :=
| Some (x : X)
| None.
Arguments Some {X} _.
Arguments None {X}.
(* find nth element if exist, None otherwise *)
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.
Functions as first-class citizens
Definition doit3times {X:Type} (f:X→X) (n:X) : X :=
f (f (f n)).
Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)
X
)collection-oriented programming style - my first time seeing this, any comments?
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.
It is arguably a little sad, in the example just above, to be forced to define the function length_is_1 and give it a name just to be able to pass it as an argument to filter
Example test_anon_fun':
doit3times (fun n ⇒ n * n) 2 = 256.
Proof. reflexivity. Qed.
Syntax: hybrid of OCaml fun n -> n
and SML fn n => n
.
and support multi-arguments (curried)
Compute ((fun x y => x + y) 3 5).
Should be familar.
Fixpoint map {X Y: Type} (f:X→Y) (l:list X) : (list Y) :=
match l with
| [] ⇒ []
| h :: t ⇒ (f h) :: (map f t)
end.
Check @map
@map : forall X Y : Type, (X -> Y) -> list X -> list Y
option
mapDefinition option_map {X Y : Type} (f : X → Y) (xo : option X) : option Y :=
match xo with
| None ⇒ None
| Some x ⇒ Some (f x)
end.
Functor Map (fmap
) !
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.
Fold Right (foldr
). Argument order same with OCaml, different with Haskell.
Check @fold
@fold
: forall X Y : Type,
(X -> Y -> Y) -> list X -> Y -> Y
list nat -> nat -> nat
Should be familar. Use of closure.
definition constfun {X: Type} (x: X) : nat→X :=
fun (k:nat) ⇒ x.
Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.
Example constfun_example2 : (constfun 5) 99 = 5.
Curried and partial application
Check plus.
(* ==> nat -> nat -> nat *)
Check plus 3.
(* ==> nat -> nat *)
I encounter this problem when doing church numeral exercise.
Definition plus (n m : cnat) : cnat := n cnat succ m.
will result in universe inconsistency
error.
Set Printing Universes. (* giving more error msg *)
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{Top.168+1}" while it is expected to have type "Type@{Top.168}"
(universe inconsistency: Cannot enforce Top.168 < Top.168 because Top.168 = Top.168).
Yes, you can define:
Definition plus (n m : cnat) : cnat := n cnat succ m.
in System F. However, in Coq’s richer logic, you need to be a little more careful about allowing types to be instantiated at their own types, else you run into issue of inconsistency. Essentially, there is a stratification of types (by “universes”) that says that one universe cannot contain a “bigger” universe. Often, things are polymorphic in their universe (i.e., work in all universes), you run into this where you cannot instantiate the “forall X, …” that is the definition of cnat by cnat itself. — Prof. Fluet
Check Type => Type
is a bit of a lie, everytime it the Type
is not that same, but a bigger one.
Formally, every Type has an index associated to it, called its universe level.
Set Printing Universes. (* giving more error msg *)
Check Type.
Type@{Top.1} : Type@{Top.1+1} (* {Top.1} |= *)
Check Type.
Type@{Top.2} : Type@{Top.2+1} (* {Top.2} |= *)
Thus, the correct answer for that question is that
Type_i
has typeType_j
, for any indexj > i
. This is needed to ensure the consistency of Coq’s theory: if there were only one Type, it would be possible to show a contradiction, similarly to how one gets a contradiction in set theory if you assume that there is a set of all sets. Coq generates one new index variable every time you write Type, and keeps track of internal constraints The error message you saw means that Coq’s constraint solver for universe levels says that there can’t be a solution to the constraint system you asked for. The problem is that theforall
in the definition ofnat
is quantified overType_i
, but Coq’s logic forcesnat
to be itself of typeType_j
, withj > i
. On the other hand, the applicationn nat
requires thatj <= i
, resulting in a non-satisfiable set of index constraints.
From my understanding, the essences are:
forall
is quantified over types in the previous universe (the universe w/o itself).Definition identity {A : Type} (a : A) := a.
Fail Definition selfid := identity (@identity).
The command has indeed failed with message:
The term "@identity" has type "forall A : Type, A -> A"
while it is expected to have type "?A"
(unable to find a well-typed instantiation for "?A": cannot ensure that
"Type@{Top.1+1}" is a subtype of "Type@{Top.1}").
The link also introduce some advanced/experimental way to do polymorphic universe
References: https://en.wikipedia.org/wiki/Church_encoding
Untyped doesn’t need to declare type… STLC doesn’t have enough expressive power to represent church encoding System F definition:
Definition cnat := forall X : Type, (X -> X) -> X -> X.
succ
succ = \n s z -> s (n s z)
Definition succ (n : cnat) : cnat :=
fun X s z => s (n X s z).
plus
plus = \m n -> m scc n
plus = \m n s z -> m s (n s z)
Definition plus (n m : cnat) : cnat :=
n cnat succ m. (* System F *)
fun X s z => n X s (m X s z). (* Coq *)
plus =
lambda m:CNat.
lambda n:CNat. (
lambda X.
lambda s:X->X.
lambda z:X.
m [X] s (n [X] s z)
) as CNat;
plus =
lambda m:CNat.
lambda n:CNat.
m [CNat] succ' n;
mult
mult = \m n -> m (plus n) n0
Definition mult (n m : cnat) : cnat :=
n cnat (plus m) zero. (* SystemF *)
fun X s z => (m X (n X s) z). (* Coq *)
mult =
lambda m:CNat.
lambda n:CNat.
m [CNat] (plus n) c0; /* partial app `plus` */
exp
pow = \m n -> m (mult n) n1
exp = \m n -> n m
Definition exp (n m : cnat) : cnat :=
n cnat (mult m) one (* SystemF *)
fun X => m (X -> X) (n X). (* Coq *)