OCaml 中的值级模块打包和函子

Question

我想知道为什么一个例子失败了，而另一个例子却失败了。

  (* this fails  *)
  (* (l fails to type check)
     This expression has type 'a but an expression was expected of type
     (module M.TFixU)
     The module type M.TFixU would escape its scope
  *)
  let foldList1 (type ar) algr l =
    let module M = FixT (ListIntF) in
    let (module LU : M.TFixU) = l in
    assert false

  (* but this works  *)
  let foldList2 (type ar) algr l =
    let (module LU : FixT(ListIntF).TFixU) = l in
    assert false

完整代码

module Higher = struct
  type ('a, 't) app

  module type NewType1 = sig
    type 'a s
    type t

    val inj : 'a s -> ('a, t) app
    val prj : ('a, t) app -> 'a s
  end

  module NewType1 (X : sig
    type 'a t
  end) =
  struct
    type 'a s = 'a X.t
    type t

    external inj : 'a s -> ('a, t) app = "%identity"
    external prj : ('a, t) app -> 'a s = "%identity"
  end
end

module Fix = struct
  open Higher

  module FixT (T : NewType1) = struct
    module type T_Alg = sig
      type a

      val alg : (a, T.t) app -> a
    end

    module type TFixU = sig
      module App : functor (A : T_Alg) -> sig
        val res : A.a
      end
    end

    type tFixU = (module TFixU)
  end
end

module Pb = struct
  open Higher
  open Fix

  (* intro *)
  type 'r listIntF = Empty | Succ of (int * 'r)

  module ListIntF = NewType1 (struct
    type 'r t = 'r listIntF
  end)

  (* this fails  *)
  let foldList1 (type ar) algr l =
    let module M = FixT (ListIntF) in
    let (module LU : M.TFixU) = l in
    (* (l fails to type check)
       This expression has type 'a but an expression was expected of type
       (module M.TFixU)
       The module type M.TFixU would escape its scope
    *)
    let module T = LU.App (struct
      type a = ar

      let alg = algr
    end) in
    T.res

  (* but this doesn't  *)
  let foldList2 (type ar) algr l =
    let (module LU : FixT(ListIntF).TFixU) = l in
    let module T = LU.App (struct
      type a = ar

      let alg = algr
    end) in
    T.res
end

Answer 1

在第一种情况下， 的类型l与 中定义的类型统一module M，后者定义了模块类型。由于类型是在 value 之后引入的l，value 是 eager 语言中的参数，因此它已经存在，因此该值l接收到在创建时尚不存在的类型。OCaml 类型系统的健全性要求是值生命周期必须包含在其类型生命周期内，或者更简单地说每个值必须有一个类型。最简单的例子是，

let x = ref None  (* here `x` doesn't have a type since it is defined later *)
type foo = Foo;;  (* the `foo` scope starts here *)
x := Some Foo (* foo escapes the scope as it is assigned to `x` via `foo option` *)

另一个涉及函数参数的简化示例如下：

let foo x =
  let open struct
    type foo = Foo
  end in
  match x with
  | Some Foo -> true (* again, type foo escapes the scope as it binds to `x` *)
  | None -> false

Oleg Kiselyov 的《OCaml 类型检查器如何工作——或者说多态性和垃圾收集有什么共同点》是一篇非常好的文章，可以帮助您深入理解范围和泛化。

l关于第二种情况，您明确指定了使用 OCaml 函子的应用性质的类型。因为类型检查器知道 的生命周期FixT(ListIntF).TFixU大于l它的生命周期，所以很高兴。