Module Generic_core.Ty

module Ty: Generic_core_ty

Type witnesses.

Type Reflection

_ ty is extensible: when the user defines a new type ('a0,...'an) t, we add a homonymous constructor to _ty:

_ ty += T : 'a0 ty * ... * 'an ty -> ('a0,...'an) t ty

module T: sig .. end

Primitive and Standard Types The core generic library comes with the type reflection and introspection for all types in the standard library.

type 'a t = 'a T.ty

type 'a ty = 'a T.ty = ..

type '_ Generic_core_ty.ty +=

`\|`	`Any : 'a ty`
`\|`	`Int32 : int32 ty`
`\|`	`Int64 : int64 ty`
`\|`	`Nativeint : nativeint ty`
`\|`	`Lazy : 'a0 ty -> 'a0 Lazy.t ty`
`\|`	`Exn : exn ty`
`\|`	`Bool : bool ty`
`\|`	`Int : int ty`
`\|`	`Float : float ty`
`\|`	`Char : char ty`
`\|`	`Bytes : bytes ty`
`\|`	`String : string ty`
`\|`	`Option : 'a1 ty -> 'a1 option ty`
`\|`	`List : 'a2 ty -> 'a2 list ty`
`\|`	`Array : 'a3 ty -> 'a3 array ty`
`\|`	`Ref : 'a4 ty -> 'a4 Pervasives.ref ty`
`\|`	`Ty : 'a5 ty -> 'a5 ty ty`
`\|`	`Unit : unit ty`
`\|`	`Pair : 'a6 ty * 'b ty -> ('a6 * 'b) ty`
`\|`	`Triple : 'a7 ty * 'b0 ty * 'c ty -> ('a7 * 'b0 * 'c) ty`
`\|`	`Quadruple : 'a8 ty * 'b1 ty * 'c0 ty * 'd ty -> ('a8 * 'b1 * 'c0 * 'd) ty`
`\|`	`Quintuple : 'a9 ty * 'b2 ty * 'c1 ty * 'd0 ty * 'e ty -> ('a9 * 'b2 * 'c1 * 'd0 * 'e) ty`
`\|`	`Sextuple : 'a10 ty * 'b3 ty * 'c2 ty * 'd1 ty * 'e0 ty * 'f ty -> ('a10 * 'b3 * 'c2 * 'd1 * 'e0 * 'f) ty`
`\|`	`Septuple : 'a11 ty * 'b4 ty * 'c3 ty * 'd2 ty * 'e1 ty * 'f0 ty * 'g ty -> ('a11 * 'b4 * 'c3 * 'd2 * 'e1 * 'f0 * 'g) ty`
`\|`	`Octuple : 'a12 ty * 'b5 ty * 'c4 ty * 'd3 ty * 'e2 ty * 'f1 ty * 'g0 ty * 'h ty -> ('a12 * 'b5 * 'c4 * 'd3 * 'e2 * 'f1 * 'g0 * 'h) ty`
`\|`	`Nonuple : 'a13 ty * 'b6 ty * 'c5 ty * 'd4 ty * 'e3 ty * 'f2 ty * 'g1 ty * 'h0 ty * 'i ty -> ('a13 * 'b6 * 'c5 * 'd4 * 'e3 * 'f2 * 'g1 * 'h0 * 'i) ty`
`\|`	`Decuple : 'a14 ty * 'b7 ty * 'c6 ty * 'd5 ty * 'e4 ty * 'f3 ty * 'g2 ty * 'h1 ty * 'i0 ty * 'j ty -> ('a14 * 'b7 * 'c6 * 'd5 * 'e4 * 'f3 * 'g2 * 'h1 * 'i0 * 'j) ty`
`\|`	`Fun : 'a15 ty * 'b8 ty -> ('a15 -> 'b8) ty`

Re-export of T.ty constructors

Forgetting the index

GADT allow us to forget the type index using existential quantification. The type ty' is the union of all 'a ty for all 'a.

type ty' =

`\|`	`E : 'a ty -> ty'`

Equality on types of possibly different indices

Using the index-less ty' we may now compare 'a ty and 'b ty values using the generic equality primitive.

val eq : 'a ty -> 'b ty -> bool

eq x y == E x = E y

val neq : 'a ty -> 'b ty -> bool

neq x y == not (eq x y)

Functions for constraining a type

val with_type : 'a ty -> 'a -> 'a

with_type is used to help the type-checker fix the type of a value to the index of ='a ty=.

Type Patterns

The type synonym 'a pat is meant to mark the contexts where patterns are expected rather than type codes. Any type code is also a type pattern, but in addition there is a wildcard pattern Generic_core_ty.Any which is not a type code.

type 'a pat = 'a ty

Wildcard Pattern

The constructor Any is a type pattern that can match any type. It is not valid in contexts where a type code is expected: use only in contexts where a pattern is expected.

val any : 'a pat

any == Any

Patterns Functions

Patterns for common type constructors are given.

val pair : ('a * 'b) pat

pair == Pair (Any,Any)

val triple : ('a * 'b * 'c) pat

triple == Triple (Any,Any,Any)

val quadruple : ('a * 'b * 'c * 'd) pat

val quintuple : ('a * 'b * 'c * 'd * 'e) pat

val sextuple : ('a * 'b * 'c * 'd * 'e * 'f) pat

val septuple : ('a * 'b * 'c * 'd * 'e * 'f * 'g) pat

val octuple : ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) pat

val nonuple : ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) pat

val decuple : ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) pat

val option : 'a option pat

option == Option Any

val list : 'a list pat

list == List Any

val array : 'a array pat

array == Array Any

Constructor Pattern

conpat computes the constructor pattern of a type code: it replaces all the parameters with Any.

For instance:

conpat Int == Int
conpat (List Int) == List Any
conpat (Pair (String, List Int)) == Pair (Any, Any)

val conpat : 'a ty -> 'a pat

conpat computes a constructor pattern:

conpat (Pair (Int, List String)) == Pair (Any,Any)

val conpat' : ty' -> ty'

conpat' is the ty' version of conpat, working on index-less type codes.

conpat' (E t) == E (conpat t)

Dynamic values

Dynamically typed languages have a notion of runtime types which we can emulate by packaging type witnesses with the values.

module Typed: sig .. end

Values tagged with their type witness.

type 'a typed = 'a Typed.typed

type '_ Generic_core_ty.ty +=

`\|`	`Typed : 'a ty -> 'a typed ty`

module Dynamic: sig .. end

Dynamic values are the union of all types.

type dynamic = Dynamic.dynamic =

`\|`	`Dyn : 'a typed -> dynamic`

type dyn = dynamic

type '_ Generic_core_ty.ty +=

`\|`	`Dynamic : dyn ty`