键入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

这是topelevel的回应:

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

Answer 1

我会说在从模块导出之前string -> string不会应用输入g.在模块内部(因为你没有给它一个类型)它有类型 'a -> 'a.(免责声明:我不是模块专家,试图学习.)

Answer 2

这里要理解的重要一点是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 ... endmake 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 -> stringOCaml的结论是,一切都很好.当然,使用的全部意义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