Блог

Заданный тип

 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 , и нет способа удалить такое экзистенциальное количественное определение, в лучшем случае вы можете выразить его по-разному.