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

Fri Jul 6 09:11:18 CEST 2012

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.