Stlc.v

(** * Stlc: Functorial semantics of STLC (McBride) *)

(** Coq programmers usually avoid using dependent types, because
    dependent pattern matching is difficult to use. However, with a
    principled use of the induction principle and using refine/eapply,
    dependently typed programming in Coq can be made enjoyable. *)

Module Stlc.

Inductive Ty : Type :=
  tunit : Ty
| tfunc : Ty -> Ty -> Ty.

Notation "τ ⇒ σ" := (tfunc τ σ) (at level 40).

Reserved Notation "⟦ τ ⟧".

Fixpoint interpTy (τ : Ty) : Type :=
  match τ with
  | tunit => unit
  | (τ1 ⇒ τ2) => ⟦ τ1 ⟧ -> ⟦ τ2 ⟧
  end where "⟦ τ ⟧" := (interpTy τ).

Inductive Ctx {A : Type} : Type :=
  empty : Ctx
| snoc  : Ctx -> A -> Ctx.

Notation "'∙'" := empty.
Notation "Γ , τ" := (snoc Γ τ) (at level 40).

Fixpoint interpCtx {A} (interpA : A -> Type) (Γ : @Ctx A) : Type :=
  match Γ with
  | ∙ => unit
  | Δ , σ => interpCtx interpA Δ * interpA σ
  end.

Notation "⟦ Γ ⟧ᶜ" := (interpCtx interpTy Γ).

Reserved Notation "τ ∈ Γ" (at level 40).

Inductive In (τ : Ty) : Ctx -> Type :=
  here  : forall {Γ}, τ ∈ (Γ , τ)
| there : forall {Γ σ}, τ ∈ Γ -> τ ∈ (Γ , σ)
where "τ ∈ Γ" := (In τ Γ).

Definition interpIn {Γ} {τ} (ix : τ ∈ Γ) : ⟦ Γ ⟧ᶜ -> ⟦ τ ⟧.
  Check In_rect.
  unshelve eapply (In_rect τ (fun Γ ix => ⟦ Γ ⟧ᶜ -> ⟦ τ ⟧) _ _ _ _); simpl in *.
  - clear. intros Γ (_,e). exact e.
  - clear. intros Γ σ _ θ (Γ',σ'). exact (θ Γ').
  - exact ix.
  Show Proof.
Defined.

Notation "⟦ ix ⟧ⁱ" := (interpIn ix).

Reserved Notation "Γ ⊢ τ" (at level 40).

Inductive Tm (Γ : @Ctx Ty) : Ty -> Type :=
  var : forall {τ}, τ ∈ Γ -> Γ ⊢ τ
| lam : forall {τ σ}, (Γ , σ) ⊢ τ -> Γ ⊢ (σ ⇒ τ)
| app : forall {τ σ}, Γ ⊢ (σ ⇒ τ) -> Γ ⊢ σ -> Γ ⊢ τ
where "Γ ⊢ τ" := (Tm Γ τ).

Definition interp {Γ : @Ctx Ty} {τ : Ty} (e : Γ ⊢ τ) : ⟦ Γ ⟧ᶜ -> ⟦ τ ⟧.
Proof.
  Check Tm_rect.
  unshelve eapply (Tm_rect (fun Γ τ e => ⟦ Γ ⟧ᶜ -> ⟦ τ ⟧) _ _ _ _ _); simpl in *.
  - clear. intros Γ τ ix Γ'.
    exact (⟦ ix ⟧ⁱ Γ').
  - clear. intros Γ τ σ e_lam e_lam' Γ' σ'.
    exact (e_lam' (pair Γ' σ')).
  - clear. intros Γ τ σ e_rator e_rator' e_rand e_rand' Γ'.
    exact (e_rator' Γ' (e_rand' Γ')).
  - exact e.
  Show Proof.
Defined.

Example ident : forall {τ}, ∙ ⊢ (τ ⇒ τ) :=
  fun τ => (lam ∙ (var (∙ , τ) (here τ))).
Example ident_interp : unit -> unit :=
  interp (@ident tunit) tt.

Compute ident_interp tt.

End Stlc.