遵循this方法，我正在尝试使用Coq中的效果处理程序来模拟功能程序，基于Haskell中的实现。本文介绍了两种方法：
data Prog sig a = Return a | Op (sig (Prog sig a))
由于终止检查不喜欢非严格正定义，因此无法直接定义此数据类型。但是，容器可用于表示严格正面的仿函数，如this paper中所述。这种方法有效，但由于我需要对需要显式作用域语法的作用域效果建模，因此可能存在不匹配的开始/结束标记。对于程序的推理，这并不理想。
data Prog sig a = Return a | Op (sig (Prog sig) a)
现在sig有类型（* - > *） - > * - > *。由于与之前相同的原因，无法在Coq中定义数据类型。我正在寻找模拟这种数据类型的方法，这样我就可以在没有显式范围标记的情况下实现范围效果。
我为高阶函子定义容器的尝试并没有多少成果，我找不到关于这个主题的任何内容。我很感谢指导正确的方向和有用的评论。
编辑：我想要表示的论文中的作用域语法的一个示例是以下异常数据类型。
data HExc e m a = Throw′ e | forall x. Catch′ (m x) (e -> m x) (x -> m a)
Edit2：我已将建议的想法与我的方法合并。
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.
代码可以找到here。 Lambda Calculus示例有效，我可以证明容器表示与数据类型是同构的。我试图对异常处理程序数据类型的简化版本进行相同的操作，但它不适合容器表示。
定义智能构造函数也不起作用。在Haskell中，构造函数的工作原理是将Catch'应用于可能发生异常的程序和一个在开头为空的延续。
catch :: (HExc <: sig) => Prog sig a -> Prog sig a
catch p = inject (Catch' p return)
我在Coq实现中看到的主要问题是形状需要在仿函数上进行参数化，这会导致各种各样的问题。
这个答案给出了更多关于如何从仿函数派生容器的直觉。我采取了不同的角度，所以我正在做一个新的答案而不是修改旧答案。
让我们首先考虑一个简单的递归类型来理解非参数容器，并与参数化泛化进行比较。 Lambda演算不关心范围，由以下仿函数给出：
Inductive LC_F (t : Type) : Type :=
| App : t -> t -> LC_F t
| Lam : t -> LC_F t
.
我们可以从这种类型中学到两条信息：
App，Lam），以及可能还有与语法的递归性质无关的辅助数据（这里没有）。有两个构造函数，因此形状有两个值。 Shape := App_S | Lam_S（bool也可以，但是将形状声明为独立的归纳类型很便宜，并且命名构造函数也可以作为文档使用。）App包含两个子项，因此我们可以将它们的两个位置定义为布尔值; Lam包含一个子项，因此它的位置是一个单位。人们也可以使Pos (s : Shape)成为一个索引归纳类型，但这是一个痛苦的编程（只是尝试）。(* Lambda calculus *)
Inductive ShapeLC :=
| App_S (* The shape App _ _ *)
| Lam_S (* The shape Lam _ *)
.
Definition PosLC s :=
match s with
| App_S => bool
| Lam_S => unit
end.
现在，适当范围的lambda演算：
Inductive LC_F (f : Type -> Type) (a : Type) : Type :=
| App : f a -> f a -> LC_F a
| Lam : f (unit + a) -> LC_F a
.
在这种情况下，我们仍然可以重用之前的Shape和Pos数据。但是这个仿函数编码了另外一条信息：每个位置如何改变类型参数a。我将此参数称为上下文（Ctx）。
Definition CtxLC (s : ShapeLC) : PosLC s -> Type -> Type :=
match s with
| App_S => fun _ a => a (* subterms of App reuse the same context *)
| Lam_S => fun _ a => unit + a (* Lam introduces one variable in the context of its subterm *)
end.
这个容器(ShapeLC, PosLC, CtxLC)通过同构性与仿函数LC_F有关：在sigma { s : ShapeLC & forall p : PosLC s, f (CtxLC s p a) }和LC_F a之间。特别要注意函数y : forall p, f (CtxLC s p)如何告诉你究竟如何填充形状s = App_S或s = Lam_S来构造一个值App (y true) (y false) : LC_F a或Lam (y tt) : LC_F a。
我之前的代表编码Ctx在一些额外的Pos类型索引。这些陈述是等价的，但这里的陈述看起来更整洁。
我们只考虑Catch构造函数。它有四个字段：类型X，主要计算（返回X），异常处理程序（也恢复X）和延续（消耗X）。
Inductive Exc_F (E : Type) (F : Type -> Type) (A : Type) :=
| ccatch : forall X, F X -> (E -> F X) -> (X -> F A) -> Exc_F E F A.
形状是单个构造函数，但您必须包含X。从本质上讲，查看所有字段（可能展开嵌套的归纳类型），并保留所有未提及F的数据，这就是你的形状。
Inductive ShapeExc :=
| ccatch_S (X : Type) (* The shape ccatch X _ (fun e => _) (fun x => _) *)
.
(* equivalently, Definition ShapeExc := Type. *)
位置类型列出了从相应形状的F中获取Exc_F的所有方法。特别是，一个位置包含应用函数的参数，并且可能包含任何数据以解析任何其他类型的分支。特别是，您需要知道异常类型以存储处理程序的异常。
Inductive PosExc (E : Type) (s : ShapeExc) : Type :=
| main_pos (* F X *)
| handle_pos (e : E) (* E -> F X *)
| continue_pos (x : getX s) (* X -> F A *)
.
(* The function getX takes the type X contained in a ShapeExc value, by pattern-matching: getX (ccatch_S X) := X. *)
最后，对于每个位置，您需要决定上下文如何变化，即您现在是否正在计算X或A：
Definition Ctx (E : Type) (s : ShapeExc) (p : PosExc E s) : Type -> Type :=
match p with
| main_pos | handle_pos _ => fun _ => getX s
| continue_pos _ => fun A => A
end.
使用your code中的约定，您可以编码Catch构造函数，如下所示：
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)).
(* I had problems with type inference for some reason, hence @ext is explicitly applied *)
充分的要点https://gist.github.com/Lysxia/6e7fb880c14207eda5fc6a5c06ef3522
“一阶”自由monad编码的主要技巧是将一个函子F : Type -> Type编码为一个容器，它本质上是一个依赖对{ Shape : Type ; Pos : Shape -> Type }，因此，对于所有a，类型F a与sigma类型{ s : Shape & Pos s -> a }同构。
进一步考虑这个想法，我们可以将高阶函子F : (Type -> Type) -> (Type -> Type)编码为容器{ Shape : Type & Pos : Shape -> Type -> (Type -> Type) }，这样，对于所有f和a，F f a与{ s : Shape & forall x : Type, Pos s a x -> f x }同构。
我不太明白Type中的额外Pos参数在那里做了什么，但It Works™，至少可以在结果类型中构造一些lambda演算术语。
例如，lambda演算语法仿函数：
Inductive LC_F (f : Type -> Type) (a : Type) : Type :=
| App : f a -> f a -> LC_F a
| Lam : f (unit + a) -> LC_F a
.
由容器(Shape, Pos)表示定义为：
(* 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;
其中App_F和Lam_F由下式给出：
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)
.
那么自由式monad Prog（由(Shape, Pos)隐式参数化）由下式给出：
Inductive Prog (a : Type) : Type :=
| Ret : a -> Prog a
| Op (s : Shape) : (forall b, Pos s a b -> Prog b) -> Prog a
.
定义了一些样板文件后，您可以编写以下示例：
(* \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)).
全部要点：https://gist.github.com/Lysxia/5485709c4594b836113736626070f488