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

Kangyuan Niu kangyuan.niu at gmail.com
Thu Jul 5 06:55:39 CEST 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
        ys :: [a]
        ys = reverse xs

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

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
        ys :: 'a list
        ys = reverse xs

in SML?

-Kangyuan Niu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120705/510c9801/attachment.html>

More information about the Haskell-Cafe mailing list