Re: [Haskell-cafe] How to understand the 'forall' ?

17 Sep 2009

      On Thu, Sep 17, 2009 at 6:59 AM, Cristiano Paris  wrote:
...
On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram  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