<div dir="ltr"><br><br><div class="gmail_quote">On Mon, Oct 6, 2008 at 1:56 PM, Ryan Ingram <span dir="ltr">&lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
2008/10/6 Jason Dagit &lt;<a href="mailto:dagit@codersbase.com">dagit@codersbase.com</a>&gt;:<br>
<div class="Ih2E3d">&gt; \begin{code}<br>
&gt; badOrder :: (Sealed (p x)) -&gt; (forall b. (Sealed (q b))) -&gt; (Sealed (q x))<br>
&gt; badOrder sx sy = case sy of<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;Sealed y -&gt; case sx of<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;Sealed x -&gt; Sealed (f x y)<br>
&gt; \end{code}<br>
&gt;<br>
&gt; \begin{code}<br>
&gt; goodOrder :: (Sealed (p x)) -&gt; (forall b. (Sealed (q b))) -&gt; (Sealed (q x))<br>
&gt; goodOrder sx sy = case sx of<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; Sealed x -&gt; case sy of<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; Sealed y -&gt; Sealed (f x y)<br>
&gt; \end{code}<br>
<br>
</div>It may help if you transform this a bit closer to System F with<br>
existentials &amp; datatypes:<br>
/\ = forall</blockquote><div><br>Why is useful to replace forall with /\?<br>&nbsp;</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
@t = type application, with the rule:<br>
<br>
(a :: forall x. b) @t :: (replace occurrences of x in b with t)</blockquote><div><br>How do you know how to apply this rule in general?<br><br>For example, (a :: forall x y. x -&gt; y) @t, would mean what?<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
-- the quantified type &quot;x&quot; gets packed into the data<br>
-- and comes out when you pattern match on it<br>
data Sealed s where<br>
 &nbsp; &nbsp;Sealed :: /\t. s t -&gt; Sealed s</blockquote><div><br>By &#39;x&#39; you mean &#39;t&#39; right? <br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

goodOrder = \sx :: Sealed (p x) -&gt; \sy :: (/\b. Sealed (q b)) -&gt;<br>
 &nbsp; &nbsp;case sx of (Sealed @y pxy) -&gt;<br>
 &nbsp; &nbsp; &nbsp; &nbsp;case (sy @y) of (Sealed @z qyz) -&gt;<br>
 &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;Sealed @z (f pxy qyz)</blockquote><div><br>You have the expression (Sealed @y pxy), but I don&#39;t understand what that signifies.&nbsp; Are you just saying that by doing a pattern match on &#39;sx&#39; that you&#39;re going to bind the existentially quantified variable to &#39;y&#39;?&nbsp; This notation confuses me, but I can happily accept that we are binding the existential type &#39;y&#39; somewhere.<br>
<br>Assuming, I understand that, correctly, the expression (Sealed @z qyz) is binding &#39;z&#39; to an existential.&nbsp; Why do you say, (sy @y).&nbsp; What does that mean?&nbsp; That makes &#39;b&#39; unify with &#39;y&#39; that was bound in the first case?&nbsp; goodOrder works as I expect, so I&#39;m happy with this.<br>
<br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
badOrder = \sx :: Sealed (p x) -&gt; \sy :: (/\b. Sealed (q b)) -&gt;<br>
 &nbsp; &nbsp;-- in order to pattern-match on sy, we need to give it a type<br>
 &nbsp; &nbsp;-- so we just pick an arbitrary type &quot;unknown&quot; or &quot;u&quot; distinct<br>
from any other type we know about<br>
 &nbsp; &nbsp;case (sy @u) of (Sealed @z quz) -&gt;<br>
 &nbsp; &nbsp; &nbsp; &nbsp;case sx of (Sealed @y pxy) -&gt;<br>
 &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;Sealed @z (f pxy quz) -- doesn&#39;t typecheck!<br>
<br>
In the good order, you have already unpacked the existential for sx,<br>
so you know what type to instantiate sy at. &nbsp;In the bad order, you<br>
don&#39;t know what type to instantiate sy at.</blockquote><div><br>We instantiate &#39;u&#39; to be the existential in sy.&nbsp; OK.&nbsp; But, my understanding is that &#39;u&#39; is unconstrained at this point, we said, forall b. Sealed (q b), afterall.&nbsp; So, when we bind &#39;y&#39; in the second case, what prevents &#39;u&#39; from unifying with &#39;y&#39;?<br>
<br>For what it&#39;s worth, in my real program where this came up, sy was created by a recursive call like this:<br>foo :: Sealed (p x) -&gt; Sealed (q b)<br>foo = do<br>&nbsp; p &lt;- blah<br>&nbsp; q &lt;- foo<br>&nbsp; return (Sealed (f p q))<br>
<br>Because the b doesn&#39;t appear on the LHS of the function arrow, I understand it to have the same polymorphic properties as the &#39;forall b.&#39; in the type signature of goodOrder and badOrder.&nbsp; Indeed, this example seems to re-enforce that.&nbsp; We had to reorder the binding of p and q to get this to type check.<br>
<br>Thanks for the quick response,<br>Jason<br></div></div><br></div>