Avoiding record for polymorphism in ocaml

Question

Say I want to have polymorphic functions, here in a module.

  module type NewHType1 = sig
    type ('a, 'n) t
    type t'
    type ('n, 't) inj = { inj : 'a. ('a, 'n) t -> ('a, ('n, t') happ) app
    type ('n, 't) prj = { prj : 'a. ('a, ('n, t') happ) app -> ('a, 'n) t }

    val inj : ('n, 't) inj
    val prj : ('n, 't) prj
  end

Do I syntactically really have to have a polymorphic record type, with a superfluous record field ?

(I vaguely remember someone mentioning objects to avoid this extra noise (?))

Answer 1

You can encode existentials natively using GADT. For example, this is how you can encode higher-kinded polymorphism with GADT,

type ('p, 'f) app = ..

module Newtype1 (T : sig type 'a t end) () : sig
  type 'a s = 'a T.t
  type t

  val inj : 'a s -> ('a, t) app
  val prj : ('a, t) app -> 'a s
end = struct
  type 'a s = 'a T.t
  type t
  type (_,_) app += App : 'a s -> ('a, t) app
  let inj v = App v
  let prj (App v) = v
end

module Newtype2 (T : sig type ('a,'b) t end) () : sig
  type ('a, 'b) s = ('a, 'b) T.t
  type t

  val inj : ('a, 'b) s -> ('a, ('b, t) app) app
  val prj : ('a, ('b, t) app) app -> ('a, 'b) s
end = struct
  type ('a,'b) s = ('a,'b) T.t
  type t
  type (_,_) app += App : ('a,'b) s -> ('a, ('b,t) app) app
  let inj v = App v
  let prj (App v) = v
end

As a side note, you don't need to use records or anything else in the signature to specify that the type variable is polymorphic, as it is already polymorphic. I.e., you can describe your signature as simple as,

module type NewHType1 = sig
  type ('a, 'n) t
  type t'
  val inj : ('a, 'n) t -> ('a, ('n, t') happ) app
  val prj : ('a, ('n, t') happ) app -> ('a, 'n) t
end

It is because in value specifications (in module types) polymorphic variables denote polymorphic types, which is different from type constraints, which are used in value definitions, where type variables denote just variables that can have ground types, so if you want to prevent its unification with the ground type, you have to add a type annotation, e.g.,

module NewHType1 : sig
  type ('a, 'n) t
  type t'
  val inj : ('a, 'n) t -> ('a, ('n, t') happ) app
  val prj : ('a, ('n, t') happ) app -> ('a, 'n) t
end = struct
  type ('a,'n) t and t'
  let inj : 'a. ('a, 'n) t -> ('a, ('n, t') happ) app = fun _ -> assert false
  let prj : 'a. ('a, ('n, t') happ) app -> ('a, 'n) t = fun _ -> assert false
end

To summarize, 'a. 'a -> 'a type constraint generates the polymoprhic 'a -> 'a type. You might find the following answer useful as well.