<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="generator" content="Asciidoctor 2.0.26">
<title>EqualityTypeVariable</title>
<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700">
<link rel="stylesheet" href="./asciidoctor.css">
<link rel="stylesheet" href="./mlton.css">

</head>
<body class="article">
<div id="mlton-header">
<div id="mlton-header-text">
<h2>
<a href="./Home">
MLton
20241230+git20251029+dfsg-5
</a>
</h2>
</div>
</div>
<div id="header">
<h1>EqualityTypeVariable</h1>
</div>
<div id="content">
<div id="preamble">
<div class="sectionbody">
<div class="paragraph">
<p>An equality type variable is a type variable that starts with two or
more primes, as in <code>''a</code> or <code>''b</code>.  The canonical use of equality type
variables is in specifying the type of the <a href="PolymorphicEquality">PolymorphicEquality</a>
function, which is <code>''a * ''a -&gt; bool</code>.  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>
</div>
<div class="paragraph">
<p>For example, the following program is type correct because polymorphic
equality is applied to variables of type <code>''a</code>.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">fun f (x: ''a, y: ''a): bool = x = y</code></pre>
</div>
</div>
<div class="paragraph">
<p>On the other hand, the following program is not type correct, because
polymorphic equality is applied to variables of type <code>'a</code>, which is
not an equality type.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">fun f (x: 'a, y: 'a): bool = x = y</code></pre>
</div>
</div>
<div class="paragraph">
<p>MLton reports the following error, indicating that polymorphic
equality expects equality types, but didn&#8217;t get them.</p>
</div>
<div class="listingblock">
<div class="content">
<pre>Error: z.sml 1.30-1.34.
  Function applied to incorrect argument.
    expects: [&lt;equality&gt;] * [&lt;equality&gt;]
    but got: ['a] * ['a]
    in: = (x, y)</pre>
</div>
</div>
<div class="paragraph">
<p>As an example of using such a function that requires equality types,
suppose that <code>f</code> has polymorphic type <code>''a -&gt; unit</code>.  Then, <code>f 13</code> is
type correct because <code>int</code> is an equality type.  On the other hand,
<code>f 13.0</code> and <code>f (fn x =&gt; x)</code> are not type correct, because <code>real</code> and
arrow types are not equality types.  We can test these facts with the
following short programs.  First, we verify that such an <code>f</code> can be
applied to integers.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">functor Ok (val f: ''a -&gt; unit): sig end =
   struct
      val () = f 13
      val () = f 14
   end</code></pre>
</div>
</div>
<div class="paragraph">
<p>We can do better, and verify that such an <code>f</code> can be applied to
any integer.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">functor Ok (val f: ''a -&gt; unit): sig end =
   struct
      fun g (x: int) = f x
   end</code></pre>
</div>
</div>
<div class="paragraph">
<p>Even better, we don&#8217;t need to introduce a dummy function name; we can
use a type constraint.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">functor Ok (val f: ''a -&gt; unit): sig end =
   struct
      val _ = f: int -&gt; unit
   end</code></pre>
</div>
</div>
<div class="paragraph">
<p>Even better, we can use a signature constraint.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">functor Ok (S: sig val f: ''a -&gt; unit end):
   sig val f: int -&gt; unit end = S</code></pre>
</div>
</div>
<div class="paragraph">
<p>This functor concisely verifies that a function of polymorphic type
<code>''a -&gt; unit</code> can be safely used as a function of type <code>int -&gt; unit</code>.</p>
</div>
<div class="paragraph">
<p>As above, we can verify that such an <code>f</code> can not be used at
non-equality types.</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">functor Bad (S: sig val f: ''a -&gt; unit end):
   sig val f: real -&gt; unit end = S

functor Bad (S: sig val f: ''a -&gt; unit end):
   sig val f: ('a -&gt; 'a) -&gt; unit end = S</code></pre>
</div>
</div>
<div class="paragraph">
<p>MLton reports the following errors.</p>
</div>
<div class="listingblock">
<div class="content">
<pre>Error: z.sml 2.4-2.30.
  Variable in structure disagrees with signature (type): f.
    structure: val f: [&lt;equality&gt;] -&gt; _
    defn at: z.sml 1.25-1.25
    signature: val f: [real] -&gt; _
    spec at: z.sml 2.12-2.12
Error: z.sml 5.4-5.36.
  Variable in structure disagrees with signature (type): f.
    structure: val f: [&lt;equality&gt;] -&gt; _
    defn at: z.sml 4.25-4.25
    signature: val f: [_ -&gt; _] -&gt; _
    spec at: z.sml 5.12-5.12</pre>
</div>
</div>
</div>
</div>
<div class="sect1">
<h2 id="_equality_type_variables_in_type_and_datatype_declarations">Equality type variables in type and datatype declarations</h2>
<div class="sectionbody">
<div class="paragraph">
<p>Equality type variables can be used in type and datatype declarations;
however they play no special role.  For example,</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">type 'a t = 'a * int</code></pre>
</div>
</div>
<div class="paragraph">
<p>is completely identical to</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">type ''a t = ''a * int</code></pre>
</div>
</div>
<div class="paragraph">
<p>In particular, such a definition does <em>not</em> require that <code>t</code> only be
applied to equality types.</p>
</div>
<div class="paragraph">
<p>Similarly,</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">datatype 'a t = A | B of 'a</code></pre>
</div>
</div>
<div class="paragraph">
<p>is completely identical to</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="rouge highlight"><code data-lang="sml">datatype ''a t = A | B of ''a</code></pre>
</div>
</div>
</div>
</div>
</div>
</body>
</html>