OCaml 中的多态函子（与 Include 命令相关）

Question

编辑：我用模块类型 A 和 B 替换了抽象示例，使用组和环的更具体示例。

我在一个使用众所周知的代数结构的例子中展示了我的函子问题。定义组的签名：

module type Group = 
sig
    type t
    val neutral: t
    val add: t -> t -> t
    val opp: t -> t
end

并为包含许多有用操作的组定义一个签名，例如这里的共轭：

module type Extended_Group =
sig
    include Group
    val conjugate: t -> t -> t
end

共轭的实现仅取决于加法和相反，所以我不想为我定义的所有组显式编写它，所以我编写了以下函子：

module F (G: Group) =
struct
    include G
    let conjugate x y = add (add x y) (opp x)
end

现在，假设您正在使用“扩展”组概念的其他结构，例如整数环：

module Z = 
struct
    (* Group *)
    type t = int
    let neutral = 0
    let add x y = x+y
    let opp x = -x
    (* Ring *)
    let m_neutral = 1
    let mult x y = x*y
end

由于环是群的粒子情况，我们可以对它应用函子 F：

module Extended_Z = F(Z)

不幸的是，为了将 F 应用到 Z，Ocaml 首先将 Z 的类型限制为 Group，然后应用 F。一切都与我这样做的完全一样：

module (Group_Z: Group) = Z
module Extended_Z = F(Group_Z)

因此，尽管 Z.mult 有意义，但 Extended_Z.mult 对编译器来说是未知的。我不想失去 Extended_Z 仍然是戒指的事实！当然，写一个函子 F_Ring 的解决方案与 F 一样，但以 Ring 作为输入并不是一个令人满意的解决方案：我不想写 F_Fields、F_VectorSpace 等等。

这是我想要的：

1. 一种扩展模块签名的方法，以公开更多值。也可以用另一种方式来限制模块的签名（使用我用于 Group_Z 的语法），但我找不到放大签名的方法。这将是这样的：

   module (Ring_Extended_Z: Ring) = Extended_Z
   

2. 或者，一种定义多态函子的方法，即定义一个函子 F，该函子 F 接受签名为“至少 Group”的模块并输出签名为“至少 Extended_Group”的模块。当然，这只有在存在 include 时才有意义，这就是为什么我坚信 OCaml 中不存在这样的特性。

在网上搜索了几天的答案后，我认为实现这一点的正确方法实际上是以下一种：（灵感来自Real World OCaml的第9章）

module F (G: Group) =
struct
    let conjugate x y = ...
end

（与之前相同但没有包含）然后在同一点执行所有包含：

module Extended_Z =
struct
    include Z
    include F(Z)
end

有人可以确认这是实现我想要的好方法，并且我的第一种方法不符合 OCaml 的精神吗？更具体地说，有人可以确认选项 1. 和 2. 在 OCaml 中确实是不可能的吗？

编辑：关于动态类型

在我看来这仍然是静态类型，因为如果我写

module Extended_Z = F(Z: Ring)

OCaml 仍然可以将其静态键入为具有签名 Ring 和额外值“共轭”的模块。它需要模块级别的多态性，我理解这是不存在的，但我认为它可以在不使类型系统动态化的情况下存在。

Answer 1

函子是结构的抽象，从结构生成结构。事实上，它们是范畴态射，即箭头。这是一个非常强大的机制，但仍然有一个限制：模块的所有参数必须具有固定（常量）的模块类型，即没有模块类型变量。这意味着，不可能获得您想要的东西，有时您需要编写比您预期更多的代码。

您的示例实际上捕获了最小（最小）结构和最大（最大）结构的概念。前者提取了代数结构的最低要求，而后者描述了可以从中导出的最大元素集（其中元素表示为结构域）。将其与 Haskell 的类型类进行比较，在其中提供最小的实现，其余部分由类型类定义派生。同样，可以用函子来表达，但与 Haskell 不同的是，没有机器可以自动应用这个函子，你需要手动实例化所有函子。这符合 OCaml 的意识形态——显式优于隐式。（尽管，即将推出的模块化隐式将通过提供与 Haskell 类型类类似的推理机制来偏离这种意识形态）。

话已经够多了，让我们来编写一些代码。正如我所说，你的例子为最小和最大结构提供了一个很好的例子。我们将从定义相应代数结构的最低要求开始，尝试严格遵循定义：

