包括模块,强制

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

现在At和Bt是同一类型!为什么？如果你这样做,那就显而易见了

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

我知道可以使用私有类型缩写来防止这种情况,然后如果要将它们放在同一个列表中则使用强制.我的问题是:为什么不这样做？编译器如何知道它A.t并且B.t来自相同的基类型？

关心
Olle

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模块系统函子的两个不同的概念,被称为一"生成"(各算符的调用产生"新鲜的"类型,可与其他调用不兼容),和那些被称为"应用性"(全部在同等参数的仿函数的调用具有兼容的类型).OCaml的系统行为中,如果你有一个名为(更通常是一个模块参数初始化它的应用性的方式路径),并在生成方式,如果你用一个module参数未命名实例化.

您可以在Xavier Leroy的2000纸张模块化模块系统(PDF)中了解有关OCaml模块系统的更多知识(来自网页关于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 *)