doc/guide/localhost/AdmitsEquality

   1 <!DOCTYPE html>
   2 <html lang="en">
   3 <head>
   4 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
   5 <meta name="generator" content="AsciiDoc 8.6.9">
   6 <title>AdmitsEquality</title>
   7 <link rel="stylesheet" href="./asciidoc.css" type="text/css">
   8 <link rel="stylesheet" href="./pygments.css" type="text/css">
   9
  10
  11 <script type="text/javascript" src="./asciidoc.js"></script>
  12 <script type="text/javascript">
  13 /*<![CDATA[*/
  14 asciidoc.install();
  15 /*]]>*/
  16 </script>
  17 <link rel="stylesheet" href="./mlton.css" type="text/css">
  18 </head>
  19 <body class="article">
  20 <div id="banner">
  21 <div id="banner-home">
  22 <a href="./Home">MLton 20180207</a>
  23 </div>
  24 </div>
  25 <div id="header">
  26 <h1>AdmitsEquality</h1>
  27 </div>
  28 <div id="content">
  29 <div id="preamble">
  30 <div class="sectionbody">
  31 <div class="paragraph"><p>A <a href="TypeConstructor">TypeConstructor</a> admits equality if whenever it is applied to
  32 equality types, the result is an <a href="EqualityType">EqualityType</a>.  This notion enables
  33 one to determine whether a type constructor application yields an
  34 equality type solely from the application, without looking at the
  35 definition of the type constructor.  It helps to ensure that
  36 <a href="PolymorphicEquality">PolymorphicEquality</a> is only applied to sensible values.</p></div>
  37 <div class="paragraph"><p>The definition of admits equality depends on whether the type
  38 constructor was declared by a <span class="monospaced">type</span> definition or a
  39 <span class="monospaced">datatype</span> declaration.</p></div>
  40 </div>
  41 </div>
  42 <div class="sect1">
  43 <h2 id="_type_definitions">Type definitions</h2>
  44 <div class="sectionbody">
  45 <div class="paragraph"><p>For type definition</p></div>
  46 <div class="listingblock">
  47 <div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="p">(</span><span class="n">&#39;a1</span><span class="p">,</span><span class="w"> </span><span class="p">...,</span><span class="w"> </span><span class="n">&#39;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>
  48 </pre></div></div></div>
  49 <div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality if the right-hand side of the
  50 definition is an equality type after replacing <span class="monospaced">'a1</span>, &#8230;,
  51 <span class="monospaced">'an</span> by equality types (it doesn&#8217;t matter which equality types
  52 are chosen).</p></div>
  53 <div class="paragraph"><p>For a nullary type definition, this amounts to the right-hand side
  54 being an equality type.  For example, after the definition</p></div>
  55 <div class="listingblock">
  56 <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>
  57 </pre></div></div></div>
  58 <div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality because <span class="monospaced">bool * int</span> is
  59 an equality type.   On the other hand, after the definition</p></div>
  60 <div class="listingblock">
  61 <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>
  62 </pre></div></div></div>
  63 <div class="paragraph"><p>type constructor <span class="monospaced">t</span> does not admit equality, because <span class="monospaced">real</span>
  64 is not an equality type.</p></div>
  65 <div class="paragraph"><p>For another example, after the definition</p></div>
  66 <div class="listingblock">
  67 <div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
  68 </pre></div></div></div>
  69 <div class="paragraph"><p>type constructor <span class="monospaced">t</span> admits equality because <span class="monospaced">bool * int</span>
  70 is an equality type (we could have chosen any equality type other than
  71 <span class="monospaced">int</span>).</p></div>
  72 <div class="paragraph"><p>On the other hand, after the definition</p></div>
  73 <div class="listingblock">
  74 <div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
  75 </pre></div></div></div>
  76 <div class="paragraph"><p>type constructor <span class="monospaced">t</span> does not admit equality because
  77 <span class="monospaced">real * int</span> is not equality type.</p></div>
  78 <div class="paragraph"><p>We can check that a type constructor admits equality using an
  79 <span class="monospaced">eqtype</span> specification.</p></div>
  80 <div class="listingblock">
  81 <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">&#39;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>
  82 <span class="w">   </span><span class="k">struct</span><span class="w"></span>
  83 <span class="w">      </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
  84 <span class="w">   </span><span class="k">end</span><span class="w"></span>
  85 </pre></div></div></div>
  86 <div class="listingblock">
  87 <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">&#39;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>
  88 <span class="w">   </span><span class="k">struct</span><span class="w"></span>
  89 <span class="w">      </span><span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
  90 <span class="w">   </span><span class="k">end</span><span class="w"></span>
  91 </pre></div></div></div>
  92 <div class="paragraph"><p>On <span class="monospaced">structure Bad</span>, MLton reports the following error.</p></div>
  93 <div class="listingblock">
  94 <div class="content monospaced">
  95 <pre>Error: z.sml 1.16-1.34.
  96   Type in structure disagrees with signature (admits equality): t.
  97     structure: type 'a t = [real] * _ * _
  98     defn at: z.sml 3.15-3.15
  99     signature: [eqtype] 'a t
 100     spec at: z.sml 1.30-1.30</pre>
 101 </div></div>
 102 <div class="paragraph"><p>The <span class="monospaced">structure:</span> section provides an explanation of why the type
 103 did not admit equality, highlighting the problematic component
 104 (<span class="monospaced">real</span>).</p></div>
 105 </div>
 106 </div>
 107 <div class="sect1">
 108 <h2 id="_datatype_declarations">Datatype declarations</h2>
 109 <div class="sectionbody">
 110 <div class="paragraph"><p>For a type constructor declared by a datatype declaration to admit
 111 equality, every <a href="Variant">variant</a> of the datatype must admit equality.  For
 112 example, the following datatype admits equality because <span class="monospaced">bool</span> and
 113 <span class="monospaced">char * int</span> are equality types.</p></div>
 114 <div class="listingblock">
 115 <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>
 116 </pre></div></div></div>
 117 <div class="paragraph"><p>Nullary constructors trivially admit equality, so that the following
 118 datatype admits equality.</p></div>
 119 <div class="listingblock">
 120 <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>
 121 </pre></div></div></div>
 122 <div class="paragraph"><p>For a parameterized datatype constructor to admit equality, we
 123 consider each <a href="Variant">variant</a> as a type definition, and require that the
 124 definition admit equality.  For example, for the datatype</p></div>
 125 <div class="listingblock">
 126 <div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">&#39;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">&#39;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">&#39;a</span><span class="w"></span>
 127 </pre></div></div></div>
 128 <div class="paragraph"><p>the type definitions</p></div>
 129 <div class="listingblock">
 130 <div class="content"><div class="highlight"><pre><span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
 131 <span class="k">type</span><span class="w"> </span><span class="n">&#39;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">&#39;a</span><span class="w"></span>
 132 </pre></div></div></div>
 133 <div class="paragraph"><p>both admit equality.  Thus, type constructor <span class="monospaced">t</span> admits equality.</p></div>
 134 <div class="paragraph"><p>On the other hand, the following datatype does not admit equality.</p></div>
 135 <div class="listingblock">
 136 <div class="content"><div class="highlight"><pre><span class="k">datatype</span><span class="w"> </span><span class="n">&#39;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">&#39;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">&#39;a</span><span class="w"></span>
 137 </pre></div></div></div>
 138 <div class="paragraph"><p>As with type definitions, we can check using an <span class="monospaced">eqtype</span>
 139 specification.</p></div>
 140 <div class="listingblock">
 141 <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">&#39;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>
 142 <span class="w">   </span><span class="k">struct</span><span class="w"></span>
 143 <span class="w">      </span><span class="k">datatype</span><span class="w"> </span><span class="n">&#39;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">&#39;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">&#39;a</span><span class="w"></span>
 144 <span class="w">   </span><span class="k">end</span><span class="w"></span>
 145 </pre></div></div></div>
 146 <div class="paragraph"><p>MLton reports the following error.</p></div>
 147 <div class="listingblock">
 148 <div class="content monospaced">
 149 <pre>Error: z.sml 1.16-1.34.
 150   Type in structure disagrees with signature (admits equality): t.
 151     structure: datatype 'a t = B of [real] * _ | ...
 152     defn at: z.sml 3.19-3.19
 153     signature: [eqtype] 'a t
 154     spec at: z.sml 1.30-1.30</pre>
 155 </div></div>
 156 <div class="paragraph"><p>MLton indicates the problematic constructor (<span class="monospaced">B</span>), as well as
 157 the problematic component of the constructor&#8217;s argument.</p></div>
 158 <div class="sect2">
 159 <h3 id="_recursive_datatypes">Recursive datatypes</h3>
 160 <div class="paragraph"><p>A recursive datatype like</p></div>
 161 <div class="listingblock">
 162 <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>
 163 </pre></div></div></div>
 164 <div class="paragraph"><p>introduces a new problem, since in order to decide whether <span class="monospaced">t</span>
 165 admits equality, we need to know for the <span class="monospaced">B</span> <a href="Variant">variant</a> whether
 166 <span class="monospaced">t</span> admits equality.  The <a href="DefinitionOfStandardML">Definition</a>
 167 answers this question by requiring a type constructor to admit
 168 equality if it is consistent to do so.  So, in our above example, if
 169 we assume that <span class="monospaced">t</span> admits equality, then the <a href="Variant">variant</a>
 170 <span class="monospaced">B of int * t</span> admits equality.  Then, since the <span class="monospaced">A</span> <a href="Variant">variant</a>
 171 trivially admits equality, so does the type constructor <span class="monospaced">t</span>.
 172 Thus, it was consistent to assume that <span class="monospaced">t</span> admits equality, and
 173 so, <span class="monospaced">t</span> does admit equality.</p></div>
 174 <div class="paragraph"><p>On the other hand, in the following declaration</p></div>
 175 <div class="listingblock">
 176 <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>
 177 </pre></div></div></div>
 178 <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>
 179 does not admit equality.  Hence, the type constructor <span class="monospaced">t</span> does not
 180 admit equality, and our assumption was inconsistent.  Hence, <span class="monospaced">t</span>
 181 does not admit equality.</p></div>
 182 <div class="paragraph"><p>The same kind of reasoning applies to mutually recursive datatypes as
 183 well.  For example, the following defines both <span class="monospaced">t</span> and <span class="monospaced">u</span> to
 184 admit equality.</p></div>
 185 <div class="listingblock">
 186 <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>
 187 <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>
 188 </pre></div></div></div>
 189 <div class="paragraph"><p>But the following defines neither <span class="monospaced">t</span> nor <span class="monospaced">u</span> to admit
 190 equality.</p></div>
 191 <div class="listingblock">
 192 <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>
 193 <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>
 194 </pre></div></div></div>
 195 <div class="paragraph"><p>As always, we can check whether a type admits equality using an
 196 <span class="monospaced">eqtype</span> specification.</p></div>
 197 <div class="listingblock">
 198 <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>
 199 <span class="w">   </span><span class="k">struct</span><span class="w"></span>
 200 <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>
 201 <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>
 202 <span class="w">   </span><span class="k">end</span><span class="w"></span>
 203 </pre></div></div></div>
 204 <div class="paragraph"><p>MLton reports the following error.</p></div>
 205 <div class="listingblock">
 206 <div class="content monospaced">
 207 <pre>Error: z.sml 1.16-1.40.
 208   Type in structure disagrees with signature (admits equality): t.
 209     structure: datatype t = B of [_str.u] * [real] | ...
 210     defn at: z.sml 3.16-3.16
 211     signature: [eqtype] t
 212     spec at: z.sml 1.27-1.27
 213 Error: z.sml 1.16-1.40.
 214   Type in structure disagrees with signature (admits equality): u.
 215     structure: datatype u = D of [_str.t] | ...
 216     defn at: z.sml 4.11-4.11
 217     signature: [eqtype] u
 218     spec at: z.sml 1.36-1.36</pre>
 219 </div></div>
 220 </div>
 221 </div>
 222 </div>
 223 </div>
 224 <div id="footnotes"><hr></div>
 225 <div id="footer">
 226 <div id="footer-text">
 227 </div>
 228 <div id="footer-badges">
 229 </div>
 230 </div>
 231 </body>
 232 </html>