Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | UniversalType |
2 | ============= | |
3 | ||
4 | A universal type is a type into which all other types can be embedded. | |
5 | Here's a <:StandardML:Standard ML> signature for a universal type. | |
6 | ||
7 | [source,sml] | |
8 | ---- | |
9 | signature UNIVERSAL_TYPE = | |
10 | sig | |
11 | type t | |
12 | ||
13 | val embed: unit -> ('a -> t) * (t -> 'a option) | |
14 | end | |
15 | ---- | |
16 | ||
17 | The idea is that `type t` is the universal type and that each call to | |
18 | `embed` returns a new pair of functions `(inject, project)`, where | |
19 | `inject` embeds a value into the universal type and `project` extracts | |
20 | the value from the universal type. A pair `(inject, project)` | |
21 | returned by `embed` works together in that `project u` will return | |
22 | `SOME v` if and only if `u` was created by `inject v`. If `u` was | |
23 | created by a different function `inject'`, then `project` returns | |
24 | `NONE`. | |
25 | ||
26 | Here's an example embedding integers and reals into a universal type. | |
27 | ||
28 | [source,sml] | |
29 | ---- | |
30 | functor Test (U: UNIVERSAL_TYPE): sig end = | |
31 | struct | |
32 | val (intIn: int -> U.t, intOut) = U.embed () | |
33 | val r: U.t ref = ref (intIn 13) | |
34 | val s1 = | |
35 | case intOut (!r) of | |
36 | NONE => "NONE" | |
37 | | SOME i => Int.toString i | |
38 | val (realIn: real -> U.t, realOut) = U.embed () | |
39 | val () = r := realIn 13.0 | |
40 | val s2 = | |
41 | case intOut (!r) of | |
42 | NONE => "NONE" | |
43 | | SOME i => Int.toString i | |
44 | val s3 = | |
45 | case realOut (!r) of | |
46 | NONE => "NONE" | |
47 | | SOME x => Real.toString x | |
48 | val () = print (concat [s1, " ", s2, " ", s3, "\n"]) | |
49 | end | |
50 | ---- | |
51 | ||
52 | Applying `Test` to an appropriate implementation will print | |
53 | ||
54 | ---- | |
55 | 13 NONE 13.0 | |
56 | ---- | |
57 | ||
58 | Note that two different calls to embed on the same type return | |
59 | different embeddings. | |
60 | ||
61 | Standard ML does not have explicit support for universal types; | |
62 | however, there are at least two ways to implement them. | |
63 | ||
64 | ||
65 | == Implementation Using Exceptions == | |
66 | ||
67 | While the intended use of SML exceptions is for exception handling, an | |
68 | accidental feature of their design is that the `exn` type is a | |
69 | universal type. The implementation relies on being able to declare | |
70 | exceptions locally to a function and on the fact that exceptions are | |
71 | <:GenerativeException:generative>. | |
72 | ||
73 | [source,sml] | |
74 | ---- | |
75 | structure U:> UNIVERSAL_TYPE = | |
76 | struct | |
77 | type t = exn | |
78 | ||
79 | fun 'a embed () = | |
80 | let | |
81 | exception E of 'a | |
82 | fun project (e: t): 'a option = | |
83 | case e of | |
84 | E a => SOME a | |
85 | | _ => NONE | |
86 | in | |
87 | (E, project) | |
88 | end | |
89 | end | |
90 | ---- | |
91 | ||
92 | ||
93 | == Implementation Using Functions and References == | |
94 | ||
95 | [source,sml] | |
96 | ---- | |
97 | structure U:> UNIVERSAL_TYPE = | |
98 | struct | |
99 | datatype t = T of {clear: unit -> unit, | |
100 | store: unit -> unit} | |
101 | ||
102 | fun 'a embed () = | |
103 | let | |
104 | val r: 'a option ref = ref NONE | |
105 | fun inject (a: 'a): t = | |
106 | T {clear = fn () => r := NONE, | |
107 | store = fn () => r := SOME a} | |
108 | fun project (T {clear, store}): 'a option = | |
109 | let | |
110 | val () = store () | |
111 | val res = !r | |
112 | val () = clear () | |
113 | in | |
114 | res | |
115 | end | |
116 | in | |
117 | (inject, project) | |
118 | end | |
119 | end | |
120 | ---- | |
121 | ||
122 | Note that due to the use of a shared ref cell, the above | |
123 | implementation is not thread safe. | |
124 | ||
125 | One could try to simplify the above implementation by eliminating the | |
126 | `clear` function, making `type t = unit -> unit`. | |
127 | ||
128 | [source,sml] | |
129 | ---- | |
130 | structure U:> UNIVERSAL_TYPE = | |
131 | struct | |
132 | type t = unit -> unit | |
133 | ||
134 | fun 'a embed () = | |
135 | let | |
136 | val r: 'a option ref = ref NONE | |
137 | fun inject (a: 'a): t = fn () => r := SOME a | |
138 | fun project (f: t): 'a option = (r := NONE; f (); !r) | |
139 | in | |
140 | (inject, project) | |
141 | end | |
142 | end | |
143 | ---- | |
144 | ||
145 | While correct, this approach keeps the contents of the ref cell alive | |
146 | longer than necessary, which could cause a space leak. The problem is | |
147 | in `project`, where the call to `f` stores some value in some ref cell | |
148 | `r'`. Perhaps `r'` is the same ref cell as `r`, but perhaps not. If | |
149 | we do not clear `r'` before returning from `project`, then `r'` will | |
150 | keep the value alive, even though it is useless. | |
151 | ||
152 | ||
153 | == Also see == | |
154 | ||
155 | * <:PropertyList:>: Lisp-style property lists implemented with a universal type |