ocaml - 输入Ocaml的一个奇怪示例

Question

奇怪的是，该ocaml代码段由顶级人很好地键入了。查看结构，如果g如顶级所示为int-> int类型，则该结构的h x = g x部分将无法获得类型统一的信息。那么任何人都可以澄清一下吗？

module Mymodule : sig
  val h:int ->int
  val g: string-> string
end = struct
  let g x = x
  let h x = g x
end

这是最高层的回应:

  module Mymodule : sig val h : int -> int val g : string -> string end

Answer 1

在这里要了解的重要一点是，OCaml以组合方式执行类型推断，即首先将推断struct ... end的类型，然后才将推断出的类型与sig ... end进行匹配，以验证该结构确实实现了签名。

例如，如果您写

module Monkey : sig val f : int -> int end =
struct
  let f x = x
end 

然后OCaml将很高兴，因为它将看到 f具有多态类型 'a -> 'a，该类型可以专用于所需的 int -> int类型。因为 sig ... end使 Monkey不透明，即签名隐藏了实现，所以即使实际实现具有多态类型，它也会告诉您 f的类型为 int -> int。

在您的特定情况下，OCaml首先推断 g的类型为 'a -> 'a，然后推断 h的类型也为 'a -> 'a。因此得出结论，该结构具有类型

sig val g : 'a -> 'a val h : 'a -> 'a end

接下来，将签名与给定的签名进行匹配。因为 'a -> 'a和 int -> int可以将 string -> string类型的函数专用化，所以OCaml得出结论，一切都很好。当然，使用 sig ... end的全部目的是使结构不透明(实现是隐藏的)，这就是为什么顶层不公开 g和 h的多态类型的原因。

这是另一个示例，显示了OCaml的工作方式:

module Cow =
struct
  let f x = x
  let g x = f [x]
  let a = f "hi"
end

module Bull : sig
  val f : int -> int
  val g : 'b * 'c -> ('b * 'c) list
  val a : string
end = Cow

响应是

module Cow :
    sig 
      val f : 'a -> 'a
      val g : 'a -> 'a list
      val a : string
    end

module Bull :
    sig
      val f : int -> int
      val g : 'a * 'b -> ('a * 'b) list
      val a : string end
    end