[Haskell-cafe] translation between two flavors of lexically-scoped type variables

5 Jul 2012

      The paper "Lexically scoped type variables" by Simon Peyton Jones and Mark
Shields describes two ways to give type variables lexical scoping. They
state that one of the advantages of the GHC-style type-sharing approach
over the SML-style type-lambda approach is that the former allows for
existential quantification in addition to universal quantification. As an
example, they give this code:

    data Ap = forall a. Ap [a] ([a] -> Int)

The constructor `Ap` has the type:

    Ap :: forall a. [a] -> ([a] -> Int) -> Ap

And one can write a function:

    revap :: Ap -> Int
    revap (Ap (xs :: [a]) f) = f ys
      where
        ys :: [a]
        ys = reverse xs

with the annotations on `xs` and `ys` being existential instead of
universal.

But I'm a little confused about *why* type-lambdas don't allow this. Aren't
both Haskell and SML translatable into System F, from which type-lambda is
directly taken? What does the translation for the above code even look
like? 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?

-Kangyuan Niu