<!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>
distrib
>
Fedora
>
18
>
x86_64
>
media
>
updates
>
by-pkgid
>
171636fb720078ab07822dd4a76f1938
>
files
>
2249
