ocaml - 我可以仅为某些仿函数参数定义 OCaml 函数吗？

Question

我想做这样的事情:

module Make (M: MInt) (N: MInt) : T = struct
    (* always defined *)
    let foo = 42

    (* only defined when M == N or M.x == N.x, something like that *)
    let bar a b = a * b
end

这可能吗？

显然我可以在运行时检查，但我很好奇如何在编译时进行检查。谢谢!

Answer 1

要对此类事物进行编码，需要一种具有 dependent typing 的语言。依赖类型是类型系统的一个强大功能，但不幸的是它使语言变得复杂并使类型推断变得不可判定。通常，这比普通程序员愿意支付的费用要高得多。如果您确实想要一种允许您编写此类规范的语言，那么您需要尝试 Coq 。

OCaml 仍然通过 Generalized Algebraic Data types 对某种程度受限的依赖类型提供支持。 。因此，理论上，在 OCaml 中，您可以编码一个函数，该类型确保两个参数是相等的整数。为此，您需要使用皮亚诺数字而不是内置整数，或者用幻像类型注释内置整数，描述其大小。但这一切都是相当不切实际的。在 Coq 中编写此代码，然后将定义提取为 OCaml 程序要容易得多。

总而言之，在仿函数级别上做你想做的事情是不可能的。使用 OCaml 类型系统来表达这样的事情是可能的。但最好使用 Coq 来实现这一点，并在 OCaml 中让事情变得简单。