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中定义的类型统一，定义了模块类型。由于类型是在值 l 之后引入的，它是一种急切语言中的参数，因此它已经存在，因此值 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 的 How OCaml type checker works -- or what polymorphism and garbage collection have in common.

是一篇非常好的文章，可以帮助您理解深入的范围和概括

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

OCaml 中的值级模块打包和仿函数

value level module packing and functors in OCaml

ocaml

module