# Destructive substitution: is it possible to replace a type constructor with a monomorphic type? **URL:** \ **Category:** Learning\ **Tags:** core\ **Created:** [April 9, 2018, 9:04pm UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830 "2018-04-09T21:04:03Z")\ **Posts on this page:** 5\ **Page:** 1
**Author:** ![smolkaj](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/smolkaj/32/266_2.png) [@smolkaj](https://discuss.ocaml.org/u/smolkaj)\ **Post date:** [April 9, 2018, 9:04pm UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830/1 "2018-04-09T21:04:03Z")
I have often wanted something like the following: ```ocaml 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 ```auto 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 ```auto type t = (K.t, V.t, K.comparator_witness) Map.t ``` for the polymorphic type ```auto type 'v t = (K.t, 'v, K.comparator_witness) Map.t ``` Is there any way to achieve this? Here is what I have tried: ```auto 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 ```auto 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 ```auto 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. ---
**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\ **Post date:** [April 9, 2018, 11:07pm UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830/2 "2018-04-09T23:07:15Z")
Not sure why this works, but I got it to work with: ```ocaml 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: ```ocaml open Core type t = (Int.t, String.t, Int.comparator_witness) Map.t ``` ---
**Author:** ![smolkaj](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/smolkaj/32/266_2.png) [@smolkaj](https://discuss.ocaml.org/u/smolkaj)\ **Post date:** [April 10, 2018, 1:16am UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830/3 "2018-04-10T01:16:34Z")
Very cool! I was almost certain this was impossible. Actually, after doing some research, I found that [this was impossible until very recently:](https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec248) > 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 ```auto Error: Only type constructors with identical parameters can be substituted. ``` ---
**Author:** ![ins](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ins/32/923_2.png) [@ins](https://discuss.ocaml.org/u/ins)\ **Post date:** [April 18, 2019, 1:31pm UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830/4 "2019-04-18T13:31:43Z")
I have a similar issue that I often find myself tackling. I often write stuff like: **talias.ml** ```auto open Core type t = (String.t, Type.t, String.comparator_witness) Map.t ``` **tcontext.ml** ```auto 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** ```auto type t val singleton : String.t -> Type.t -> t ...and all the other Map functions... ``` **tcontext.ml** ```auto 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](https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec237), but haven’t come up with anything. ---
**Author:** ![Konstantin\_Olkhovski](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/konstantin_olkhovski/32/1494_2.png) [@Konstantin\_Olkhovski](https://discuss.ocaml.org/u/Konstantin_Olkhovski)\ **Post date:** [July 30, 2019, 10:05am UTC](https://discuss.ocaml.org/t/destructive-substitution-is-it-possible-to-replace-a-type-constructor-with-a-monomorphic-type/1830/5 "2019-07-30T10:05:01Z")
Also looking for a solution to make monomorphic version of a module with some specialized extensions. @ins have you managed to figure it out since your last post maybe?