Polymorphic homogeneous map

[mlemerre]

I came across needing polymorphic (but homogeneous) maps, where a 'a t goes from a 'a key to a 'a value (but always the same 'a for the whole map). Then, the MAP_WITH_VALUE interface does not work well (because keys are homogeneous) and the HETEROGENEOUS_MAP is not very convenient (because the functions need the higher-rank polymorphism).

Such a polymorphic map is useful when defining combined maps, e.g. I want a polymorphic map of terms, which is a heterogeneous map from 'a term to a 'a map, but the second map is a map from a 'a term to another 'a term and is this time homogeneous (and defining a fold on this combined map is not easy because of the higher-ranked polymorphism).

How could we integrate this?

[dlesbre]

You can't, the polymorphic fumctiom are required even when simply mapping 'a key to 'a value. See dmap's S_WITH_VALUE which does exactly this.

One way to side-step this a bit is to replace fully polymorphic function with ones that take existential arguments. I.E. replace:

type 'b polyiter = { 'a. 'a key -> ('a, 'b) value -> unit }
val iter: 'b polyiter -> 'b t -> unit

With:

type _ key_value = KeyValue : 'a key * ('a, 'b) value -> 'b key_value
val iter: ('b key_value -> unit) -> 'b t -> unit

This would avoid the bug we've been having, at the cost of boxing/unboxing arguments at each function call.