Existential types as module types in OCaml

Question

Given a type

type 'a ty

and a module type

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

I can define

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

and I would like to define a function (although this doesn't typecheck)

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

with the intended effect that whenever m : (module TY) then ofTY m : m.a ty, so trying to define it as

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

does not have the intended effect.

What is the appropriate way of defining ofTY?

octachron octachron · Accepted Answer · 2021-01-19T11:38:46

OCaml is not dependently typed, thus a type cannot depend on a value. In other words, since m is a value, m.a cannot be a type.

Another way to see the issue is that in the module type

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

the value x is existentially quantified by type a, and there is no way to remove such existential quantification, at most you can express it in different ways.

Existential types as module types in OCaml

1 Answers