Figuring out how to return an open polymorphic variant from application to a module

Learning
, , , ,
1

I stumbled upon an interesting problem when attempting to figure out a way to nicely and elegantly encode tags for data in a modular fashion.

First, we may want to approach the problem in an elementary fashion:

module type TAG = sig
  type 'a t
  type data
  val tag : data -> 'a t
end

let tagme (type a b)
    (module Tag : TAG with type data = a)
    (item : a) : b Tag.t =
  (Tag.tag item : b Tag.t)

It is obvious that it won’t work, because we’ll be attempting to return an existentially typed value. Now, how may we hide this existential type?

Btw, I also don’t see a way to refer to the _ Tag.t type if I was referencing it from the type definition after the function itself, before the arguments. Could this limitation be overcome in general?

Consider the following monstrosity as an attempt to find a solution:

module type TAG = sig
  type row
  type 'a tag constraint 'a = row
  type t
  type data
  val tag : data -> t
end

let tagme: type a b.
  (module TAG with type data = a and type t = b) -> a -> b =
  fun (module Tag) (item : a) ->
  Tag.tag item


module Int_tag :
  TAG with type data = int =
struct
  type row (* supposed to represent 'a variable in tag type *)
  type 'a tag = [> `Int of int ] as 'a
  type t
  type data = int
  let tag item = `Int item
end

The goal is to obtain a polymorphic variant value from tagme. On my first attempt, I wanted to return values from tagme typed with non-zero arity types within the module TAG, but it wasn’t possible to express 'a t in the module type specification. Thus, I tried to approach by returning abstract types. Now, I cannot construct the specific modules.

Does this problem have a solution? Something more general? Am I overlooking a known method? Am I overlooking something obvious?

I wonder, if trying to use something from the Higher_kinded library would actually help? My slight concern with that approach is that when I need modules in a more efficient implementation, I may be introducing an extra layer of wrapper values (though it appears that the Higher_kinded specifically uses %identity, and only changes types).

2

This is a contradiction. Polymorphic variants are structural types (they exist without being declared), they cannot be derived from values and using modules doesn’t add any expressiveness at this level.

The complexity of the higher-kinded library is rarely justified, I would advise to ignore this library until you are far more familiar with OCaml.

3

I’m more familiar with Coq than OCaml, and not so much in the context of creating type systems for programming languages.

I attempted to use higher-kinded library as an exercise to solve this problem, but apparently it does not allow me to resolve the issue with the lingering 'a' type in the 'a t. However, by varying over the higher_ordertype, I was able to get the definition of thetagme` to compile.

The use of module to pass to the tagme function is an alternative to the use of records or objects. It’s much more of a software engineering approach than anything else. I would appreciate your perspective on how similar problems could be tackled, when I wish to supply a whole record of functions, and maybe even type, to another function, so that I would be able to use them in another function. The records seem to compile to an actual value, with memory footprint and pointers. The modules should not have that issue, and also they may carry types with them.

Note that if I used GADTs, I would’ve likely had to provide the functional definitions at the calling site, which I wanted to avoid. Yes, I could also have GADT tags that carry records with them, but that’s hardly different from just passing records around, including efficiency-wise.

The motivation for attempting to use functors stems from the need to deal with the fact that the compiler would not allow me to compile the code when the 'a t is a closed variant type. I thought that by varying over variants with 'a, I may be able to construct a function that would return an open variant. Alas, it’s not working out, since the 'a in open variants is much more of a constraint than a variable.