Skip to content

Instantly share code, notes, and snippets.

@eduardoleon
Last active August 29, 2015 14:14
Show Gist options
  • Save eduardoleon/30da2667dd1465c73c3f to your computer and use it in GitHub Desktop.
Save eduardoleon/30da2667dd1465c73c3f to your computer and use it in GitHub Desktop.
Simply-typed lambda calculus. Which one is clearer: termDen or termDenote?
Require Import List.
Section HList.
Variable A : Type.
Variable B : A -> Type.
Inductive hlist : list A -> Type :=
| HNil : hlist nil
| HCons : forall x xs, B x -> hlist xs -> hlist (x :: xs).
Variable e : A.
Inductive index : list A -> Type :=
| IZero : forall xs, index (e :: xs)
| ISucc : forall x xs, index xs -> index (x :: xs).
Definition hget xs (ys : hlist xs) (i : index xs) : B e.
Proof. induction ys; inversion i; firstorder. Defined.
End HList.
Recursive Extraction hget.
Arguments hlist [A] B _.
Arguments HNil [A B].
Arguments HCons [A B x xs] _ _.
Notation "x ::: xs" := (HCons x xs) (at level 60).
Arguments index [A] _ _.
Arguments IZero [A e xs].
Arguments ISucc [A e x xs] _.
Arguments hget [A B e xs] _ _.
Require Import List.
Require Import HList.
Inductive ty :=
| Unit : ty
| Arrow : ty -> ty -> ty.
Notation "T1 ~> T2" := (Arrow T1 T2) (at level 20).
Fixpoint typeDenote T :=
match T with
| Unit => unit
| T1 ~> T2 => typeDenote T1 -> typeDenote T2
end.
Reserved Notation "G ⊢ T" (at level 80).
Inductive term : list ty -> ty -> Type :=
| Const : forall {G}, G ⊢ Unit
| Var : forall {G T}, index T G -> G ⊢ T
| Abs : forall {G T1 T2}, T1 :: G ⊢ T2 -> G ⊢ T1 ~> T2
| App : forall {G T1 T2}, G ⊢ T1 ~> T2 -> G ⊢ T1 -> G ⊢ T2
where "G ⊢ T" := (term G T).
Definition termDen {G T} (t : G ⊢ T) (xs : hlist typeDenote G) : typeDenote T.
Proof.
induction t.
exact tt.
exact (hget xs i).
exact (fun x => IHt (x ::: xs)).
exact ((IHt1 xs) (IHt2 xs)).
Defined.
Fixpoint termDenote {G T} (t : G ⊢ T) : hlist typeDenote G -> typeDenote T :=
match t with
| Const _ => fun xs => tt
| Var _ _ i => fun xs => hget xs i
| Abs _ _ _ t => fun xs => fun x => termDenote t (x ::: xs)
| App _ _ _ t1 t2 => fun xs => (termDenote t1 xs) (termDenote t2 xs)
end.
Reserved Notation "t₁ → t₂" (at level 90).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment