在 Coq 中将高阶函子表示为容器
Representing Higher-Order Functors as Containers in Coq
按照 this 方法，我尝试基于 Haskell 中的实现，在 Coq 中使用效果处理程序对功能程序进行建模。论文中提出了两种方法：
- Effect 语法表示为仿函数并与自由 monad 结合。
data Prog sig a = Return a | Op (sig (Prog sig a))
由于终止检查不喜欢非严格正定义，不能直接定义该数据类型。但是，容器可用于表示严格正函子，如 this paper 中所述。这种方法有效，但由于我需要对需要显式作用域语法的作用域效果进行建模，因此 begin/end 标签不匹配是可能的。对于程序的推理，这并不理想。
- 第二种方法使用高阶仿函数，即以下数据类型。
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 微积分示例有效，我可以证明容器表示与数据类型同构。
我已尝试对异常处理程序数据类型的简化版本进行相同操作，但它不适合容器表示。
定义智能构造函数也不起作用。在 Haskell 中，构造函数通过将 Catch' 应用于可能发生异常的程序和开始时为空的延续来工作。
catch :: (HExc <: sig) => Prog sig a -> Prog sig a
catch p = inject (Catch' p return)
我在 Coq 实现中看到的主要问题是形状需要通过仿函数进行参数化，这会导致各种问题。
"first-order" 自由 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 }.
我不太明白 Pos 中额外的 Type 参数在那里做什么，但它有效™，至少你可以在结果类型。
例如，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
这个答案比我之前的答案更直观地说明了如何从仿函数派生容器。我采取了完全不同的角度，所以我正在做一个新的答案而不是修改旧的。
简单的递归类型
让我们先考虑一个简单的递归类型来理解非参数容器，并与参数化泛化进行比较。 Lambda 演算，不关心范围，由以下函子给出：
Inductive LC_F (t : Type) : Type :=
| App : t -> t -> LC_F t
| Lam : t -> LC_F t
.
我们可以从这个类型中了解到两条信息：
shape 告诉我们关于构造函数（App、Lam）以及与语法的递归性质（此处为none）。有两个构造函数，所以形状有两个值。 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.
我之前的表示在 Pos 的一些附加类型索引中编码 Ctx。表示是等价的，但这里看起来更整洁。
异常处理程序演算
我们将只考虑 Catch 构造函数。它有四个字段：类型 X、主要计算（returns 和 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. *)
位置类型列出了从相应形状的 Exc_F 中得到 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
按照 this 方法，我尝试基于 Haskell 中的实现，在 Coq 中使用效果处理程序对功能程序进行建模。论文中提出了两种方法：
- Effect 语法表示为仿函数并与自由 monad 结合。
data Prog sig a = Return a | Op (sig (Prog sig a))
由于终止检查不喜欢非严格正定义，不能直接定义该数据类型。但是，容器可用于表示严格正函子，如 this paper 中所述。这种方法有效，但由于我需要对需要显式作用域语法的作用域效果进行建模，因此 begin/end 标签不匹配是可能的。对于程序的推理，这并不理想。
- 第二种方法使用高阶仿函数，即以下数据类型。
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 微积分示例有效，我可以证明容器表示与数据类型同构。 我已尝试对异常处理程序数据类型的简化版本进行相同操作，但它不适合容器表示。
定义智能构造函数也不起作用。在 Haskell 中，构造函数通过将 Catch' 应用于可能发生异常的程序和开始时为空的延续来工作。
catch :: (HExc <: sig) => Prog sig a -> Prog sig a
catch p = inject (Catch' p return)
我在 Coq 实现中看到的主要问题是形状需要通过仿函数进行参数化，这会导致各种问题。
"first-order" 自由 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 }.
我不太明白 Pos 中额外的 Type 参数在那里做什么，但它有效™，至少你可以在结果类型。
例如，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
这个答案比我之前的答案更直观地说明了如何从仿函数派生容器。我采取了完全不同的角度，所以我正在做一个新的答案而不是修改旧的。
简单的递归类型
让我们先考虑一个简单的递归类型来理解非参数容器，并与参数化泛化进行比较。 Lambda 演算，不关心范围，由以下函子给出：
Inductive LC_F (t : Type) : Type :=
| App : t -> t -> LC_F t
| Lam : t -> LC_F t
.
我们可以从这个类型中了解到两条信息：
shape 告诉我们关于构造函数（
App、Lam）以及与语法的递归性质（此处为none）。有两个构造函数，所以形状有两个值。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.
我之前的表示在 Pos 的一些附加类型索引中编码 Ctx。表示是等价的，但这里看起来更整洁。
异常处理程序演算
我们将只考虑 Catch 构造函数。它有四个字段：类型 X、主要计算（returns 和 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. *)
位置类型列出了从相应形状的 Exc_F 中得到 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