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"><<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>></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>
> Aren't both Haskell and SML translatable into System F, from which<br>
> 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>
> data Ap = forall a. Ap [a] ([a] -> Int)<br>
</div><div>> Why isn't it possible to write something like:<br>
><br>
> fun 'a revap (Ap (xs : 'a list) f) = f ys<br>
> where<br>
> ys :: 'a list<br>
> ys = reverse xs<br>
><br>
> in SML?<br>
<br>
</div>This looks like a polymorphic function: an expression of the form<br>
/\a.<body> has the type forall a. <type>. However, the Haskell function<br>
<div><br>
> revap :: Ap -> Int<br>
> revap (Ap (xs :: [a]) f) = f ys<br>
> where<br>
> ys :: [a]<br>
> 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'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] -> Int)<br>
<br>
</div>-- Elimination principle<br>
deconAp :: Ap -> (forall a. [a] -> ([a] -> Int) -> w) -> w<br>
deconAp (Ap xs f) k = k xs f<br>
<br>
<br>
revap :: Ap -> Int<br>
revap ap = deconAp ap revap'<br>
<br>
revap' :: forall a. [a] -> ([a] -> Int) -> Int<br>
revap' 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>