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
|
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="generator" content="AsciiDoc 8.6.8">
<title>AdmitsEquality</title>
<link rel="stylesheet" href="./asciidoc.css" type="text/css">
<link rel="stylesheet" href="./pygments.css" type="text/css">
<script type="text/javascript" src="./asciidoc.js"></script>
<script type="text/javascript">
/*<![CDATA[*/
asciidoc.install();
/*]]>*/
</script>
<link rel="stylesheet" href="./mlton.css" type="text/css"/>
</head>
<body class="article">
<div id="banner">
<div id="banner-home">
<a href="./Home">MLton 20130715</a>
</div>
</div>
<div id="header">
<h1>AdmitsEquality</h1>
</div>
<div id="content">
<div id="preamble">
<div class="sectionbody">
<div class="paragraph"><p>A <a href="TypeConstructor">TypeConstructor</a> admits equality if whenever it is applied to
equality types, the result is an <a href="EqualityType">EqualityType</a>. This notion enables
one to determine whether a type constructor application yields an
equality type solely from the application, without looking at the
definition of the type constructor. It helps to ensure that
<a href="PolymorphicEquality">PolymorphicEquality</a> is only applied to sensible values.</p></div>
<div class="paragraph"><p>The definition of admits equality depends on whether the type
constructor was declared by a <span class="monospaced">type</span> definition or a
<span class="monospaced">datatype</span> declaration.</p></div>
</div>
</div>
<div class="sect1">
<h2 id="_type_definitions">Type definitions</h2>
<div class="sectionbody">
<div class="paragraph"><p>For type definition</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="p">(</span><span class="n">'a1</span><span class="p">,</span><span class="w"> </span><span class="p">...,</span><span class="w"> </span><span class="n">'an</span><span class="p">)</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="p">...</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality if the right-hand side of the
definition is an equality type after replacing <span class="monospaced">'a1</span>, …,
<span class="monospaced">'an</span> by equality types (it doesn’t matter which equality types
are chosen).</p></div>
<div class="paragraph"><p>For a nullary type definition, this amounts to the right-hand side
being an equality type. For example, after the definition</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">int</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality because <span class="monospaced">bool * int</span> is
an equality type. On the other hand, after the definition</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">int</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">real</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>type constructor <span class="monospaced">t</span> does not admit equality, because <span class="monospaced">real</span>
is not an equality type.</p></div>
<div class="paragraph"><p>For another example, after the definition</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality because <span class="monospaced">bool * int</span>
is an equality type (we could have chosen any equality type other than
<span class="monospaced">int</span>).</p></div>
<div class="paragraph"><p>On the other hand, after the definition</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">real</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>type constructor <span class="monospaced">t</span> does not admit equality because
<span class="monospaced">real * int</span> is not equality type.</p></div>
<div class="paragraph"><p>We can check that a type constructor admits equality using an
<span class="monospaced">eqtype</span> specification.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Ok</span><span class="p">:</span><span class="w"> </span><span class="k">sig</span><span class="w"> </span><span class="k">eqtype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
<span class="w"> </span><span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Bad</span><span class="p">:</span><span class="w"> </span><span class="k">sig</span><span class="w"> </span><span class="k">eqtype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">real</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">int</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
<span class="w"> </span><span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>On <span class="monospaced">structure Bad</span>, MLton reports the following error.</p></div>
<div class="listingblock">
<div class="content monospaced">
<pre>Type t admits equality in signature but not in structure.
not equality: [real] * _ * _</pre>
</div></div>
<div class="paragraph"><p>The <span class="monospaced">not equality</span> section provides an explanation of why the type
did not admit equality, highlighting the problematic component
(<span class="monospaced">real</span>).</p></div>
</div>
</div>
<div class="sect1">
<h2 id="_datatype_declarations">Datatype declarations</h2>
<div class="sectionbody">
<div class="paragraph"><p>For a type constructor declared by a datatype declaration to admit
equality, every <a href="Variant">variant</a> of the datatype must admit equality. For
example, the following datatype admits equality because <span class="monospaced">bool</span> and
<span class="monospaced">char * int</span> are equality types.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">char</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">int</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>Nullary constructors trivially admit equality, so that the following
datatype admits equality.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">C</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>For a parameterized datatype constructor to admit equality, we
consider each <a href="Variant">variant</a> as a type definition, and require that the
definition admit equality. For example, for the datatype</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>the type definitions</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">tA</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
<span class="k">type</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">tB</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>both admit equality. Thus, type constructor <span class="monospaced">t</span> admits equality.</p></div>
<div class="paragraph"><p>On the other hand, the following datatype does not admit equality.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">real</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>As with type definitions, we can check using an <span class="monospaced">eqtype</span>
specification.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Bad</span><span class="p">:</span><span class="w"> </span><span class="k">sig</span><span class="w"> </span><span class="k">eqtype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w"> </span><span class="k">datatype</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">bool</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">real</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">'a</span><span class="w"></span>
<span class="w"> </span><span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>MLton reports the following error.</p></div>
<div class="listingblock">
<div class="content monospaced">
<pre>Type t admits equality in signature but not in structure.
not equality: B of [real] * _</pre>
</div></div>
<div class="paragraph"><p>MLton indicates the problematic constructor (<span class="monospaced">B</span>), as well as
the problematic component of the constructor’s argument.</p></div>
<div class="sect2">
<h3 id="_recursive_datatypes">Recursive datatypes</h3>
<div class="paragraph"><p>A recursive datatype like</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">int</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>introduces a new problem, since in order to decide whether <span class="monospaced">t</span>
admits equality, we need to know for the <span class="monospaced">B</span> <a href="Variant">variant</a> whether
<span class="monospaced">t</span> admits equality. The <a href="DefinitionOfStandardML">Definition</a>
answers this question by requiring a type constructor to admit
equality if it is consistent to do so. So, in our above example, if
we assume that <span class="monospaced">t</span> admits equality, then the <a href="Variant">variant</a>
<span class="monospaced">B of int * t</span> admits equality. Then, since the <span class="monospaced">A</span> <a href="Variant">variant</a>
trivially admits equality, so does the type constructor <span class="monospaced">t</span>.
Thus, it was consistent to assume that <span class="monospaced">t</span> admits equality, and
so, <span class="monospaced">t</span> does admit equality.</p></div>
<div class="paragraph"><p>On the other hand, in the following declaration</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">real</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>if we assume that <span class="monospaced">t</span> admits equality, then the <span class="monospaced">B</span> <a href="Variant">variant</a>
does not admit equality. Hence, the type constructor <span class="monospaced">t</span> does not
admit equality, and our assumption was inconsistent. Hence, <span class="monospaced">t</span>
does not admit equality.</p></div>
<div class="paragraph"><p>The same kind of reasoning applies to mutually recursive datatypes as
well. For example, the following defines both <span class="monospaced">t</span> and <span class="monospaced">u</span> to
admit equality.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">u</span><span class="w"></span>
<span class="k">and</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">D</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>But the following defines neither <span class="monospaced">t</span> nor <span class="monospaced">u</span> to admit
equality.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">real</span><span class="w"></span>
<span class="k">and</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">D</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>As always, we can check whether a type admits equality using an
<span class="monospaced">eqtype</span> specification.</p></div>
<div class="listingblock">
<div class="content"><div class="highlight"><pre><span class="k">structure</span><span class="w"> </span><span class="n">Bad</span><span class="p">:</span><span class="w"> </span><span class="k">sig</span><span class="w"> </span><span class="k">eqtype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="k">eqtype</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="k">end</span><span class="w"> </span><span class="p">=</span><span class="w"></span>
<span class="w"> </span><span class="k">struct</span><span class="w"></span>
<span class="w"> </span><span class="k">datatype</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">*</span><span class="w"> </span><span class="n">real</span><span class="w"></span>
<span class="w"> </span><span class="k">and</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="p">|</span><span class="w"> </span><span class="n">D</span><span class="w"> </span><span class="k">of</span><span class="w"> </span><span class="n">t</span><span class="w"></span>
<span class="w"> </span><span class="k">end</span><span class="w"></span>
</pre></div></div></div>
<div class="paragraph"><p>MLton reports the following error.</p></div>
<div class="listingblock">
<div class="content monospaced">
<pre>Error: z.sml 1.16.
Type t admits equality in signature but not in structure.
not equality: B of [u] * [real]
Error: z.sml 1.16.
Type u admits equality in signature but not in structure.
not equality: D of [t]</pre>
</div></div>
</div>
</div>
</div>
</div>
<div id="footnotes"><hr></div>
<div id="footer">
<div id="footer-text">
</div>
<div id="footer-badges">
</div>
</div>
</body>
</html>
|
