存在类型作为 OCaml 中的模块类型

Question

给定一个类型

type 'a ty

和模块类型

module type TY = (sig  type a  val x : a ty  end)

我可以定义

let toTY (type b) (x' : b ty) : (module TY) =
(module struct
  type a = b
  let x = x'
end)

我想定义一个函数（尽管这不进行类型检查）

let ofTY (m : (module TY)) : m.a ty = ???

的预期效果是每当 m : (module TY) 然后 ofTY m : m.a ty，所以试图将其定义为

let ofTY (type b) (m : (module TY with type a = b)) : b ty = ...

没有达到预期的效果。

定义 ofTY 的正确方法是什么？

Answer 1

OCaml 不是依赖类型的，因此类型不能依赖于值。换句话说，因为 m 是一个值，所以 m.a 不能是一个类型。

查看问题的另一种方法是在模块类型中

module type TY = sig
  type a
  val x: a ty
end

值x是按类型a进行存在量化的，这种存在量化是没有办法去掉的，顶多换个方式表达。

Existential types as module types in OCaml