[Haskell-cafe] How to understand the 'forall' ?
Ryan Ingram
ryani.spam at gmail.com
Thu Sep 17 12:49:32 EDT 2009
On Thu, Sep 17, 2009 at 6:59 AM, Cristiano Paris <frodo at theshire.org> wrote:
> On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram <ryani.spam at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090917/7427d394/attachment.html
More information about the Haskell-Cafe
mailing list