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

[Kangyuan Niu]

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, o...@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.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Kangyuan Niu]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe