On Thu, Sep 17, 2009 at 6:59 AM, Cristiano Paris <fr...@theshire.org> wrote:
> On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram <ryani.s...@gmail.com> wrote: > > ... > > Explicitly: > > > > Haskell: > >> test1 :: forall a. a -> Int > >> test1 _ = 1 > >> test2 :: (forall a. a) -> Int > >> test2 x = x > > > > explicitly in System F: > > > > test1 = /\a \(x :: a). 1 > > test2 = \(x :: forall a. a). x @Int > > > > /\ is type-level lambda, and @ is type-level application. > > Ok. But let me be pedantic: where is the universal quantification in > test1? It seems to me the a is a free variable in test1 while being > closed under universal quantification in test2. > The universal quantification is right in the extra lambda: it works for all types "a". Just like this works on all lists [a]: length = /\a. \(xs :: [a]). case xs of { [] -> 0 ; (x:ys) -> 1 + length @a ys } Here are some uses of test1: v1 = test1 @Int 0 v2 = test1 @[Char] "hello" v3 = test1 @() () Here's a use of test2: v4 = test2 (/\a. error @a "broken") given error :: forall a. String -> a -- ryan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe