OCaml仿函数::反直觉行为

Question

我正在尝试使用OCaml的模块语言(​​3.12.1),为模块定义仿函数和签名等等,主要是遵循OCaml手册第2章中的示例,我偶然发现了一个明显的情况我的仿函数和模块签名如何工作的心理模型是有缺陷的.我试图将我遇到的情况缩小到可能的最短代码量,所以不要问我想要完成什么,这是一个完全人为的例子来演示有问题的OCaml功能.

因此,我们有一个functor,它只提供一个标识函数'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),其f功能行为与预期.

现在是不直观的部分.如果我们想明确提供的模块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中,仿函数模块Identity也必须将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在键入使用时,只有签名中给出的信息仍然可用M : S.在您编写时module IntType : SOMETYPE = struct type t end,这是一种替代语法

module IntType = (struct type t end : SOMETYPE)

由于类型字段t中SOMETYPE被保留为未指定,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

(你不需要parens,但他们帮助精神解析).基本上,你揭露了t是带有签名的int的事实.因此OCaml知道IntType.t = int的相等性.

有关内部细节的更多细节,我会留给更多知识渊博的人.

Answer 3

当你写:

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

你都制约的签名InType必须准确SOMETYPE.例如,这意味着该类型t现在变为抽象类型(其实现对于typer来说是未知的).

所以IdentityInt.f类型仍然是IntType.t -> IntType.t,但是,通过使用签名约束,您已经明确地IntType.t = int从typer知识中移除了等式.你得到的错误信息正好告诉你.

Answer 4

你的关键错误在这里:

module IntType:SOMETYPE = struct type t end ;;

当你归咎于签名时SOMETYPE,它是一个不透明的归属,并且int遗失了同一性.Type 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年关于模块,类型和单独编译的论文中得到了很好的阐述.毛茸茸的数学部分都可以跳过.