Thanks, I think I understand it now.
Do you know why they switched over in GHC 6.6?
-Kangyuan Niu
On Fri, Jul 6, 2012 at 3:11 AM,
Kangyuan Niu wrote:
Aren't both Haskell and SML translatable into System F, from which type-lambda is directly taken?
The fact that both Haskell and SML are translatable to System F does not imply that Haskell and SML are just as expressive as System F. Although SML (and now OCaml) does have what looks like a type-lambda, the occurrences of that type lambda are greatly restricted. It may only come at the beginning of a polymorphic definition (it cannot occur in an argument, for example).
data Ap = forall a. Ap [a] ([a] -> Int) Why isn't it possible to write something like:
fun 'a revap (Ap (xs : 'a list) f) = f ys where ys :: 'a list ys = reverse xs
in SML?
This looks like a polymorphic function: an expression of the form /\a.<body> has the type forall a. <type>. However, the Haskell function
> revap :: Ap -> Int > revap (Ap (xs :: [a]) f) = f ys > where > ys :: [a] > ys = reverse xs
you meant to emulate is not polymorphic. Both Ap and Int are concrete types. Therefore, your SML code cannot correspond to the Haskell code.
That does not mean we can't use SML-style type variables (which must be forall-bound) with existentials. We have to write the elimination principle for existentials explicitly
{-# LANGUAGE ExistentialQuantification, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}
data Ap = forall a. Ap [a] ([a] -> Int)
-- Elimination principle deconAp :: Ap -> (forall a. [a] -> ([a] -> Int) -> w) -> w deconAp (Ap xs f) k = k xs f
revap :: Ap -> Int revap ap = deconAp ap revap'
revap' :: forall a. [a] -> ([a] -> Int) -> Int revap' xs f = f ys where ys :: [a] ys = reverse xs
Incidentally, GHC now uses SML-like design for type variables. However, there is a special exception for existentials. Please see 7.8.7.4. Pattern type signatures of the GHC user manual. The entire section 7.8.7 is worth reading.