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 ... endThe equivalence horizon of type nyms defined above.
module type Form = sig ... endThe signature of modules for extracting opaque values within a given type equivalence horizon.
Use form r to create an unpacking module for an equivalence class.
Include the default Form for the above horizon.
include FormUse ck n v to test whether n is equivalent to the encapsulated runtime type.
Use opt n v to extract Some v' if n is equivalent to the encapsulated runtime type, otherwise returns None.