.TH "Type.Id" 3 2024-02-29 OCamldoc "OCaml library"
.SH NAME
Type.Id \- Type identifiers.
.SH Module
Module   Type.Id
.SH Documentation
.sp
Module
.BI "Id"
 : 
.B sig end

.sp
Type identifiers\&.
.sp
A type identifier is a value that denotes a type\&. Given two type
identifiers, they can be tested for 
.ft B
Type\&.Id\&.provably_equal
.ft R
to
prove they denote the same type\&. Note that:
.sp
.sp
\-Unequal identifiers do not imply unequal types: a given type can be
denoted by more than one identifier\&.
.sp
\-Type identifiers can be marshalled, but they get a new, distinct,
identity on unmarshalling, so the equalities are lost\&.

See an 
.ft B
Type\&.Id\&.example
.ft R
of use\&.

.sp

.sp
.sp

.PP
.SS Type identifiers

.PP
.I type 
.B !'a
.I t 

.sp
The type for identifiers for type 
.ft B
\&'a
.ft R
\&.

.sp

.I val make 
: 
.B unit -> 'a t
.sp

.ft B
make ()
.ft R
is a new type identifier\&.

.sp

.I val uid 
: 
.B 'a t -> int
.sp

.ft B
uid id
.ft R
is a runtime unique identifier for 
.ft B
id
.ft R
\&.

.sp

.I val provably_equal 
: 
.B 'a t -> 'b t -> ('a, 'b) Type.eq option
.sp

.ft B
provably_equal i0 i1
.ft R
is 
.ft B
Some Equal
.ft R
if identifier 
.ft B
i0
.ft R
is equal
to 
.ft B
i1
.ft R
and 
.ft B
None
.ft R
otherwise\&.

.sp

.PP
.SS Example
.sp
The following shows how type identifiers can be used to
implement a simple heterogeneous key\-value dictionary\&. In contrast to
.ft B
Map
.ft R
values whose keys map to a single, homogeneous type of
values, this dictionary can associate a different type of value
to each key\&.
.EX
.ft B
.br
\&(** Heterogeneous dictionaries\&. *)
.br
\&module Dict : sig
.br
\&  type t
.br
\&  (** The type for dictionaries\&. *)
.br
\&
.br
\&  type \&'a key
.br
\&  (** The type for keys binding values of type [\&'a]\&. *)
.br
\&
.br
\&  val key : unit \-> \&'a key
.br
\&  (** [key ()] is a new dictionary key\&. *)
.br
\&
.br
\&  val empty : t
.br
\&  (** [empty] is the empty dictionary\&. *)
.br
\&
.br
\&  val add : \&'a key \-> \&'a \-> t \-> t
.br
\&  (** [add k v d] is [d] with [k] bound to [v]\&. *)
.br
\&
.br
\&  val remove : \&'a key \-> t \-> t
.br
\&  (** [remove k d] is [d] with the last binding of [k] removed\&. *)
.br
\&
.br
\&  val find : \&'a key \-> t \-> \&'a option
.br
\&  (** [find k d] is the binding of [k] in [d], if any\&. *)
.br
\&end = struct
.br
\&  type \&'a key = \&'a Type\&.Id\&.t
.br
\&  type binding = B : \&'a key * \&'a \-> binding
.br
\&  type t = (int * binding) list
.br
\&
.br
\&  let key () = Type\&.Id\&.make ()
.br
\&  let empty = []
.br
\&  let add k v d = (Type\&.Id\&.uid k, B (k, v)) :: d
.br
\&  let remove k d = List\&.remove_assoc (Type\&.Id\&.uid k) d
.br
\&  let find : type a\&. a key \-> t \-> a option = fun k d \->
.br
\&    match List\&.assoc_opt (Type\&.Id\&.uid k) d with
.br
\&    | None \-> None
.br
\&    | Some (B (k\&', v)) \->
.br
\&        match Type\&.Id\&.provably_equal k k\&' with
.br
\&        | Some Type\&.Equal \-> Some v
.br
\&        | None \-> assert false
.br
\&end
.br
\&
.ft R
.EE
.PP