FreeContainers.v

Class Container : Type :=
  { Shape : Type;
    Pos : Shape -> Type;
  }.

Inductive Ext (C : Container) (A : Type) :=
| ext : forall s, (forall p : Pos s, A) -> Ext C A.

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

Inductive HExt (C : HContainer) (F : Type -> Type) A :=
| Hext : forall s, (forall p : Pos s, F (@Shape (Ctx s p))) -> (forall p : Pos s, Ext (Ctx s p) A) -> HExt C F A.

(**)

Inductive Free (C : HContainer) A :=
| pure : A -> Free C A
| impure : HExt C (Free C) A -> Free C A.

Fail Inductive List A :=
| Nil  : List A
| Cons : Free C A -> Free C (List A) -> List A.

Inductive List {C} A :=
| Nil  : List A
| Cons {T : Type} : Free C A -> Free C T -> (T -> List A) -> List A.

(**)

Inductive FreeShape {C : HContainer} : Type :=
| pureS : FreeShape
| impureS : forall (s : Shape), (forall p : Pos s, FreeShape) -> FreeShape.
Arguments FreeShape : clear implicits.

Fixpoint FreePos {C : HContainer} (p : FreeShape C) : Type :=
  match p with
  | pureS => unit
  | impureS s fs => { p0 : Pos s & FreePos (fs p0) }
  end.

Definition FreeC (C : HContainer) : Container := {|
  Shape := FreeShape C;
  Pos := FreePos;
|}.

(* Free C A = Ext (FreeC C) A *)

Variable C : HContainer.

Inductive ListShape : Type :=
| NilS : ListShape
| ConsS
    (s_head : FreeShape C)
    (s_tail : FreeShape C)
    (p_tail : forall p : FreePos s_tail, ListShape)
  (* the pair (s_tail, p_tail) is just a [Ext] *) : ListShape.

Fixpoint ListPos (s : ListShape) : Type :=
  match s with
  | NilS => Empty_set
  | ConsS s_head s_tail p_tail =>
    FreePos s_head + { p : FreePos s_tail & ListPos (p_tail p) }
  end.

Definition ListC : Container := {|
  Shape := ListShape;
  Pos := ListPos;
|}.

(* List A = Ext ListC A *)