Extensible runtime type indicators and equality constraints.
This module provides logic for encapsulating arbitrary OCaml values with a runtime type indication, here called a type nym. A function is provided to compose a value and its corresponding type nym into a value of opaque type. Additional functions are provided to extract a typed value from an opaque value when provided with a nym for an equivalent type.
To handle the case where the nym type is extended, a class is provided that tests for equivalence of two nyms. Extending the nym type entails defining an subclass with methods that test for equivalence of the new variant cases. The functions that extract from values of opaque type are declared in a module signature that can be instantiated from an instance of the equivalence class.
The type of equality relation constraints.
val refl : ('a, 'a) eqThe reflexive equality constraint.
Use trans a b to obtain the transitive constraint from a to b.
val coerce : ('a, 'b) eq -> 'a -> 'bUse coerce eq v to coerce v into an equivalent type.
An opaque type is one comprising a value of existential type witnessed by a type nym for it.
An generalized algebraic type for values witnessed by a type nym.
The type nym indicating a value of opaque type. This kind of recursion is often useful for representing containers of heterogenously typed values that may themselves include containers.
The exception raised when extracting from an opaque value with a nym that is not equivalent to the encapsulated type.
class horizon : object ... endA class that defines the equality constraint for all the type nyms defined above and provides for extending the equality constraint for new type nyms by defining subclasses.
module type Form = sig ... endThe signature of modules for extracting opaque values within a given type equivalence horizon. Because all the functions in this module use the equiv method on the horizon used to construct it, expressions that directly match on the `Witness (_, nym)` type constructor are likely to be substantially more efficient.
Use form r to create an unpacking module for an equivalence class.
Include the default Form for the above horizon.
include FormUse opt n v to extract v' if n is equivalent to the encapsulated runtime type, otherwise raises an exception (conventionally Type_error).
Use opt n v to extract Some v' if n is equivalent to the encapsulated runtime type, otherwise returns None.
Use eq a b to produce the equivalence constraint for the types associated with nyms a and b under the horizon. Returns Eq if a and b are nyms for equivalent types, otherwise raises Type_error.