TypedLambdaDependentType.v

Require Import Arith List.


Set Implicit Arguments.
Set Asymmetric Patterns.


Section hlist.

    Variable A : Type.
    Variable B : A -> Type.

    Inductive hlist : list A -> Type :=
    | HNil : hlist nil 
    | HCons x ls : B x -> hlist ls -> hlist (x :: ls).


    Variable elm : A.
    
    Inductive member : list A -> Type := 
    | HFirst ls : member (elm :: ls)
    | HNext x ls : member ls -> member (x :: ls).



    Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
        match mls with 
        | HNil => fun mem =>
            match mem in member ls' return (match ls' with 
                                            | nil => B elm 
                                            | _ :: _ => unit
                                            end) with
            | HFirst _ => tt 
            | HNext _ _ _ => tt 
            end 
        | HCons _ _ x mls' => fun mem =>
            match mem in member ls' return (match ls' with 
                                             | nil => Empty_set 
                                             | x' :: ls'' => 
                                                B x' -> (member ls'' -> B elm) -> B elm
                                             end) with 
            | HFirst _ => fun x _ => x 
            | HNext _ _ mem' => fun _ get_mls' => get_mls' mem' 
            end x (hget mls') 
        end.

End hlist.

Arguments HNil {A B}.
Arguments HCons {A B x ls} _ _ .

Arguments HFirst {A elm ls}.
Arguments HNext {A elm x ls} _.


Definition someTypes : list Set := nat :: bool :: nil.


Example someValues : hlist (fun T : Set => T) someTypes :=
    HCons 5 (HCons true HNil).

Print hlist.

Eval compute in hget someValues (HNext HFirst).


Inductive type : Set :=
    | Unit : type 
    | Arrow : type -> type -> type.


Inductive exp : list type -> type -> Type :=
    | Const ts : exp ts Unit 
    | Var ts t : member t ts -> exp ts t
    | App ts dom ran : exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
    | Abs ts dom ran : exp (dom :: ts) ran -> exp ts (Arrow dom ran).

Arguments Const {ts}.

Fixpoint typeDenote (t : type) : Set :=
    match t with 
    | Unit => unit 
    | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 
    end.


Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
    match e with 
    | Const _ => fun _ => tt 
    | Var _ _ mem => fun s => hget s mem 
    | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
    | Abs _ _ _ e' => fun s x => expDenote e' (HCons x s)
    end.