| Basic source-level lambda calculus with naturals, products, and sums |
Require Import List.
Require Import Binding.
Set Implicit Arguments.
The language |
| We start by defining the language of data types in a very straightforward way. |
Inductive dty : Set :=
| Nat : dty
| Prod : dty -> dty -> dty
| Sum : dty -> dty -> dty.
| Next are the types in general. |
Inductive ty : Set :=
| Data : dty -> ty
| Arrow : ty -> ty -> ty.
Here is the language of terms.
The type family term is parameterized by a Debruijn-indexed typing context
and type that appear in the typing judgment for a particular term.
The type Var is a generic Debruijn variable type defined in Binding.
|
Inductive term : list ty -> ty -> Set :=
| EVar : forall G t,
Var G t
-> term G t
| Lam : forall G dom ran,
term (dom :: G) ran
-> term G (Arrow dom ran)
| App : forall G dom ran,
term G (Arrow dom ran)
-> term G dom
-> term G ran
| Const : forall G, nat -> term G (Data Nat)
| Pair : forall G t1 t2,
term G (Data t1)
-> term G (Data t2)
-> term G (Data (Prod t1 t2))
| Fst : forall G t1 t2,
term G (Data (Prod t1 t2))
-> term G (Data t1)
| Snd : forall G t1 t2,
term G (Data (Prod t1 t2))
-> term G (Data t2)
| Inl : forall G t1 t2,
term G (Data t1)
-> term G (Data (Sum t1 t2))
| Inr : forall G t1 t2,
term G (Data t2)
-> term G (Data (Sum t1 t2))
| Case : forall G t1 t2 t,
term G (Data (Sum t1 t2))
-> term (Data t1 :: G) t
-> term (Data t2 :: G) t
-> term G t.
Denotational semantics |
We compile data types into their natural Coq Set counterparts.
|
Fixpoint dtyDenote (t : dty) : Set :=
match t with
| Nat => nat
| Prod t1 t2 => (dtyDenote t1 * dtyDenote t2)%type
| Sum t1 t2 => (dtyDenote t1 + dtyDenote t2)%type
end.
| Likewise for types in general |
Fixpoint tyDenote (t : ty) : Set :=
match t with
| Data t => dtyDenote t
| Arrow t1 t2 => tyDenote t1 -> tyDenote t2
end.
Term denotation is further parameterized by a substitution assigning values
to all free variables. The generic type Subst is from Binding.
It is parameterized first, by a denotation function explaining what type of
value we want to include for each type in the typing context; and second, by
the actual typing context to use.
|
Fixpoint termDenote (G : list ty) (t : ty) (e : term G t) {struct e}
: Subst tyDenote G -> tyDenote t :=
match e in (term G t) return (Subst tyDenote G -> tyDenote t) with
| EVar _ _ v => VarDenote v
| Lam _ _ _ e' => fun s x => termDenote e' (SCons _ x s)
| App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s)
| Const _ n => fun _ => n
| Pair _ _ _ e1 e2 => fun s => (termDenote e1 s, termDenote e2 s)
| Fst _ _ _ e => fun s => fst (termDenote e s)
| Snd _ _ _ e => fun s => snd (termDenote e s)
| Inl _ _ _ e1 => fun s => inl _ (termDenote e1 s)
| Inr _ _ _ e2 => fun s => inr _ (termDenote e2 s)
| Case _ t1 t2 _ e e1 e2 => fun s =>
match termDenote e s with
| inl e' => termDenote e1 (SCons (denote:= tyDenote) (Data t1) e' s)
| inr e' => termDenote e2 (SCons (denote:= tyDenote) (Data t2) e' s)
end
end.