types - 包括模块、强制

Question

我正在写一篇关于如何使用 OCaml 的模块系统而不是 Java 的 OO 系统(一个有趣的视角)的博客文章。我遇到了一些我不理解的关于强制的事情。下面是一个基本模块和两个包含它的模块:

module M = struct
  type t = int
  let make () = 1
end   
module A = struct
  include M
end
module B = struct
  include M
end

现在 A.t 和 B.t 是同一类型!为什么？如果你这样做很明显

let a = A.make();;
let b = B.make();;
[a;b] --> A.t list (* ? *)

我知道可以使用私有(private)类型缩写来防止这种情况，然后如果您想将它们放在同一个列表中，请使用强制。我的问题是:为什么这还没有完成？编译器怎么知道 A.t和 B.t来自相同的基本类型？

问候
偶来

Answer 1

在很多情况下，您希望这两个模块兼容。一个更简单的用例如下:

module Hashtbl = struct ... (* definition in the stdlib *) end

module ExtHashtbl = struct ... (* my own layer on top of it *) end

我要 ExtHashtbl.t与 Hashtbl.t 兼容, 这样我就可以使用 ExtHashtbl 的功能在代码中间使用 Hashtbl.t , 或对仅知道 Hashtbl 的其他人建立的值进行操作图书馆，而不是我自己的东西。

在 ML 模块的理论中，有一种称为“强化”的操作，它用尽可能多的方程来丰富模块定义，并将它们暴露在签名中。这个想法是，如果你想要更多的抽象(更少的方程)，你总是可以使用类型签名来限制它，所以严格来说拥有方程更一般。

在仿函数的情况下情况有点不同。考虑一下，您没有将 A 和 B 定义为简单的模块，而是将它们作为空签名上的仿函数:

module A (U : sig end) = struct include M end
module B (U : sig end) = struct include M end

在 ML 模块系统中有两种不同的仿函数概念，一种称为“生成”(仿函数的每次调用都会生成与其他调用不兼容的"new"类型)，另一种称为“应用”(所有对等参数的仿函数的调用具有兼容的类型)。如果您使用命名的模块参数(更通常是路径)实例化 OCaml 系统，则 OCaml 系统将以应用方式运行，如果您使用未命名的模块参数实例化它，则以生成方式运行。

在 Xavier Leroy 的 2000 年论文 A Modular Module System (PDF) 中，您可以了解比您想知道的更多的 OCaml 模块系统。 (来自网页 A few papers on Caml)。您还将在下面找到我上面描述的所有情况的代码示例。

最近关于 ML 模块系统的工作，尤其是 Anreas Rossberg、Derek Dreyer 和 Claudio Russo，倾向于对“应用”和“生成”仿函数之间的经典区别提出不同的观点。他们声称它们应该对应于“纯”和“不纯”仿函数:应用程序执行副作用的仿函数应该始终是生成的，而只带纯项的仿函数应该默认适用(带有一些密封结构以强制不兼容，特此提供抽象)。

module type S = sig
  type t
  val x : t
end;;

module M : S = struct
  type t = int
  let x = 1
end;;

(* definitions below are compatible, the test type-checks *)
module A1 = M;;
module B1 = M;;
let _ = (A1.x = B1.x);;

(* definitions below are each independently sealed with an abstract
   signature, so incompatible; the test doesn't type-check *)
module A2 : S = M;;
module B2 : S = M;;
let _ = (A2.x = B2.x);;
(*This expression has type B2.t but an expression was expected of type A2.t*)


(* note: if you don't seal Make with the S module type, all functor
   applications will be transparently equal to M, and all examples below
   then have compatible types. *)
module Make (U : sig end) : S = M;;

(* same functor applied to same argument:
   compatible (applicative behavior) *)
module U = struct end;;
module A3 = Make(U);;
module B3 = Make(U);;
let _ = (A3.x = B3.x);;

(* same functor applied to different argument:
   incompatible (applicative behavior) *)
module V = struct end;;
module A4 = Make(U);;
module B4 = Make(V);;
let _ = (A4.x = B4.x);;
(* This expression has type B4.t = Make(V).t
   but an expression was expected of type A4.t = Make(U).t *)

(* same functor applied to non-path (~unnamed) arguments:
   incompatible (generative behavior) *)
module A5 = Make(struct end);;
module B5 = Make(struct end);;
let _ = (A5.x = B5.x);;
(* This expression has type B5.t but an expression was expected
   of type A5.t *)