OCaml函子::反直觉行为

Question

我正在试验OCaml（3.12.1）的模块语言，定义模块的函子和签名等等，主要是遵循Chapter 2 of the OCaml manual的例子，我偶然发现了意外，在这种情况下，显然我的心智模型如何运算符和模块签名的工作是有缺陷的。我试图缩小我遇到的最短代码量的情况，所以不要问我想要完成什么，这是一个完全人为的例子来演示OCaml特性。

因此，我们有一个函数，它只是提供了一个标识函数'f'，并通过提供该函数输入参数类型的模块进行参数化。像我说的那样完全做作的例子。

module type SOMETYPE = sig type t end ;; 
module Identity = functor (Type: SOMETYPE) -> struct let f (x: Type.t) = x end ;; 

鉴于上述情况，我们进行到定义一个模块提供int类型：

module IntType = struct type t = int end ;; 

..然后我们使用仿函数来生成用于INT标识功能的模块：

module IdentityInt = Identity(IntType) ;;      

果然产生模块及其f函数像预期的那样：

#IdentityInt.f(3) + 10 ;; 
- : int = 13 

函子的心智模型是将模块作为输入和返回模块的函数，目前为止我们似乎正在为我们服务。仿函数Identity期望作为签名模块（模块类型）SOMETYPE的输入参数，实际上我们提供的模块（IntType）具有正确的签名，因此会生成一个有效的输出模块（IdentityInt），其函数的行为与预期相同。

现在是不直观的部分。如果我们想明确指出提供的模块IntType确实是SOMETYPE类型的模块，该怎么办？如：

module IntType : SOMETYPE = struct type t = int end ;; 

，然后生成仿函数的输出模块的方式和以前一样：

module IdentityInt = Identity(IntType) ;; 

...让我们尝试用新生成的模块的f功能：

IdentityInt.f 0 ;; 

因此，REPL抱怨：

"Error: This expression [the value 0] has type int but an expression was expected of type IntType.t." 

如何提供冗余但正确的类型信息破坏代码？即使在情况A中，功能模块身份必须将IntType模块视为SOMETYPE类型。那么如何明确宣布IntType为SOMETYPE类型会产生不同的结果？

Answer 1

:构造在核心语言和模块语言中是不同的。在核心语言中，它是一个注释构造。例如，((3, x) : 'a * 'a list)将表达式约束为某种类型，它是'a * 'a list的实例;因为这一对的第一个元素是一个整数，所以let (a, b) = ((3, x) : 'a * 'a list) in a + 1是很好的类型。模块上的:构造并不意味着这一点。

该构建M : S密封模块M到签名S。这是一个不透明的印章：只有在的打字使用中，签字S中给出的信息仍然可用。当你写module IntType : SOMETYPE = struct type t end，这是

module IntType = (struct type t end : SOMETYPE) 

由于类型字段中SOMETYPEt留下未指定的一个替代的语法，IntType有一个抽象类型字段t：类型IntType是一种新型的，由该定义生成。

顺便说一下，你的意思可能是module IntType = (struct type t = int end : SOMETYPE);但无论如何，IntType.t是一种抽象类型。

如果您想指定某个模块具有某个签名，同时保留某些类型的暴露，则需要为这些类型添加明确的相等性。没有构造可以添加所有可推广的平等，因为对模块应用签名通常意味着信息隐藏。为了简单起见，该语言仅提供了这种生成密封构造。如果您想使用已定义签名SOMETYPE并保留类型t的透明度，约束添加至签名：在这里

module IntType = (struct type t = int end : SOMETYPE with type t = int) 

Answer 2

如果你看看推断的签名，当你不写的东西明确：

# module IntType = struct type t = int end ;; 
module IntType : sig type t = int end 

签名暴露了t是int。您的签名，与此相反：

# module IntType : SOMETYPE = struct type t = int end ;; 
module IntType : SOMETYPE 

是真的：

# module IntType : sig type t end = struct type t = int end ;; 
module IntType : sig type t end 

这似乎解决你的问题：

# module IntType : (SOMETYPE with type t = int) = struct type t = int end ;; 
module IntType : sig type t = int end 
# module IdentityInt = Identity(IntType) ;; 
module IdentityInt : sig val f : IntType.t -> IntType.t end 
# IdentityInt.f 0 ;; 
- : IntType.t = 0 

（你不需要括号，但他们帮助精神解析）。基本上，你暴露了t与你的签名一致的事实。这样OCaml知道相等IntType.t = int。

有关内部结构的更多详细信息，请留给更有见识的人。

Answer 3

当你写：

module IntType : SOMETYPE = struct type t = int end ;; 

你都制约的InType的签名是完全SOMETYPE。这意味着，例如，类型t现在正在成为一种抽象类型（其实现方式对于typer而言是未知的）。

因此IdentityInt.f类型仍然是IntType.t -> IntType.t，但是，通过使用签名约束，您明确地从typer知识中删除了方程IntType.t = int。你得到的错误消息告诉你这一点。

Answer 4

您的密钥错误：

模块IntType上：SOMETYPE =结构输入t end ;;

当归于签名SOMETYPE，这是一个不透明的归属，并与int身份丢失。 IntType.t现在是一种抽象类型。您需要改写SOMETYPE with type t = int的签名。

该记录表明的区别：

# module type SOMETYPE = sig type t end;; 
module type SOMETYPE = sig type t end 
# module IntType : SOMETYPE with type t = int = struct type t = int end;; 
module IntType : sig type t = int end 
# module AbsType : SOMETYPE = struct type t = int end;;     
module AbsType : SOMETYPE 

围绕模块和归属于语言的设计问题以及所涵盖的首席设计师的1994 paper on modules, types, and separate compilation。毛茸茸的数学部分都可以跳过。