package orsetto

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Extensible runtime type indicators and equality constraints.

Overview

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.

Relational Constraints
type (_, _) eq =
  1. | Eq : ('a, 'a) eq

The type of equality relation constraints.

val refl : ('a, 'a) eq

The reflexive equality constraint.

val symm : ('a, 'b) eq -> ('b, 'a) eq

Use symm eq to obtain the symmetric constraint of eq.

val trans : ('a, 'b) eq -> ('b, 'c) eq -> ('a, 'c) eq

Use trans a b to obtain the transitive constraint from a to b.

val coerce : ('a, 'b) eq -> 'a -> 'b

Use coerce eq v to coerce v into an equivalent type.

Opaque Type

An opaque type is one comprising a value of existential type witnessed by a type nym for it.

type _ nym = ..

The extensible generalized algebraic data type of type nyms.

type opaque = private
  1. | Witness : 'a * 'a nym -> opaque

An generalized algebraic type for values witnessed by a type nym.

Runtime Type Indicators
type nym +=
  1. | Unit : unit nym

The runtime type for the unit value.

type nym +=
  1. | Bool : bool nym

The runtime type for boolean values.

type nym +=
  1. | Char : char nym

The runtime type for character values.

type nym +=
  1. | Uchar : Uchar.t nym

The runtime type for Unicode codepoint values.

type nym +=
  1. | String : string nym

The runtime type for string values.

type nym +=
  1. | Bytes : bytes nym

The runtime type for byte array values.

type nym +=
  1. | Int : int nym

The runtime type for integer values.

type nym +=
  1. | Int32 : int32 nym

The runtime type for boxed 32-bt integer values.

type nym +=
  1. | Int64 : int64 nym

The runtime type for boxed 64-bit integer values.

type nym +=
  1. | Float : float nym

The runtime type for floating point values.

type nym +=
  1. | Option : 'a nym -> 'a option nym

The runtime type for option values.

type nym +=
  1. | Pair : 'a nym * 'b nym -> ('a * 'b) nym

The runtime type for pair values.

type nym +=
  1. | Seq : 'a nym -> 'a Seq.t nym

The runtime type for sequence values.

type nym +=
  1. | Opaque : opaque 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.

val witness : 'a nym -> 'a -> opaque

Use witness n v to make an opaque value of v witnessed by n.

type exn +=
  1. | Type_error

The exception raised when extracting from an opaque value with a nym that is not equivalent to the encapsulated type.

class horizon : object ... end

A 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 ... end

The 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.

val form : horizon -> (module Form)

Use form r to create an unpacking module for an equivalence class.

Include the default Form for the above horizon.

include Form
val req : 'a nym -> opaque -> 'a

Use opt n v to extract v' if n is equivalent to the encapsulated runtime type, otherwise raises an exception (conventionally Type_error).

val opt : 'a nym -> opaque -> 'a option

Use opt n v to extract Some v' if n is equivalent to the encapsulated runtime type, otherwise returns None.

val eq : 'a nym -> 'b nym -> ('a, 'b) eq

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.

val ck : 'a nym -> opaque -> bool

Use ck n v to test whether n is equivalent to the encapsulated runtime type.

OCaml

Innovation. Community. Security.