在 Coq 中将高阶函子表示为容器

Question

按照这种方法，我尝试基于 Haskell 中的实现，在 Coq 中使用效果处理程序对函数式程序进行建模。论文中提出了两种方法：

• Effect 语法被表示为一个函子并与自由 monad 结合。

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

由于终止检查不喜欢非严格肯定的定义，因此无法直接定义此数据类型。但是，容器可用于表示严格正函子，如本文所述。这种方法有效，但由于我需要对需要显式作用域语法的作用域效果进行建模，因此可能会出现不匹配的开始/结束标记。对于程序的推理，这并不理想。

• 第二种方法使用高阶函子，即以下数据类型。

    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.

代码可以在这里找到。Lambda 演算示例有效，我可以证明容器表示与数据类型同构。我试图对异常处理程序数据类型的简化版本进行相同的操作，但它不适合容器表示。

定义智能构造函数也不起作用。在 Haskell 中，构造函数通过应用Catch'到可能发生异常的程序和开始时为空的延续来工作。

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

我在 Coq 实现中看到的主要问题是形状需要在函子上参数化，这会导致各种问题。

Answer 1

这个答案比我之前的答案更直观地了解如何从函子派生容器。我采取了完全不同的角度，所以我正在做出一个新的答案，而不是修改旧的答案。

简单的递归类型

让我们首先考虑一个简单的递归类型，以了解非参数容器，并与参数化泛化进行比较。Lambda 演算，不关心范围，由以下函子给出：

Inductive LC_F (t : Type) : Type :=
| App : t -> t -> LC_F t
| Lam : t -> LC_F t
.

从这个类型中我们可以了解到两个信息：

• 形状告诉我们有关构造函数 ( , ) 的信息，以及可能与语法的递归性质无关的辅助数据（此处没有）。有两个构造函数，因此形状有两个值。（也可以，但是将形状声明为独立的归纳类型很便宜，并且命名构造函数也可以兼作文档。）AppLamShape := App_S | Lam_Sbool

• 对于每个形状（即构造函数），位置告诉我们该构造函数中语法的递归出现。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. *)

最后，对于每个位置，您需要决定上下文如何变化，即您现在是否正在计算 anX或 an 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.

使用代码中的约定，您可以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