# Typing limitation with first-class modules, existential types and type constraints
**URL:** https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261
**Category:** Community
**Created:** [January 27, 2023, 9:07am UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261 "2023-01-27T09:07:28Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@Saroupille](https://discuss.ocaml.org/u/Saroupille)
#### Post date: [January 27, 2023, 9:07am UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261/1 "2023-01-27T09:07:28Z")
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:
```ocaml
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:
```ocaml
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:
```ocaml
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:
```ocaml
type map = value t
```
Otherwise the declaration of `('key,'value) t` is invalid:
```bash
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?
---
### Author:  [@gasche](https://discuss.ocaml.org/u/gasche)
#### Post date: [January 27, 2023, 9:13am UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261/2 "2023-01-27T09:13:13Z")
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:
```ocaml
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
```
---
### Author:  [@Saroupille](https://discuss.ocaml.org/u/Saroupille)
#### Post date: [January 27, 2023, 9:39am UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261/3 "2023-01-27T09:39:03Z")
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!
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [January 27, 2023, 9:53am UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261/4 "2023-01-27T09:53:34Z")
You can also replace your conversions functions by an explicit type equality:
```ocaml
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})
```
---
### Author:  [@hyphenrf](https://discuss.ocaml.org/u/hyphenrf)
#### Post date: [January 27, 2023, 4:36pm UTC](https://discuss.ocaml.org/t/typing-limitation-with-first-class-modules-existential-types-and-type-constraints/11261/5 "2023-01-27T16:36:52Z")
> [@Saroupille](#):
>
> ```auto
> 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 tried to implement something simple like cardinal… ideally:
```ocaml
let cardinal (E {md; set}) = md.cardinal set
```
I started by making this actual OCaml syntax:
```ocaml
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
```ocaml
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:
```ocaml
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
```ocaml
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:
```ocaml
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.