Type(3) | OCaml library | Type(3) |

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

2024-02-29 | OCamldoc |