Universal/heterogeneous maps.
These maps are useful for storing values of arbitrary type in a single map. In order
to recover a value, it must be looked up with exactly the Key.t
it was stored in.
In other words, given different Key.t
's from the same string
, one will not be able
to recover the key stored in the other one.
This is similar to Univ
in spirit, and is indeed built on top of Univ
.
A key in a Univ_map
is just a Type_equal.Id
.
Every Id.t
contains a unique id that is distinct from the Uid.t
in any other
Id.t
.
create ~name
defines a new type identity. Two calls to create
will result in
two distinct identifiers, even for the same arguments with the same type. If the
type 'a
doesn't support sexp conversion, then a good practice is to have the
converter be <:sexp_of< _ >>
, (or sexp_of_opaque
, if not using pa_sexp).
same_witness t1 t2
and same_witness_exn t1 t2
return a type equality proof iff
the two identifiers are the same (i.e. physically equal, resulting from the same
call to create
). This is a useful way to achieve a sort of dynamic typing.
same_witness
does not allocate a Some
every time it is called.
same t1 t2 = is_some (same_witness t1 t2)
.
keys that map to an accumulator value with an associated fold operation