1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* The OCaml programmers *)
(* *)
(* Copyright 2022 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(** Type introspection.
@since 5.1 *)
(** {1:witness 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.
*)
(** {1:identifiers Type identifiers} *)
(** Type identifiers.
A type identifier is a value that denotes a type. Given two type
identifiers, they can be tested for {{!Id.provably_equal}equality} 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 {{!Id.example}example} of use. *)
module Id : sig
(** {1:ids Type identifiers} *)
type !'a t
(** The type for identifiers for type ['a]. *)
val make : unit -> 'a t
(** [make ()] is a new type identifier. *)
val uid : 'a t -> int
(** [uid id] is a runtime unique identifier for [id]. *)
val provably_equal : 'a t -> 'b t -> ('a, 'b) eq option
(** [provably_equal i0 i1] is [Some Equal] if identifier [i0] is equal
to [i1] and [None] otherwise. *)
(** {1:example Example}
The following shows how type identifiers can be used to
implement a simple heterogeneous key-value dictionary. In contrast to
{!Stdlib.Map} values whose keys map to a single, homogeneous type of
values, this dictionary can associate a different type of value
to each key.
{[
(** Heterogeneous dictionaries. *)
module Dict : sig
type t
(** The type for dictionaries. *)
type 'a key
(** The type for keys binding values of type ['a]. *)
val key : unit -> 'a key
(** [key ()] is a new dictionary key. *)
val empty : t
(** [empty] is the empty dictionary. *)
val add : 'a key -> 'a -> t -> t
(** [add k v d] is [d] with [k] bound to [v]. *)
val remove : 'a key -> t -> t
(** [remove k d] is [d] with the last binding of [k] removed. *)
val find : 'a key -> t -> 'a option
(** [find k d] is the binding of [k] in [d], if any. *)
end = struct
type 'a key = 'a Type.Id.t
type binding = B : 'a key * 'a -> binding
type t = (int * binding) list
let key () = Type.Id.make ()
let empty = []
let add k v d = (Type.Id.uid k, B (k, v)) :: d
let remove k d = List.remove_assoc (Type.Id.uid k) d
let find : type a. a key -> t -> a option = fun k d ->
match List.assoc_opt (Type.Id.uid k) d with
| None -> None
| Some (B (k', v)) ->
match Type.Id.provably_equal k k' with
| Some Type.Equal -> Some v
| None -> assert false
end
]}
*)
end
|
