Previous  Up  Next

Module Generic_core_ty

module Generic_core_ty: sig .. end
Type witnesses.

The type _ ty reflects type terms as value terms. We call such terms /type codes/. The GADT syntax allows us to constrain the type parameter of _ ty so that for any given type t, there is at most one value of type t ty, that value is the reflection of t.

For each type of arity n, corresponds a ty constructor of arity n whose arguments are themselves ty values reflecting the type parameters.


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 '_ 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 '_ 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 '_ ty +=
| Dynamic : dyn ty