What is type (_, _) eq = Equal: ('a, 'a) eq (source) useful for? I've used refl in Coq, but haven't needed anything like in OCaml yet.
The type is defined and in an upcoming version of the OCaml Stdlib and there's a similar type in Base.
How can I know when to use this type, and what does code using this type look like?
The Base docs say:
The purpose of Type_equal is to represent type equalities that the type checker otherwise would not know, perhaps because the type equality depends on dynamic data, or perhaps because the type system isn't powerful enough.
So it sounds like I'm looking for examples where type equalities depend on dynamic data or the type system isn't powerful enough, where the equal type is helpful.
I found a use of an
equaltype with the same definition inStdlib.camlinternalFormatbut didn't understand it
UPDATE the quote from the Base docs above may not have been about eq specifically, and may be more relevant to Base.Type_equal.Id iuc.
The equality type
is probably the quintessential example of GADTs(Generalized Abstract Data Types). It is a witness that some types were equal in some context. Importantly, that witness can outlast the context in which those types were equal. It is thus useful when one need to transport some type equalities between functions or modules.
The easiest way to introduce such local equations in OCaml is to use the module system to hide an equation:
Here, inside the module
M, the fact thatt=intis trivial, and we can capture it withHowever, outside of the module, the equality has been lost, and it survives only through the
M.eqequality witness. Which means, that we can still learn thatM.xis in fact anintby matching over theM.eq:Outside the module system, local equations mostly appear in presence of GADTs which are thus the main context in which the
eqtype is useful.In fact, any GADTs can be replaced by
Eq. For instance, if we use GADTs to define a familly of compact array with optimized array representation in function of the element types:we can use this definition GADT to define common function that works on any compact array:
However, here we were mostly using the type equality recorded in the GADT constructor, we can do exactly the same thing with an ordinary variant that stores the right
Eqconstructor:This is less memory efficient and a bit harder to read, but this is doable. And this generality means that the
eqtype is a great way to transport equalities between functions or types. For instance, with thecompact_arraywitness for above I can use this witness to store a array with a witness of its type in a data structure:then I can match on the packed witness to recover a type.
but then I may need one function for each witness. The solution to avoid code duplication is then to write an equality function ... that returns an equality type:
As before with the
Mmodule, we are storing equalities from a context into a witness that can outlives this context.And then whenever, we want to compare two
compact_arrayimplementation, we can use===. For instance, we can first write a genericmapfunction which works on all compact array withWe can then use this function and
===to map a function to packed compact array if we guessed at runtime its type using a type witness:Here, we are using the
eqtype has way to communicate potential type equalities discovered in the body of===to the body ofmap_if_compatible. We could have recoved the same equality by matching onwandkexplicitly, but that would have been equivalent to inlining the definition of===inmap_if_compatible. In brief, theeqgive us a way to transport type equations between context in a composable way.As a side-note, it is important to note that the
eqtypes and GADTs types are all about local type equations. They are not more powerful than the type system, neither do they allow to generate types from runtime data. At most, they can bridge the types of runtime data with global type information by recovering local type equations between those types.