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.