ocaml - 为什么OCaml不能推断出以下类型：

Question

考虑以下代码

module type Foo = sig 
  type t
  val do_with_t : t -> unit
end

let any_foo t (module F : Foo) = F.do_with_t t

被以下可爱的类型错误拒绝：

Error: This expression has type F.t but an expression was expected of type F.t
      The type constructor F.t would escape its scope

但是一旦我添加以下类型注释就被接受：

let any_foo (type s) (t:s) (module F : Foo with type t = s) = F.do_with_t t

共享约束对我来说很有意义，所以我的问题是为什么 OCaml 不能从我t在函数内部的使用中推断出类型签名。

score 7 · Accepted Answer

我不是专家，但这是我对此的看法。

真正的错误是消息的最后一点：

类型构造函数 Ft 将逃脱其范围

为了理解错误信息，让我们首先any_foo在没有模式匹配参数的情况下重写，并重命名参数以使解释更容易理解：

let any_foo arg foo = 
  let (module F : Foo) = foo in
    F.do_with_t arg

您在这里使用一流的模块，并将变量解包foo到新的模块中F，在该 let 语句的范围内。

arg现在让我们考虑可以从这个事实中推断出的论点类型。显然，类型是F.t，但关键的是，这是一种仅在当前范围内已知的类型，因为module F仅在当前范围内已知。

现在让我们尝试定义结果any_foo函数的类型：

val any_foo : F.t -> (module Foo) -> unit

还有你的问题，你正试图F.t从函数范围的深处公开新铸造的类型。换句话说，您期望调用者知道仅存在于您的函数内部的类型。或者，换一种说法，您期望该类型F.t能够“逃脱”其范围，以吸引更广泛的受众。

现在我们知道了问题所在，我们可以认识到需要向编译器解释这种类型存在于“外部”范围内，并且参数arg属于该类型。

换句话说，我们需要为新生成的模块添加一个约束，F以说明参数arg的类型等于t我们新模块中的类型F。为此，我们可以使用本地抽象类型。

继续使用相同的功能，我们可以添加一个局部抽象类型a，并用它来约束模块F：

let (type a) any_foo arg foo = 
  let (module F : Foo with type t = a) = foo in
    F.do_with_t arg

让我们考虑一下any_foo现在的类型。

val any_foo : 'a -> (module Foo with type t = 'a) -> unit

那里没有问题。

为了完整起见，让我们回到我们的模式匹配版本：

let (type a) any_foo arg (module F : Foo with type t = a) =
  F.do_with_t arg

score 6 · Accepted Answer

这并不能真正回答您的问题，但在您的情况下，您只需要引入一个新的类型变量s：

let any_foo (type s) t (module F : Foo with type t = s) = F.do_with_t t

即你不需要(t:s)，因为类型推断在这里可以正常工作。

2 回答 2