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