| A compilation from pure Fsub to the Calculus of Constructions |
Warning: You need to run Coq with the -impredicative-set flag to compile this file!
|
Set Implicit Arguments.
The type language |
Here's a generalization of the pure Fsub type language. As you can see, it actually includes the entirety of the Set universe. The idea is that each type stands for a particular Set, and Forall is implemented using HOAS based on this idea. Because of Coq's positivity constraint for inductive definitions, it wouldn't be legal to change Forall's second argument type to ty -> ty; Set is the best I know how to do. I'll prove the interesting theorems about this more general type language, and at the end I'll define a relation that exactly characterizes which tys are true representations of pure Fsub types.
|
Inductive ty : Type :=
| TVar : Set -> ty
| Top : ty
| Arrow : ty -> ty -> ty
| Forall : ty -> (Set -> ty) -> ty.
Some syntactic abbreviations for particular ty constructors
|
Notation "@ x" := (TVar x) (at level 30).
Infix "-->" := Arrow (right associativity, at level 31).
Notation "'All' x <: t1 , t2" := (Forall t1 (fun x => t2)) (at level 32).
A compilation from types to Sets. The Forall case is the interesting one; this translation uses a "coercion-passing style", so a universally quantified type is translated into a function type that takes as arguments a Set and a coercion from it to the domain type.
|
Fixpoint tyDenote (t : ty) : Set :=
match t with
| TVar T => T
| Top => unit
| Arrow t1 t2 => tyDenote t1 -> tyDenote t2
| Forall t1 t2 => forall (T : Set), (T -> tyDenote t1) -> tyDenote (t2 T)
end.
Subtyping |
A context of subtyping facts about variables, which are represented as arbitrary Sets in HOAS style. Each fact gives the Set, its bounding type, and a coercion into that type.
|
Inductive context : Type :=
| CNil : context
| CCons : forall (T : Set) (t : ty), (T -> tyDenote t) -> context -> context.
Notation "'__'" := CNil.
Notation "G ,, x <: t :: c" := (CCons (T:= x) t c G) (at level 40).
| Searching a context for a subtyping fact |
Reserved Notation "[ x <: t :: c ] \in G" (at level 50).
Inductive lookup : context -> forall (T : Set) (t : ty), (T -> tyDenote t) -> Prop :=
| LHead : forall G x t c, [x <: t :: c] \in G,, x <: t :: c
| LTail : forall G x t c x' t' c', [x <: t :: c] \in G -> [x <: t :: c] \in G,, x' <: t' :: c'
where "[ x <: t :: c ] \in G" := (lookup G (T:= x) t c).
| The actual subtyping relation. In addition to the arguments from the written POPLmark spec, my judgment is also with respect to a coercion from the first type to the second. |
Reserved Notation "G |-- t1 <: t2 :: c" (at level 50).
Inductive subTyp : context -> forall (t1 t2 : ty), (tyDenote t1 -> tyDenote t2) -> Prop :=
| SA_Top : forall G S,
G |-- S <: Top :: (fun _ => tt)
| SA_Refl_TVar : forall G X,
G |-- @X <: @X :: (fun x => x)
| SA_Trans_TVar : forall G X U T c1 c2,
[X <: U :: c1] \in G
-> G |-- U <: T :: c2
-> G |-- @X <: T :: (fun x => c2 (c1 x))
| SA_Arrow : forall G S1 S2 T1 T2 c1 c2,
G |-- T1 <: S1 :: c1
-> G |-- S2 <: T2 :: c2
-> G |-- S1 --> S2 <: T1 --> T2 :: (fun f x => c2 (f (c1 x)))
| SA_All : forall G S1 S2 T1 T2 c1 c2,
G |-- T1 <: S1 :: c1
-> (forall X c, G,, X <: T1 :: c |-- S2 X <: T2 X :: c2 X c)
-> G |-- Forall S1 S2 <: Forall T1 T2 :: (fun f X c => c2 X c (f X (fun x => c1 (c x))))
where "G |-- t1 <: t2 :: c" := (subTyp G t1 t2 c).
Terms |
| Terms and typing judgments are combined in a single type, where the type of terms is indexed by a context and type to describe it. |
Inductive tm : context -> ty -> Type :=
| Var : forall G t, tyDenote t -> tm G t
| Lam : forall G t1 t2, (tyDenote t1 -> tm G t2) -> tm G (t1 --> t2)
| App : forall G t1 t2, tm G (t1 --> t2) -> tm G t1 -> tm G t2
| TLam : forall G t1 t2, (forall X c, tm (G,, X <: t1 :: c) (t2 X)) -> tm G (Forall t1 t2)
| TApp : forall G t1 t2, tm G (Forall t1 t2) -> forall t c, G |-- t <: t1 :: c -> tm G (t2 (tyDenote t))
| Cast : forall G t, tm G t -> forall u c, G |-- t <: u :: c -> tm G u.
Notation "# x" := (Var _ _ x) (at level 33).
Infix "!" := App (left associativity, at level 34).
Notation "\ x :: t , e" := (Lam t (fun x => e)) (at level 35).
Notation "e ! [ c ]" := (TApp e c) (left associativity, at level 34).
Notation "\ x <: t :: c , e" := (TLam (t1:= t) _ (fun x c => e)) (at level 35).
Notation "{{ c }} e" := (Cast e c) (at level 36).
| The compilation of a term to the Calculus of Constructions |
Fixpoint tmDenote (G : context) (t : ty) (e : tm G t) {struct e} : tyDenote t :=
match e in (tm G t) return (tyDenote t) with
| Var _ _ v => v
| Lam _ _ _ e' => fun x => tmDenote (e' x)
| App _ _ _ e1 e2 => (tmDenote e1) (tmDenote e2)
| TLam _ _ _ e' => fun T c => tmDenote (e' T c)
| TApp _ _ _ e1 t2 c _ => (tmDenote e1) (tyDenote t2) c
| Cast _ _ e' _ c _ => c (tmDenote e')
end.
The evaluation relation |
| A characterization of evaluation contexts for a term, where each context is associated with a type, a function from terms of that type to terms of the overall context's type, and an argument to which to apply that function to "fill in the hole" to regain the original term. |
Inductive cont : forall G t, tm G t -> forall t', (tm G t' -> tm G t) -> tm G t' -> Prop :=
| Hole : forall G t (e : tm G t),
cont e (fun x => x) e
| AppFun : forall G t1 t2 (e1 : tm G (t1 --> t2)) e2 t' f (v : tm G t'),
cont e1 f v -> cont (e1 ! e2) (fun v => f v ! e2) v
| AppArg : forall G t1 t2 (e1 : tm G (t1 --> t2)) e2 t' f (v : tm G t'),
cont e2 f v -> cont (e1 ! e2) (fun v => e1 ! f v) v
| TypeFun : forall G t1 t2 (e : tm G (Forall t1 t2)) t c (Hst : _ |-- t <: _ :: c)
t' f (v : tm G t'),
cont e f v -> cont (e ! [Hst]) (fun v => f v ! [Hst]) v.
The overall single-step relation. You can see that it's allowed to step a term to a term in a different context. The E_TappTabs rule is to blame, as it adds an extra "garbage" element to the front of the result context. I'm not sure if there's a good way to avoid this, but it seems harmless.
|
Inductive step : forall G t, tm G t -> forall G', tm G' t -> Prop :=
| E_AppAbs : forall G T11 T12 t12 v2,
step (G:= G) ((Lam T11 (t2:= T12) t12) ! v2) (t12 (tmDenote v2))
| E_TappTabs : forall G T11 T12 t12 T2 c (Hst : G |-- T2 <: T11 :: c),
step (TApp (TLam (t1:= T11) T12 t12) Hst) (t12 (tyDenote T2) c)
| E_Ctx : forall G t (e : tm G t) t' f (v : tm G t') v',
cont e f v -> step v v' -> step e (f v').
| We can reassemble a term from a context and the current value of its hole. |
Lemma cont_idem : forall G t (e : tm G t) t' f (v : tm G t'),
cont e f v -> e = f v.
induction 1; congruence.
Qed.
The functions returned by cont are well-behaved with respect to tmDenote.
|
Lemma cont_nonExotic : forall G t (e : tm G t) t' f (v : tm G t'),
cont e f v -> forall v1 v2, tmDenote v1 = tmDenote v2 -> tmDenote (f v1) = tmDenote (f v2).
induction 1; simpl; intuition;
rewrite (IHcont _ _ H0); trivial.
Qed.
step doesn't change the semantics of any term. I can use equality in the conclusion instead of an asymmetric step relation because Coq's definitional equality includes all of the reduction rules necessary to see that the two denotations are equivalent. We reason about Fsub terms in explicit time steps, while reasoning about CIC terms happens in a known strongly normalizing setting, so we can deal with equivalences.
|
Theorem stepOk : forall G t (e : tm G t) G' (e' : tm G' t), step e e' -> tmDenote e = tmDenote e'.
induction 1; trivial.
rewrite (cont_idem H);
apply (cont_nonExotic H); trivial.
Qed.
Ruling out exotic terms |
We might want to have types that stand exactly for "real" representations of pure Fsub types and terms. I'll define these types by way of relations that filter out the bad elements of the more general types we've been using so far. The basic idea is to analyze each type/term with respect to a list of Sets or variable values that are allowed to appear in it as arguments of variable constructors.
|
Lists of Sets
|
Inductive Sets : Type :=
| Snil : Sets
| Scons : Set -> Sets -> Sets.
Finding a Set in a list
|
Inductive InSets : Set -> Sets -> Prop :=
| Shead : forall T TS, InSets T (Scons T TS)
| Stail : forall T T' TS, InSets T TS -> InSets T (Scons T' TS).
| Well-formedness of types |
Inductive ty_nonExotic : Sets -> ty -> Prop :=
| NE_TVar : forall TS T,
InSets T TS
-> ty_nonExotic TS (@T)
| NE_Top : forall TS,
ty_nonExotic TS Top
| NE_Arrow : forall TS t1 t2,
ty_nonExotic TS t1
-> ty_nonExotic TS t2
-> ty_nonExotic TS (t1 --> t2)
| NE_Forall : forall TS t1 t2,
ty_nonExotic TS t1
-> (forall (X : Set), ty_nonExotic (Scons X TS) (t2 X))
-> ty_nonExotic TS (Forall t1 t2).
Lists of values from arbitrary Sets
|
Inductive Values : Type :=
| Vnil : Values
| Vcons : forall (S : Set), S -> Values -> Values.
| Looking up a value in a list |
Inductive InValues : forall (S : Set), S -> Values -> Prop :=
| Vhead : forall (S : Set) (v : S) VS, InValues v (Vcons v VS)
| Vtail : forall (S : Set) (v : S) (S' : Set) (v' : S') VS,
InValues v VS -> InValues v (Vcons v' VS).
| Well-formedness of terms |
Inductive tm_nonExotic : Sets -> Values -> forall G t, tm G t -> Prop :=
| NE_Var : forall TS VS G t (v : tyDenote t),
InValues v VS
-> tm_nonExotic (G:= G) TS VS (#v)
| NE_Lam : forall TS VS G t (e' : _ -> tm G t),
(forall x, tm_nonExotic TS (Vcons x VS) (e' x))
-> tm_nonExotic TS VS (Lam t e')
| NE_App : forall TS VS G t1 t2 (e1 : tm G (t1 --> t2)) e2,
tm_nonExotic TS VS e1
-> tm_nonExotic TS VS e2
-> tm_nonExotic TS VS (e1 ! e2)
| NE_TLam : forall TS VS G t1 t2 (e' : forall X c, tm (G,, X <: t1 :: c) (t2 X)),
(forall X c, tm_nonExotic (Scons X TS) VS (e' X c))
-> tm_nonExotic TS VS (TLam (t1:= t1) _ e')
| NE_TApp : forall TS VS G t1 t2 (e : tm G (Forall t1 t2)) t c (Hst : G |-- t <: t1 :: c),
tm_nonExotic TS VS e
-> ty_nonExotic TS t
-> tm_nonExotic TS VS (e ! [Hst]).
| Now we can build the more precise types as refinements of those defined earlier. |
Definition closed_ty : Type := sigT (ty_nonExotic Snil).
Definition closed_tm (t : ty) : Type := sigT (tm_nonExotic Snil Vnil (G:= __) (t:= t)).
An example: the polymorphic identity function |
| Here's the type of the polymorphic identity function. |
Definition idTy : ty := All X <: Top, @X --> @X.
| Now here's the function itself. It's a bit messy to write because we have to do some higher-order unification manually. |
Definition id : tm __ idTy := TLam (G:= __) (t1:= Top) (fun X => @X --> @X) (fun X c => \x :: @X, #x).
| We want to prove that these are well-formed. Add the inference rules of the relevant judgments to the logic programming database first. |
Hint Constructors InSets InValues ty_nonExotic tm_nonExotic.
We build a closed_ty from idTy and an automatically-generated proof of its well-formedness.
|
Definition idTy_nonExotic : closed_ty.
exists idTy.
unfold idTy.
auto.
Defined.
We build a closed_tm idTy from id and a mostly automatically-generated proof of its well-formedness. It's necessary to provide the first proof step manually, since it involves some manual higher-order unification.
|
Definition id_nonExotic : closed_tm idTy.
exists id.
unfold id.
apply (NE_TLam (TS:= Snil) (VS:= Vnil) (G:= __) (t1:= Top)
(fun x : Set => Arrow (TVar x) (TVar x))); auto.
Defined.
Now we can compile id into CIC.
|
Definition id_compiled := Eval compute in tmDenote id.
| We can take a look at the reduced version of the result. |
Print id_compiled.
| This outputs an OCaml program that defines the polymorphic identity function. |
Extraction id_compiled.