oracular (3) Type.3o.gz

NAME

       Type - Type introspection.

Module

       Module   Type

Documentation

       Module Type
        : sig end

       Type introspection.

       Since 5.1

   Type equality witness
       type (_, _) eq =
        | Equal : ('a, 'a) eq

       The  purpose  of  eq  is to represent type equalities that may not otherwise be known by the type checker
       (e.g. because they may depend on dynamic data).

       A value of type (a, b) eq represents the fact that types a and b are equal.

       If one has a value eq : (a, b) eq that proves types a and b are equal, one can use it to convert a  value
       of type a to a value of type b by pattern matching on Equal :
             let cast (type a) (type b) (Equal : (a, b) Type.eq) (a : a) : b = a

       At runtime, this function simply returns its second argument unchanged.

   Type identifiers
       module Id : sig end

       Type identifiers.

       A  type  identifier  is  a  value that denotes a type. Given two type identifiers, they can be tested for
       Type.Id.provably_equal to prove they denote the same type. Note that:

       -Unequal identifiers do not imply unequal types: a given type can be denoted by more than one identifier.

       -Type identifiers can be marshalled, but they get a new, distinct,  identity  on  unmarshalling,  so  the
       equalities are lost.

       See an Type.Id.example of use.