FunctorContainers.v

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.

Class HContainer : Type :=
  {
    Shape : Type;
    Pos : Shape -> Type;
    Ctx : forall s : Shape, Pos s -> Type -> Type;
  }.

Inductive Ext (C : HContainer) (F : Type -> Type) A :=
  ext : forall s, (forall p : Pos s, F (Ctx s p A)) -> Ext C F A.

Arguments ext {C F A} s pf.

Set Implicit Arguments.
Set Contextual Implicit.

Class HContainerOf (H : (Type -> Type) -> Type -> Type):=
  {
    HCO :> HContainer;
    to      : forall M A, Ext HCO M A -> H M A;
    from    : forall M A, H M A -> Ext HCO M A;
    to_from : forall M A (fx : H M A), @to M A (@from M A fx) = fx;
    from_to : forall M A (e : Ext HCO M A), @from M A (@to M A e) = e
  }.

Arguments from {_} {_} {_} _.

Section Free.
  Inductive Free (C : HContainer) A :=
  | pure : A -> Free C A
  | impure : Ext C (Free C) A -> Free C A.
End Free.

Arguments pure {_} {_} _.

(* lambda calculus *)

Inductive LC_F (F : Type -> Type) (A : Type) : Type :=
| App : F A -> F A -> LC_F F A
| Lam : F (sum unit A) -> LC_F F A.

Inductive Shape__LC := App_S | Lam_S.

Definition Pos__LC (s : Shape__LC) : Type :=
  match s with
  | App_S => bool
  | Lam_S => unit
  end.

Definition Ctx__LC (s : Shape__LC) : Pos__LC s -> Type -> Type :=
  match s with
  | App_S => fun _ a => a
  | Lam_S => fun _ a => (unit + a)%type
  end.

Instance C__LC : HContainer :=
  { Shape := Shape__LC;
    Pos := Pos__LC;
    Ctx := Ctx__LC;
  }.

Definition Ext__LC F A := Ext C__LC F A.

Definition LC : Type -> Type := Free C__LC.

Definition App' {A} (x y : LC A) : LC A :=
  impure (ext App_S (fun (f : bool) =>
    match f with
    | true => x
    | false => y
    end)).

Definition Lam' {A} (x : LC (unit + A)) : LC A :=
  impure (ext Lam_S (fun (_ : unit) => x)).

(* \x -> x*)
Definition id_lc {A} : LC A := Lam' (pure (inl tt)).

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

(* exceptions *)

Inductive Exc (E : Type) F (A : Type) :=
| ccatch : forall X, F X -> (E -> F X) -> (X -> F A) -> Exc E F A.

Inductive Shape__Exc :=
| ccatch_S (X : Type).

Definition getX (s : Shape__Exc) : Type :=
  match s with
  | ccatch_S X => X
  end.

Inductive Pos__Exc (E : Type) (s : Shape__Exc) : Type :=
| main_pos
| handle_pos (e : E)
| continue_pos (x : getX s)
.

Definition Ctx__Exc (E : Type) (s : Shape__Exc) (p : Pos__Exc E s) : Type -> Type :=
  match p with
  | main_pos => fun _ => getX s
  | handle_pos _ => fun _ => getX s
  | continue_pos _ => fun A => A
  end.

Instance C__Exc (E : Type) : HContainer :=
  { Shape := Shape__Exc;
    Pos := Pos__Exc E;
    Ctx := @Ctx__Exc E;
  }.

Definition Ext__Exc E F A := Ext (C__Exc E) F A.

Definition Catch' {E X A}
           (m : Free (C__Exc E) X)
           (h : E -> Free (C__Exc E) X)
           (k : X -> Free (C__Exc E) A) : Free (C__Exc E) A :=
  impure (@ext (C__Exc E) (Free (C__Exc E)) A (ccatch_S X) (fun p =>
    match p with
    | main_pos => m
    | handle_pos e => h e
    | continue_pos x => k x
    end)).