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

Fri Jul 6 23:41:59 CEST 2012

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, <oleg at okmij.org> wrote:

>
> 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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120706/d8fa63c9/attachment.htm>