package orsetto

  1. Overview
  2. Docs

Module Cf_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.

Runtime Type Indicators
type _ nym = ..

The extensible generalized algebraic data type of type nyms.

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.

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 opaque = private
  1. | Witness : 'a * 'a nym -> opaque

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

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 += private
  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

The equivalence horizon of type nyms defined above.

module type Form = sig ... end

The signature of modules for extracting opaque values within a given type equivalence horizon.

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 ck : 'a nym -> opaque -> bool

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

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