在模块中使用"带类型"结构时放松类型检查

Sur*_*tor 2 ocaml types module signature

我已经定义了两个模块类型和两个模块

module type FOO = sig type e end
module type BAR = sig type t end    
module Foo : FOO = struct type e = int end
module Bar : BAR = struct type t = int end
Run Code Online (Sandbox Code Playgroud)

然后我将一个仿函数定义为

module Fun (F:FOO) (B:BAR with type t = F.e) = struct type x = string end
Run Code Online (Sandbox Code Playgroud)

(这是一个玩具示例,请忽略这一事实FB不使用的算符)

现在,如果我定义模块

module Bla = Fun (Foo) (Bar)
Run Code Online (Sandbox Code Playgroud)

我明白了

Error: Signature mismatch:
       Modules do not match:
         sig type t = Bar.t end
       is not included in
         sig type t = Foo.e end
       Type declarations do not match:
         type t = Bar.t
       is not included in
         type t = Foo.e
Run Code Online (Sandbox Code Playgroud)

虽然这两个Bar.tFoo.e作为被定义intOCaml的考虑Bar.tFoo.e是不同的.这就是打字系统的工作方式,一般认为这两种类型不同是有意义的(参见Functors和Type Abstraction的最后一段).

问题:有时我可能希望这通过类型检查,因为出于我的目的,它们可以被认为是平等的.有没有办法放松一下?


使用gasche建议删除强制,上面的代码可以写成

module type FOO = sig type e end
module type BAR = sig type t end
module Foo = struct type e = int end
module Bar = struct type t = int end
module Fun (F : FOO with type e=int) (B : BAR with type t = int) = struct type x = F.e * B.t end
module Bla = Fun (Foo) (Bar)
Run Code Online (Sandbox Code Playgroud)

编译好.奇怪的是,我明白了

# let f x : Bla.x = (x,x);;
val f : Foo.e -> Bla.x = <fun>
Run Code Online (Sandbox Code Playgroud)

问题:为什么推断出来的xFoo.e?它也可以Bar.t吗?

gas*_*che 5

问题是你如何定义FooBar:module Foo : FOO = ....通过在此处强制使用此签名,您可以"密封"模块并使类型抽象化.它无法恢复.你应该在: FOO这里删除强制,并在以后需要抽象时使用它.你也可以用module Foo : (FOO with type e = int) = ....