[ANN] Dmap : type-safe dependent (heterogeneous) immutable maps

Community
3

Hi,

thanks for asking. Here are the differences with hmap and gmap, as far as I understand. Please correct me if I misunderstood some parts.

  • hmap only supports keys with no contents. In particular, no total ordering of keys is required. Instead, you can dynamically create new keys, with the type index that you want. It is fully type-safe (no assert false, no Obj.magic, etc). It does not support (but maybe it could) a polymorphic map function (this requires second-order polymorphism). It reuses the standard library’s Map implementation by calling Map.Make.
  • gmap supports keys with contents, and expects a total ordering function that returns a GADT to witness type equality, exactly as I did in dmap. It supports a polymorphic map function (using second-order polymorphism). It reuses the standard library’s Map implementation by calling Map.Make. The implementation records the keys twice: as keys, and as part of the associated data, so that type equality witnesses can be exploited. This results in extra calls to the comparison functions on keys (see the code of get for an example). The extra calls and the double recording of keys might have an impact in terms of cost, that I cannot quantify. I should be measured. The code is almost type-safe: it relies on the invariant the key is the same as the key part that is recorded as data for that that binding. The impossible cases returned by the comparison function are given the assert false behavior.
  • dmap also supports a polymorphic map function. It does not store keys twice: as in the standard library’s implementation, the keys are stored only once. In comparison to gmap, the comparisons on keys are not done twice. The code is completely type-safe: no assert false is introduced to handle the impossible cases of key comparison. The implementation duplicates the one of the standard library, rather than calling Map.Make. The exported functions and their names are on par with the standard library’s Map.
2 Likes