Representing Higher-Order Functors as Containers in Coq

Question

Following this approach, I'm trying to model functional programs using effect handlers in Coq, based on an implementation in Haskell. There are two approaches presented in the paper:

• Effect syntax is represented as a functor and combined with the free monad.

    data Prog sig a = Return a | Op (sig (Prog sig a))

Due to the termination check not liking non-strictly positive definitions, this data type can't be defined directly. However, containers can be used to represent strictly-positive functors, as described in this paper. This approach works but since I need to model a scoped effect that requires explicit scoping syntax, mismatched begin/end tags are possible. For reasoning about programs, this is not ideal.

• The second approach uses higher-order functors, i.e. the following data type.

    data Prog sig a = Return a | Op (sig (Prog sig) a)

Now sig has the type (* -> *) -> * -> *. The data type can't be defined in Coq for the same reasons as before. I'm looking for ways to model this data type, so that I can implement scoped effects without explicit scoping tags.

My attempts of defining a container for higher-order functors have not been fruitful and I can't find anything about this topic. I'm thankful for pointers in the right direction and helpful comments.

Edit: One example of scoped syntax from the paper that I would like to represent is the following data type for exceptions.

data HExc e m a = Throw′ e | forall x. Catch′ (m x) (e -> m x) (x -> m a)

Edit2: I have merged the suggested idea with my approach.

Inductive Ext Shape (Pos : Shape -> Type -> Type -> Type) (F : Type -> Type) A :=
  ext : forall s, (forall X, Pos s A X -> F X) -> Ext Shape Pos F A.

Class HContainer (H : (Type -> Type) -> Type -> Type):=
  {
    Shape   : Type;
    Pos     : Shape -> Type -> Type -> Type;
    to      : forall M A, Ext Shape Pos M A -> H M A;
    from    : forall M A, H M A -> Ext Shape Pos 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 Shape Pos M A), @from M A (@to M A e) = e
  }.

Section Free.
  Variable H : (Type -> Type) -> Type -> Type.

  Inductive Free (HC__F : HContainer H) A :=
  | pure : A -> Free HC__F A
  | impure : Ext Shape Pos (Free HC__F) A -> Free HC__F A.
End Free.

The code can be found here. The Lambda Calculus example works and I can prove that the container representation is isomorphic to the data type. I have tried to to the same for a simplified version of the exception handler data type but it does not fit the container representation.

Defining a smart constructor does not work, either. In Haskell, the constructor works by applying Catch' to a program where an exception may occur and a continuation, which is empty in the beginning.

catch :: (HExc <: sig) => Prog sig a -> Prog sig a
catch p = inject (Catch' p return)

The main issue I see in the Coq implementation is that the shape needs to be parameterized over a functor, which leads to all sorts of problems.

Answer 1

The main trick in the "first-order" free monad encoding is to encode a functor F : Type -> Type as a container, which is essentially a dependent pair { Shape : Type ; Pos : Shape -> Type }, so that, for all a, the type F a is isomorphic to the sigma type { s : Shape & Pos s -> a }.

Taking this idea further, we can encode a higher-order functor F : (Type -> Type) -> (Type -> Type) as a container { Shape : Type & Pos : Shape -> Type -> (Type -> Type) }, so that, for all f and a, F f a is isomorphic to { s : Shape & forall x : Type, Pos s a x -> f x }.

I don't quite understand what the extra Type parameter in Pos is doing there, but It Works™, at least to the point that you can construct some lambda calculus terms in the resulting type.

For example, the lambda calculus syntax functor:

Inductive LC_F (f : Type -> Type) (a : Type) : Type :=
| App : f a -> f a -> LC_F a
| Lam : f (unit + a) -> LC_F a
.

is represented by the container (Shape, Pos) defined as:

(* LC container *)

Shape : Type := bool; (* Two values in bool = two constructors in LC_F *)
Pos (b : bool) : Type -> (Type -> Type) :=
         match b with
         | true => App_F
         | false => Lam_F
         end;

where App_F and Lam_F are given by:

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)
.

Then the free-like monad Prog (implicitly parameterized by (Shape, Pos)) is given by:

Inductive Prog (a : Type) : Type :=
| Ret : a -> Prog a
| Op (s : Shape) : (forall b, Pos s a b -> Prog b) -> Prog a
.

Having defined some boilerplate, you can write the following example:

(* \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)).

Full gist: https://gist.github.com/Lysxia/5485709c4594b836113736626070f488