Thanks, I think I understand it now.<div><br></div><div>Do you know why they switched over in GHC 6.6?<br><div><br></div><div>-Kangyuan Niu<br><br><div class="gmail_quote">On Fri, Jul 6, 2012 at 3:11 AM,  <span dir="ltr">&lt;<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>&gt;</span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><br>
Kangyuan Niu wrote:<br>
&gt; Aren&#39;t both Haskell and SML translatable into System F, from which<br>
&gt; type-lambda is directly taken?<br>
<br>
</div>The fact that both Haskell and SML are translatable to System F does<br>
not imply that Haskell and SML are just as expressive as System<br>
F. Although SML (and now OCaml) does have what looks like a<br>
type-lambda, the occurrences of that type lambda are greatly<br>
restricted. It may only come at the beginning of a polymorphic<br>
definition (it cannot occur in an argument, for example).<br>
<div><br>
&gt;     data Ap = forall a. Ap [a] ([a] -&gt; Int)<br>
</div><div>&gt; Why isn&#39;t it possible to write something like:<br>
&gt;<br>
&gt;     fun &#39;a revap (Ap (xs : &#39;a list) f) = f ys<br>
&gt;       where<br>
&gt;         ys :: &#39;a list<br>
&gt;         ys = reverse xs<br>
&gt;<br>
&gt; in SML?<br>
<br>
</div>This looks like a polymorphic function: an expression of the form<br>
/\a.&lt;body&gt; has the type forall a. &lt;type&gt;. However, the Haskell function<br>
<div><br>
    &gt; revap :: Ap -&gt; Int<br>
    &gt; revap (Ap (xs :: [a]) f) = f ys<br>
    &gt;   where<br>
    &gt;     ys :: [a]<br>
    &gt;     ys = reverse xs<br>
<br>
</div>you meant to emulate is not polymorphic. Both Ap and Int are concrete<br>
types. Therefore, your SML code cannot correspond to the Haskell code.<br>
<br>
That does not mean we can&#39;t use SML-style type variables (which must<br>
be forall-bound) with existentials. We have to write the<br>
elimination principle for existentials explicitly<br>
<br>
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
<div><br>
data Ap = forall a. Ap [a] ([a] -&gt; Int)<br>
<br>
</div>-- Elimination principle<br>
deconAp :: Ap -&gt; (forall a. [a] -&gt; ([a] -&gt; Int) -&gt; w) -&gt; w<br>
deconAp (Ap xs f) k = k xs f<br>
<br>
<br>
revap :: Ap -&gt; Int<br>
revap  ap = deconAp ap revap&#39;<br>
<br>
revap&#39; :: forall a. [a] -&gt; ([a] -&gt; Int) -&gt; Int<br>
revap&#39; xs f = f ys<br>
<div>  where<br>
  ys :: [a]<br>
  ys = reverse xs<br>
<br>
<br>
</div>Incidentally, GHC now uses SML-like design for type<br>
variables. However, there is a special exception for<br>
existentials. Please see<br>
        7.8.7.4. Pattern type signatures<br>
of the GHC user manual. The entire section 7.8.7 is worth reading.<br>
<br>
<br>
</blockquote></div><br></div>
</div>