Destructive substitution: is it possible to replace a type constructor with a monomorphic type?

core
#1

I have often wanted something like the following:

open Core

(* K.t -> V.t *)
type t = (K.t, V.t, K.comparator_witness) Map.t
include Map.Make(K)

Unfortunately, the include statement fails because Map.Make(K) defines

type 'v t = (K.t, 'v, K.comparator_witness) Map.t

but the module can only contain a single definition of the type t.

The usual way around this is to use destructive substitution – except in this case we want to substitute the monomorphic

type t = (K.t, V.t, K.comparator_witness) Map.t

for the polymorphic type

type 'v t = (K.t, 'v, K.comparator_witness) Map.t

Is there any way to achieve this?

Here is what I have tried:

open Core
type t = (Int.t, String.t, Int.comparator_witness) Map.t
include (Map.Make_using_comparator(Int) : Map.S
  with type Key.t = Int.t
  with type Key.comparator_witness = Int.comparator_witness
  with type _ t := t)

This fails with

Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type _ t = t
       is not included in
         type 'a t =
             (Key.t, 'a, Key.comparator_witness) Core_kernel__.Map_intf.Map.t
       File "src/map_intf.ml", line 300, characters 2-86:
         Expected declaration

I have also tried

open Core
type _ t0 = (Int.t, String.t, Int.comparator_witness) Map.t
include (Map.Make_using_comparator(Int) : Map.S
  with type Key.t = Int.t
  with type Key.comparator_witness = Int.comparator_witness
  with type 'a t := 'a t0)

which fails with a very similar error.

#2

Not sure why this works, but I got it to work with:

open Core

include (Map.Make_using_comparator(Int) : Map.S
         with module Key := Int
          and type 'a t := (Int.t, 'a, Int.comparator_witness) Map.t)

type t = (Int.t, String.t, Int.comparator_witness) Map.t

mli:

open Core

type t = (Int.t, String.t, Int.comparator_witness) Map.t
2 Likes
#3

Very cool! I was almost certain this was impossible.

Actually, after doing some research, I found that this was impossible until very recently:

Prior to OCaml 4.06, there were a number of restrictions: one could only remove types and modules at the outermost level (not inside submodules), and in the case of with type the definition had to be another type constructor with the same type parameters.

When executing your code in Ocaml 4.05.0, I get

Error: Only type constructors with identical parameters can be substituted.
1 Like
#4

I have a similar issue that I often find myself tackling. I often write stuff like:

talias.ml

open Core

type t = (String.t, Type.t, String.comparator_witness) Map.t

tcontext.ml

open Core

type t = (String.t, Type.t, String.comparator_witness) Map.t

to represent (in this example) a type alias environment and typing context in a type checker. Talias.t and Tcontext.t are the same, so in my type checker I could make a mistake and merge a typing context with a type alias environment Map.merge ~f talias tctx.

What I’d really like are two modules Talias and Tcontext which are essentially monomorphic versions of Map, and which also have incompatible types.

tcontext.mli

type t

val singleton : String.t -> Type.t -> t

...and all the other Map functions...

tcontext.ml

open Core

type t = (String.t, Type.t, String.comparator_witness) Map.t

let singleton s t = Map.singleton (module String) s t

Is there any slicker way? The solutions mentioned above are almost what I need, but the signature for Map.make_using_comparator is still polymorphic in value type and even if fully monomorphic the types would still be compatible.

I’ve also considered using private type abbreviations, but haven’t come up with anything.