「SF-LC」4 Poly

The critical new ideas are polymorphism (abstracting functions over the types of the data they manipulate) and higher-order functions (treating functions as data).

Polymorphism

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:

代码语言：javascript复制

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

Polymorphic Type and Constructors

But of course Coq supports polymorphic type. So we can abstract things over type

代码语言：javascript复制

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.

Q1. What’s the type of `nil` and `cons`?

Both having forall type

代码语言：javascript复制

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

Q2. What’s the type of `list nat`? Why not `Type` but weird `Set`?

代码语言：javascript复制

Check nat.
(* ===> nat : Set *)
Check list nat.
(* ===> list nat : Set *)
Check Set.
(* ===> Set: Type *)
Check Type.
(* ===> Type: Type *)

代码语言：javascript复制

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

Polymorphic Functions

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.

代码语言：javascript复制

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.

代码语言：javascript复制

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

Slide QA

ill-typed
forall X : Type, X -> nat -> list X
list nat

Type Argument Inference

X must be a Type since nil expects an Type as its first argument.

代码语言：javascript复制

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 *)

Type Argument Synthesis

We can write _ (hole) in place of X and Coq will try to unify all local information.

代码语言：javascript复制

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:

代码语言：javascript复制

repeat' X x count : list X :=
repeat' (X : _) (x : _) (count : _) : list X :=

Implicit Arguments

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.

代码语言：javascript复制

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.

代码语言：javascript复制

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

Implicit Arguments Pitfalls on `Inductive`

代码语言：javascript复制

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

Doing this will make X implicit for even list', the type constructor itself…

Other Polymorphic List functions

No difference but add implicit type argument {X : Type}.

Supplying Type Arguments Explicitly

代码语言：javascript复制

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)

代码语言：javascript复制

Check nil.

nil : 
   list ?X
where ?X : [ |- Type]

List notation

代码语言：javascript复制

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

Slide Q&A 2

we use ; not ,!!
list nat
ill-typed
ill-typed
list (list nat)
list (list nat) (tricky in first look)
list bool
ill-typed
ill-typed

Poly Pair

代码语言：javascript复制

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`

代码语言：javascript复制

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?

代码语言：javascript复制

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]

Poly Option

代码语言：javascript复制

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.

Function as data

Functions as first-class citizens

Higher-Order Functions

代码语言：javascript复制

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

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

Filter (taking a predicate on `X`)

collection-oriented programming style - my first time seeing this, any comments?

代码语言：javascript复制

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.

Anonymous Functions

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

代码语言：javascript复制

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)

代码语言：javascript复制

Compute ((fun x y => x   y) 3 5).

Map

Should be familar.

代码语言：javascript复制

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

代码语言：javascript复制

Check @map

@map : forall X Y : Type, (X -> Y) -> list X -> list Y

Slide Q&A 3

as above

`option` map

代码语言：javascript复制

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.

Functor Map (fmap) !

Fold (Reduce)

代码语言：javascript复制

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.

代码语言：javascript复制

Check @fold

@fold
     : forall X Y : Type,
       (X -> Y -> Y) -> list X -> Y -> Y

Slide Q&A 4

as above (type can be simply readed out)
list nat -> nat -> nat
10

Functions That Construct Functions

Should be familar. Use of closure.

代码语言：javascript复制

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

代码语言：javascript复制

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

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

Universe Inconsistency

I encounter this problem when doing church numeral exercise.

代码语言：javascript复制

Definition plus (n m : cnat) : cnat := n cnat succ m.

will result in universe inconsistency error.

代码语言：javascript复制

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).

What’s happening?

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

https://stackoverflow.com/questions/32153710/what-does-error-universe-inconsistency-mean-in-coq

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.

代码语言：javascript复制

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 type Type_j, for any index j > 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 the forall in the definition of nat is quantified over Type_i, but Coq’s logic forces nat to be itself of type Type_j, with j > i. On the other hand, the application n nat requires that j <= i, resulting in a non-satisfiable set of index constraints.

From my understanding, the essences are:

reasons: Allowing self-application introduces logic contradiction (paradox).
understanding: The forall is quantified over types in the previous universe (the universe w/o itself).

From https://coq.inria.fr/refman/addendum/universe-polymorphism.html

代码语言：javascript复制

Definition identity {A : Type} (a : A) := a.

Fail Definition selfid := identity (@identity).

代码语言：javascript复制

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

Polymorphic Church Numerals w/o self-applying itself

References: https://en.wikipedia.org/wiki/Church_encoding

Definition

Untyped doesn’t need to declare type… STLC doesn’t have enough expressive power to represent church encoding System F definition:

代码语言：javascript复制

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

`succ`

代码语言：javascript复制

succ = n s z -> s (n s z)

代码语言：javascript复制

Definition succ (n : cnat) : cnat :=
  fun X s z => s (n X s z).

`plus`

代码语言：javascript复制

plus = m n -> m scc n
plus = m n s z -> m s (n s z)

代码语言：javascript复制

Definition plus (n m : cnat) : cnat :=
  n cnat succ m.                (* System F *)
  fun X s z => n X s (m X s z). (* Coq *)

代码语言：javascript复制

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`

代码语言：javascript复制

mult = m n -> m (plus n) n0

代码语言：javascript复制

Definition mult (n m : cnat) : cnat :=
  n cnat (plus m) zero.         (* SystemF *)
  fun X s z => (m X (n X s) z). (* Coq *)

代码语言：javascript复制

mult = 
  lambda m:CNat.
  lambda n:CNat. 
    m [CNat] (plus n) c0;   /* partial app `plus` */

`exp`

代码语言：javascript复制

pow = m n -> m (mult n) n1
exp = m n -> n m

代码语言：javascript复制

Definition exp (n m : cnat) : cnat :=
  n cnat (mult m) one         (* SystemF *)
  fun X => m (X -> X) (n X).  (* Coq *)

nat NAT网关

0 人点赞

「SF-LC」4 Poly

Polymorphism

Polymorphic Type and Constructors

Q1. What’s the type of nil and cons?

Q2. What’s the type of list nat? Why not Type but weird Set?

Polymorphic Functions

Slide QA

Type Argument Inference

Type Argument Synthesis

Implicit Arguments

Implicit Arguments Pitfalls on Inductive

Other Polymorphic List functions

Supplying Type Arguments Explicitly

List notation

Slide Q&A 2

Poly Pair

Combine or Zip

Poly Option

Function as data

Higher-Order Functions

Filter (taking a predicate on X)

Anonymous Functions

Map

Slide Q&A 3

option map

Fold (Reduce)

Slide Q&A 4

Functions That Construct Functions

Universe Inconsistency

What’s happening?

https://stackoverflow.com/questions/32153710/what-does-error-universe-inconsistency-mean-in-coq

From https://coq.inria.fr/refman/addendum/universe-polymorphism.html

Polymorphic Church Numerals w/o self-applying itself

Definition

succ

plus

mult

exp

Q1. What’s the type of `nil` and `cons`?

Q2. What’s the type of `list nat`? Why not `Type` but weird `Set`?

Implicit Arguments Pitfalls on `Inductive`

`Combine` or `Zip`

Filter (taking a predicate on `X`)

`option` map

`succ`

`plus`

`mult`

`exp`