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

如何解决存在类型作为 OCaml 中的模块类型

给定类型

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 的适当方式是什么？

解决方法

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

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

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

值x被类型a存在量化，这种存在量化没有办法去掉，顶多可以用不同的方式表达。