FreeIndexedMonad.v

Set Implicit Arguments.
Set Contextual Implicit.

Notation TyCon := (Type -> Type).

Inductive Prog {T : Type} (sig : T -> Type -> TyCon) (a : Type) : Type :=
| Ret : a -> Prog sig a
| Op (t : T) : (forall b, sig t a b -> Prog sig b) -> Prog sig a
.

Inductive App_F (a : Type) : TyCon :=
| App_ (b : bool) : App_F a a
.

Inductive Lam_F (a : Type) : TyCon :=
| Lam_ : Lam_F a (unit + a)
.

Definition LC_sig (b : bool) : Type -> TyCon :=
  match b with
  | true => App_F
  | false => Lam_F
  end.

Definition LC : TyCon := Prog LC_sig.

Definition App {A} (x y : LC A) : LC A :=
  Op true (fun _ f =>
    match f in App_F _ B return LC B with
    | App_ true => x
    | App_ false => y
    end).

Definition Lam {A} (x : LC (unit + A)) : LC A :=
  Op false (fun _ f =>
    match f in Lam_F _ B return LC B with
    | Lam_ => x
    end).

(* \x -> x*)
Definition id_lc {a} : LC a := Lam (Ret (inl tt)).

(* \f x -> f x x *)
Definition omega {a} : LC a :=
  Lam (* f *) (Lam (* x *)
    (let f := Ret (inr (inl tt)) in
     let x := Ret (inl tt) in
     App (App f x) x)).