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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<meta name="robots" content="index,nofollow">
<title>EqualityTypeVariable - MLton Standard ML Compiler (SML Compiler)</title>
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="all" href="common.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="screen" href="screen.css">
<link rel="stylesheet" type="text/css" charset="iso-8859-1" media="print" href="print.css">
<link rel="Start" href="Home">
</head>
<body lang="en" dir="ltr">
<script src="http://www.google-analytics.com/urchin.js" type="text/javascript">
</script>
<script type="text/javascript">
_uacct = "UA-833377-1";
urchinTracker();
</script>
<table bgcolor = lightblue cellspacing = 0 style = "border: 0px;" width = 100%>
<tr>
<td style = "
border: 0px;
color: darkblue;
font-size: 150%;
text-align: left;">
<a class = mltona href="Home">MLton MLTONWIKIVERSION</a>
<td style = "
border: 0px;
font-size: 150%;
text-align: center;
width: 50%;">
EqualityTypeVariable
<td style = "
border: 0px;
text-align: right;">
<table cellspacing = 0 style = "border: 0px">
<tr style = "vertical-align: middle;">
</table>
<tr style = "background-color: white;">
<td colspan = 3
style = "
border: 0px;
font-size:70%;
text-align: right;">
<a href = "Home">Home</a>
<a href = "TitleIndex">Index</a>
</table>
<div id="content" lang="en" dir="ltr">
An equality type variable is a type variable that starts with two or more primes, as in <tt>''a</tt> or <tt>''b</tt>. The canonical use of equality type variables is in specifying the type of the <a href="PolymorphicEquality">PolymorphicEquality</a> function, which is <tt>''a * ''a -> bool</tt>. Equality type variables ensure that polymorphic equality is only used on <a href="EqualityType">equality types</a>, by requiring that at every use of a polymorphic value, equality type variables are instantiated by equality types. <p>
For example, the following program is type correct because polymorphic equality is applied to variables of type <tt>''a</tt>.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">fun</FONT></B> f (x: ''a, y: ''a): bool = x = y
</PRE>
<p>
</p>
<p>
On the other hand, the following program is not type correct, because polymorphic equality is applied to variables of type <tt>'a</tt>, which is not an equality type.
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">fun</FONT></B> f (x: 'a, y: 'a): bool = x = y
</PRE>
<p>
</p>
<p>
MLton reports the following error, indicating that polymorphic equality expects equality types, but didn't get them.
</p>
<pre>Error: z.sml 1.32.
Function applied to incorrect argument.
expects: [<equality>] * [<equality>]
but got: [<non-equality>] * [<non-equality>]
in: = (x, y)
</pre><p>
As an example of using such a function that requires equality types, suppose that <tt>f</tt> has polymorphic type <tt>''a -> unit</tt>. Then, <tt>f 13</tt> is type correct because <tt>int</tt> is an equality type. On the other hand, <tt>f 13.0</tt> and <tt>f (fn x => x)</tt> are not type correct, because <tt>real</tt> and arrow types are not equality types. We can test these facts with the following short programs. First, we verify that such an <tt>f</tt> can be applied to integers.
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Ok (<B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit): <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#0000FF">end</FONT></B> =
<B><FONT COLOR="#0000FF">struct</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> () = f <B><FONT COLOR="#5F9EA0">13</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> () = f <B><FONT COLOR="#5F9EA0">14</FONT></B>
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
<p>
</p>
<p>
We can do better, and verify that such an <tt>f</tt> can be applied to any integer.
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Ok (<B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit): <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#0000FF">end</FONT></B> =
<B><FONT COLOR="#0000FF">struct</FONT></B>
<B><FONT COLOR="#A020F0">fun</FONT></B> g (x: int) = f x
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
<p>
</p>
<p>
Even better, we don't need to introduce a dummy function name; we can use a type constraint.
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Ok (<B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit): <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#0000FF">end</FONT></B> =
<B><FONT COLOR="#0000FF">struct</FONT></B>
<B><FONT COLOR="#A020F0">val</FONT></B> _ = f: int -> unit
<B><FONT COLOR="#0000FF">end</FONT></B>
</PRE>
<p>
</p>
<p>
Even better, we can use a signature constraint.
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Ok (S: <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit <B><FONT COLOR="#0000FF">end</FONT></B>):
<B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: int -> unit <B><FONT COLOR="#0000FF">end</FONT></B> = S
</PRE>
<p>
</p>
<p>
This functor concisely verifies that a function of polymorphic type <tt>''a -> unit</tt> can be safely used as a function of type <tt>int -> unit</tt>.
</p>
<p>
As above, we can verify that such an <tt>f</tt> can not be used at non equality types.
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Bad (S: <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit <B><FONT COLOR="#0000FF">end</FONT></B>):
<B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: real -> unit <B><FONT COLOR="#0000FF">end</FONT></B> = S
</PRE>
<p>
</p>
<pre class=code>
<B><FONT COLOR="#0000FF">functor</FONT></B> Bad (S: <B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: ''a -> unit <B><FONT COLOR="#0000FF">end</FONT></B>):
<B><FONT COLOR="#0000FF">sig</FONT></B> <B><FONT COLOR="#A020F0">val</FONT></B> f: ('a -> 'a) -> unit <B><FONT COLOR="#0000FF">end</FONT></B> = S
</PRE>
<p>
</p>
<p>
For each of these programs, MLton reports the following error.
</p>
<pre>Error: z.sml 2.4.
Variable type in structure disagrees with signature.
variable: f
structure: [<equality>] -> _
signature: [<non-equality>] -> _
</pre><h2 id="head-298e9694028673faa9fcbabf774bc23e4d2fbbe0">Equality type variables in type and datatype declarations</h2>
<p>
Equality type variables can be used in type and datatype declarations; however they play no special role. For example,
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> 'a * int
</FONT></B></PRE>
<p>
</p>
<p>
is completely identical to
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">type</FONT></B><B><FONT COLOR="#228B22"> ''a t </FONT></B>=<B><FONT COLOR="#228B22"> ''a * int
</FONT></B></PRE>
<p>
</p>
<p>
In particular, such a definition does <em>not</em> require that <tt>t</tt> only be applied to equality types.
</p>
<p>
Similarly,
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> 'a t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">A</FONT> </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">B</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> 'a
</FONT></B></PRE>
<p>
</p>
<p>
is completely identical to
</p>
<pre class=code>
<B><FONT COLOR="#A020F0">datatype</FONT></B><B><FONT COLOR="#228B22"> ''a t </FONT></B>=<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">A</FONT> </FONT></B>|<B><FONT COLOR="#228B22"> <FONT COLOR="#B8860B">B</FONT> <B><FONT COLOR="#A020F0">of</FONT></B> ''a
</FONT></B></PRE>
<p>
</p>
</div>
<p>
<hr>
Last edited on 2005-12-01 04:00:38 by <span title="ppp-71-139-183-221.dsl.snfc21.pacbell.net"><a href="StephenWeeks">StephenWeeks</a></span>.
</body></html>
|
