Typing limitation with first-class modules, existential types and type constraints

Community
1

I like parametricity, and prefer as much as possible to use parametric data-types than functors. Even though this may have a cost at runtime. Following this paradigm, assume I want to write a program that requires to use a set data-structure but I want to be parametric over the type of my elements. Using the standard library of OCaml, I could use a functor:

module Make (C : sig
  type param

  module Set : Set.S with type elt = param
end) =
struct
  type t = {foo : int; bar : C.Set.t}

  (* ... *)
end

but as I said, I would prefer to avoid those for various personal reasons.

This is actually doable by doing so:

type 'param set =
  | E : {
      md : (module Set.S with type elt = 'param and type t = 'a);
      set : 'a;
    }
      -> 'param set

type 'param t = {foo : int; bar : 'param set}

I can write some wrappers for using functions declared by the signature Set.S my new datatype, but it works.

I will pay some runtime cost by boxing/unboxing the module and the corresponding set but that’s fine.

Next problem: Can I do the same thing for a Map? Well, it is a bit more involved. Sure, I could use a hashtbl instead, but I would like my program to be functional.

The solution I came up with is the following:

module type MAP = sig
  type key

  type value

  include Map.S with type key := key

  type map

  val inj : value t -> map

  val proj : map -> value t
end

type ('key, 'value) t =
  | E : {
      foo :
        (module MAP
           with type key = 'key
            and type value = 'value
            and type map = 'c);
      bar : 'c;
    }
      -> ('key, 'value) t

(* An example to implement such MAP signature *)

module Map : MAP with type key = int and type value = int = struct
  type value = int

  include Map.Make (Int)

  type map = value t 

  let inj (x : value t) : map = x [@@inline]

  let proj (x : map) : value t = x [@@inline]
end

This time, I need to use inj and proj functions which were not necessary for the case of set. The reason is that I cannot write in the MAP signature the equality:

type map = value t

Otherwise the declaration of ('key,'value) t is invalid:

Error: In this 'with' constraint, the new definition of map
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type map
       is not included in
         type map = value t

However, I believe that because the type variable 'c is hidden via a GADT, logically it could behave as an existential. Consequently, I wonder whether it would be a valid extension of the type system of OCaml to accept my signature MAP where the definition of type map is exposed with the datatype ('key,'value) t given above? If not, I would be curious to understand why?

Out of curiosity, is there any “better” way (easier to use, better performances, …) to achieve a similar result?

1 Like
2

You don’t need GADT for existentials if you are already using first-class modules, which can carry existentials as well. I tried to simplify a bit and got the following:

module type MAP = sig
  type key
  type value

  include Map.S with type key := key

  type map = value t

  val map : map
end

type ('key, 'value) t = (module MAP with type key = 'key and type value = 'value)

let get (type k v) (map : (k, v) t) (k : k) : v option =
  let (module Map) = map in
  Map.find_opt k Map.map
2 Likes
3

Sounds better indeed. So my motivation was not as a good as I thought, but I wonder whether the type system could be extended to accept the program I proposed in my initial topic?

Many thanks for your answer in any case!

4

You can also replace your conversions functions by an explicit type equality:

type (_,_) eq = Refl: ('a,'a) eq

module type MAP = sig
  type key
  type value
  include Map.S with type key := key

  type map
  val eq: (map, value t) eq
end
...
let add (type k v) (key:k) (value:v) 
   (E { foo = (module M) as foo; bar }:(k,v) t) =
  let Refl = M.eq in
  let bar = M.add key value bar in
  E ({ foo; bar})
2 Likes
5

I tried to implement something simple like cardinal… ideally:

let cardinal (E {md; set}) = md.cardinal set

I started by making this actual OCaml syntax:

let cardinal (E { md = (module Md); set }) = Md.cardinal set

but the module signature has type variables so I had to get rid of those

let cardinal (type elt t)
  (E { md = (module Md : Set.S with type t = t and type elt = elt); set })
=
  Md.cardinal set

but then even this is wrong because t has to be introduced in E’s pattern, and I also realized then that I know how to name existentials for tuple-style args, not for record-style args… so after a redefinition:

let cardinal (type elt)
  (E (type t) ((module Md), set : (module Set.S with type t = t and type elt = elt) * t))
=
  Md.cardinal set

and now it works. Is this how much it really takes? And if yes, is avoiding functors really worth all this? I’m curious to learn the advantages to this style of paramitricity.

EDIT: the error

Error: The type of this packed module contains variables:
       (module Set.S with type elt = 'a and type t = $E_'a)

was a little misleading, I don’t need to specify $E_'a, only 'a, even though (in my mind) the former appears to count as a type variable. so really it’s not that bad:

let cardinal (type elt) (E {md = (module Md); set} : elt set) = Md.cardinal set

Also during my playing with these definitions, I found this funky type syntax: (a, b) set.E. It’s not valid, just in error messages.