module Min = struct
  module type Set = sig
    type t
    val compare : t -> t -> int
  end

  module type Monoid = sig
    include Set
    val zero  : t
    val (+) : t -> t -> t
  end

  module type Group = sig
    include Monoid
    val (~-) : t -> t
  end

  module type Ring = sig
    include Group
    val one : t
    val ( * ) : t -> t -> t
    val (~/) : t -> t
  end
  ...
end

我们将所有模块类型定义放入 module 中Min，这表示它们是最小的。这些只是模块类型，即签名。

现在，我们可以定义最大签名。这里的一个问题是通常很难停下来，即找到最大的不动点。但这并不是一个大问题，因为您可以继续编写采用较小结构并返回较大结构的函子，直到您对结果感到满意为止。

例如，我们可以从类型 t 和函数中推断出很多东西compare：

module Max = struct
  module type Set = sig
    include Min.Set
    val (=) : t -> t -> t
    val (<) : t -> t -> t
    val (>) : t -> t -> t
    module Set : Set.S  (* this is Set from stdlib, not ours *)
    module Map : Map.S
    (* and much more *)
  end

  module Ring = sig
    include Min.Ring
    ...
  end
  ...
end

现在，当我们有了一个很好的结构理论后，我们就可以开始实施了。Min.T -> Max.T我们可以为所有签名提供通用态射 T，例如，

module Set(S : Min.Set) : Max.Set with type t = S.t = struct
  include S
  let (<) x y = compare x y = -1
  ...
  module Set = Set.Make(S)
  module Map = Map.Make(S)
  ...
end

使用这些通用仿函数作为基本工具，以及我们的最小定义，我们可以为我们定义的真实类型构建一个结构。此外，由于通用函子通常无法为某些操作提供最佳实现，因此我们可以提供自己的函子，这将利用我们对实现的了解。例如：

module Z = struct
  module T = struct
    type t = float
    let compare = compare
    let one = 1.
    let zero = 0.
    let (+) = (+.)
    let (~-) = (~-.)
    let (~/) x = (1. /. x)
  end
  include Set(T)
  include Ring(T)
  (* override minus and division as we can implement them more efficiently *)
  let (-) = (~.)
  let (/) = (/.)
end

我们可以Z非常轻松地描述具体模块的模块类型，只需包含相应的最大签名并添加我们的特定内容即可：

module type Z = sig
  include Ring
  val read : in_channel -> t
  val write : out_channel -> t -> unit
end

关于模块级多态性

Andreas Rossberg 在评论中指出，OCaml 模块子语言实际上至少在语法上允许多态性。这是系统 F 风格的多态性，必须通过L术语显式引入，术语绑定类型而不是值。由于模块可以携带类型，因此我们可以L使用具有以下模块类型的模块来表达术语：

module type L = sig module type T end

现在，我们可以定义经典的多态函数id、fst和snd：

module Id(L:L)(X:L.T) = X
module Fst(L1:L)(L2:L)(M1 : L1.T)(M2 : L2.T) = M1
module Snd(L1:L)(L2:L)(M1 : L1.T)(M2 : L2.T) = M2

然而，看起来我们对函子定义右侧参数的作用非常有限。例如，我们不能组合两个模块：

module Sum(L1:L)(L2:L)(M1 : L1.T)(M2 : L2.T) = struct
  include M1 
  ^^^^^^^^^^
  Error: This module is not a structure; it has type L1.T
  include M2
end

我们也无法打开模块，因为我们遇到了同样的错误。问题在于includeandopen语句正在将模块类型变量评估为其值，期望获得签名。由于打字环境还没有绑定，L1.T我们得到了一种误导性的错误消息。鉴于此限制，我们只能使用标识符级别的参数。例如，我们仍然可以将Sum模块定义为：

module Sum(L1:L)(L2:L)(M1 : L1.T)(M2 : L2.T) = struct
  module X = M1
  module Y = M2
end

但它是否有任何实际用途是非常值得怀疑的。另一个例子是定义App函子，它将把函子应用于参数（可用性也可疑）：

module App(L1:L)(L2:L)
 (F : functor (X : L1.T) -> L2.T)(X:L1.T) = struct
  module R = F(X)
end