How to understand the 'forall' ?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
24 messages Options
12
Reply | Threaded
Open this post in threaded view
|

How to understand the 'forall' ?

z_axis
data Branch tok st a = forall b. Branch (PermParser tok st (b -> a)) (GenParser tok st b)

please shed a light on me, thanks!
e^(π.i) + 1 = 0
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Eugene Kirpichov
This means that for any type 'b' you can construct a value of type
'Branch tok st a' by passing to Branch an argument of type
'(PermParser tok st (b -> a))' and 'GenParser tok st b'.
This also means that when you're given a value of type Branch tok st
a, you don't know what that 'b' type was; the only thing you know is
that the 'b' in 'b -> a' in the first argument of Branch is the same
as the 'b' in 'GenParser tok st b'.

See also: the haskellwiki page on existential types.

2009/9/2 zaxis <[hidden email]>:

>
> data Branch tok st a = forall b. Branch (PermParser tok st (b -> a))
> (GenParser tok st b)
>
> please shed a light on me, thanks!
> --
> View this message in context: http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25250783.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

z_axis
Isnot it clear without the 'forall' ?
data Branch tok st a = Branch (PermParser tok st (b -> a)) (GenParser tok st b)

thanks!

jkff wrote
This means that for any type 'b' you can construct a value of type
'Branch tok st a' by passing to Branch an argument of type
'(PermParser tok st (b -> a))' and 'GenParser tok st b'.
This also means that when you're given a value of type Branch tok st
a, you don't know what that 'b' type was; the only thing you know is
that the 'b' in 'b -> a' in the first argument of Branch is the same
as the 'b' in 'GenParser tok st b'.

See also: the haskellwiki page on existential types.

2009/9/2 zaxis <z_axis@163.com>:
>
> data Branch tok st a = forall b. Branch (PermParser tok st (b -> a))
> (GenParser tok st b)
>
> please shed a light on me, thanks!
> --
> View this message in context: http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25250783.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
e^(π.i) + 1 = 0
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Ryan Ingram
In reply to this post by Eugene Kirpichov
You can also look at it in terms of the "deconstruction" operation on
this data type.

For example, lists:

> data List a = Nil | Cons a (List a)
>
> case_list :: r -> (a -> List a -> r) -> List a -> r
> case_list nil_case cons_case Nil = nil_case
> case_list nil_case cons_case (Cons x xs) = cons_case x xs

Now, given the "Branch" type:

> data Branch tok st a = forall b. Branch (PermParser tok st (b -> a)) (GenParser tok st b)

what is the type of its "case" construct?  Here's the answer:

> case_branch :: (forall b. PermParser tok st (b -> a) -> GenParser tok st b -> r) -> Branch tok st a -> r
> case_branch k (Branch pparser gparser) = k pparser gparser

Notice the higher-rank type on the argument k; it has to be able to
accept *any* type b, because the constructor hid an object of *some*
type which is no longer known.  So unless you can accept *any* b, you
can't operate on this object.

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Eugene Kirpichov
In reply to this post by z_axis
2009/9/2 zaxis <[hidden email]>:
>
> Isnot it clear without the 'forall' ?
> data Branch tok st a = Branch (PermParser tok st (b -> a)) (GenParser tok st
> b)
>
> thanks!
>

The situation is not so simple.
Consider, for example, a procedure that takes as input a *generic*
sorting algorithm:

sortThem :: (forall a. Ord a => [a] -> [a]) -> [Int] -> [String] ->
([Int], [String])
sortThem sortAlgo ints strings = (sortAlgo ints, sortAlgo strings)

Here you can't omit the 'forall' because if you do, then inside the
body of the sortThem function the 'a' type variable has a fixed value
and can't be both Int and String!

This is a somewhat esoteric example, but one could consider, for
instance, a procedure that takes as input some trees of different
types and a generic tree traversal algorithm. Well, have a look at the
haskellwiki page, there's a pile of examples :)

P.S. I tried to write up the difference between datatype and function
declarations in this respect, but my explanations turned into a mess,
so I erased them in the hope that someone will explain it better than
me.

>
> jkff wrote:
>>
>> This means that for any type 'b' you can construct a value of type
>> 'Branch tok st a' by passing to Branch an argument of type
>> '(PermParser tok st (b -> a))' and 'GenParser tok st b'.
>> This also means that when you're given a value of type Branch tok st
>> a, you don't know what that 'b' type was; the only thing you know is
>> that the 'b' in 'b -> a' in the first argument of Branch is the same
>> as the 'b' in 'GenParser tok st b'.
>>
>> See also: the haskellwiki page on existential types.
>>
>> 2009/9/2 zaxis <[hidden email]>:
>>>
>>> data Branch tok st a = forall b. Branch (PermParser tok st (b -> a))
>>> (GenParser tok st b)
>>>
>>> please shed a light on me, thanks!
>>> --
>>> View this message in context:
>>> http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25250783.html
>>> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>>
>> --
>> Eugene Kirpichov
>> Web IR developer, market.yandex.ru
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
> --
> View this message in context: http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25251783.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

z_axis
seems a bit understanding, i still need to think it  for a while
thanks!

jkff wrote
2009/9/2 zaxis <z_axis@163.com>:
>
> Isnot it clear without the 'forall' ?
> data Branch tok st a = Branch (PermParser tok st (b -> a)) (GenParser tok st
> b)
>
> thanks!
>

The situation is not so simple.
Consider, for example, a procedure that takes as input a *generic*
sorting algorithm:

sortThem :: (forall a. Ord a => [a] -> [a]) -> [Int] -> [String] ->
([Int], [String])
sortThem sortAlgo ints strings = (sortAlgo ints, sortAlgo strings)

Here you can't omit the 'forall' because if you do, then inside the
body of the sortThem function the 'a' type variable has a fixed value
and can't be both Int and String!

This is a somewhat esoteric example, but one could consider, for
instance, a procedure that takes as input some trees of different
types and a generic tree traversal algorithm. Well, have a look at the
haskellwiki page, there's a pile of examples :)

P.S. I tried to write up the difference between datatype and function
declarations in this respect, but my explanations turned into a mess,
so I erased them in the hope that someone will explain it better than
me.

>
> jkff wrote:
>>
>> This means that for any type 'b' you can construct a value of type
>> 'Branch tok st a' by passing to Branch an argument of type
>> '(PermParser tok st (b -> a))' and 'GenParser tok st b'.
>> This also means that when you're given a value of type Branch tok st
>> a, you don't know what that 'b' type was; the only thing you know is
>> that the 'b' in 'b -> a' in the first argument of Branch is the same
>> as the 'b' in 'GenParser tok st b'.
>>
>> See also: the haskellwiki page on existential types.
>>
>> 2009/9/2 zaxis <z_axis@163.com>:
>>>
>>> data Branch tok st a = forall b. Branch (PermParser tok st (b -> a))
>>> (GenParser tok st b)
>>>
>>> please shed a light on me, thanks!
>>> --
>>> View this message in context:
>>> http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25250783.html
>>> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe@haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>>
>> --
>> Eugene Kirpichov
>> Web IR developer, market.yandex.ru
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
> --
> View this message in context: http://www.nabble.com/How-to-understand-the-%27forall%27---tp25250783p25251783.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Eugene Kirpichov
Web IR developer, market.yandex.ru
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
e^(π.i) + 1 = 0
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Cristiano Paris
On Wed, Sep 2, 2009 at 11:00 AM, zaxis<[hidden email]> wrote:
>
> seems a bit understanding, i still need to think it  for a while
> thanks!

I think I've understood the existential types thing, but I still can't
put them to work when I think to a solution for a particular problem,
i.e. it's not among my programming tools yet.

Thank you Eugene, that was one of the most enlighting examples I say
about existential types.

Cristiano
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Sean Leather

I think I've understood the existential types thing, but I still can't
put them to work when I think to a solution for a particular problem,
i.e. it's not among my programming tools yet.

Here's another commonly found, easy-to-understand example that's useful.

> {-# LANGUAGE ExistentialQuantification #-}
>
> module Main where
>
> data Showable = forall a . Show a => S a
>
> instance Show Showable where
>   show (S x) = show x
>
> main = print [S 1, S 'a', S 9.4, S (Just 2)] -- prints [1,'a',9.4,Just 2]

The datatype says that for any type 'a' with an instance of 'Show a', we can construct a value of 'Showable'. While we normally wouldn't be able to build a list with different types, we can now create a [Showable] list with existential types.

Sean

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Per Vognsen
You can of course achieve the same thing by reifying the Show
dictionary as a record and having Showable's Show instance forward to
the dictionary.

A really good paper for an overview of the strengths and weaknesses of
different object encodings (recursive records vs existentials vs
recursive existentials vs bounded existentials) for cases more
complicated than the one below is Comparing Object Encodings by Bruce,
Cardelli and Pierce. Much of the same discussion is also replicated in
Pierce's Types and Programming Languages in a less technical, more
readable form.

-Per


On Wed, Sep 2, 2009 at 10:30 PM, Sean Leather<[hidden email]> wrote:

>
>> I think I've understood the existential types thing, but I still can't
>> put them to work when I think to a solution for a particular problem,
>> i.e. it's not among my programming tools yet.
>
> Here's another commonly found, easy-to-understand example that's useful.
>
>> {-# LANGUAGE ExistentialQuantification #-}
>>
>> module Main where
>>
>> data Showable = forall a . Show a => S a
>>
>> instance Show Showable where
>>   show (S x) = show x
>>
>> main = print [S 1, S 'a', S 9.4, S (Just 2)] -- prints [1,'a',9.4,Just 2]
>
> The datatype says that for any type 'a' with an instance of 'Show a', we can
> construct a value of 'Showable'. While we normally wouldn't be able to build
> a list with different types, we can now create a [Showable] list with
> existential types.
>
> Sean
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Daniil Elovkov
In reply to this post by Eugene Kirpichov
Eugene Kirpichov wrote:
>
> P.S. I tried to write up the difference between datatype and function
> declarations in this respect, but my explanations turned into a mess,
> so I erased them in the hope that someone will explain it better than
> me.
>

Hello Eugene, I'll give it a try.

In a non-constructive way: there seems to be nothing in common between those.

In a constructive way:

Datatype forall is called existential quantification, forall in function signature is called first-class polymorphism, if I'm not mistaken.

Existential is a perfect word, because it really is
data S = exists a. Show a => S [a].
The meaning is that within a given instance of S there lies some value of some particular type (a type exists). It's not any, it's some particular type. It can be either [Int], or forall a. Show a => [a], for example [], or some other type, but it exists.

With first-class polymorphism there's nothing that lies somewhere. Nothing of some particular type. The function whose type is forall ... is applicable to any type within the given bounds. And even this function itself doesn't lie anywhere, since it's a parameter. I think it can be considered just a way to impact the scope of type parameters within the signature, roughly speaking.

Not sure it this is useful, but

data S = ∃x. S x
f :: ∀x. x -> (∀y. y -> t) -> t

and just in case, the data constructor S doesn't use first-class polymorphism since its type is just
S :: ∀x. x -> S

I know that you perfectly understand it, I just tried to word it :)

--
Daniil Elovkov

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Ryan Ingram
On Tue, Sep 8, 2009 at 12:44 PM, Daniil
Elovkov<[hidden email]> wrote:
> Existential is a perfect word, because it really is
> data S = exists a. Show a => S [a].

If you were going to make "exists" a keyword, I think you would write
it like this:

> data S = ConsS (exists a. Show a => [a])

To contrast:

> data GhcS = forall a. Show a => ConsGhcS [a]
> data T = ConsT (forall a. Show a => [a])

This gives these constructors:

> ConsS :: forall a. (Show a => [a] -> S)
> ConsGhcS :: forall a. (Show a => [a] -> S)  -- same
> ConsT :: (forall a. Show a => [a]) -> T -- higher-rank type!

T isn't very useful, it has to be able to provide a list of *any*
instance of Show, so probably [] is all you get.  But you can do
something similar:

> data N = ConsN (forall a. Num a => [a])

Now you get

> ConsN :: (forall a. Num a => [a]) -> N

and you can legally do

> n = ConsN [1,2,3]

since [1,2,3] == [fromInteger 1, fromInteger 2, fromInteger 3] ::
forall a. Num a => [a]

Conceptually, an "S" holds *some* instance of Show, so the user of a
constructed S can only use methods of Show; they don't have any
further knowledge about what is inside.  But a N holds *any* instance
of Num, so the user of the data can pick which one they want to use;
Integer, Rational, Double, some (Expr Int) instance made by an
embedded DSL programmer, etc.

Of course, there are some ways to recover information about what types
are inside the existential using GADTs or Data.Dynamic.  But those
need to be held in the structure itself.  For example:

> data Typ a where
>    TBool :: Typ Bool
>    TInt :: Typ Int
>    TFunc :: Typ a -> Typ b -> Typ (a -> b)
>    TList :: Typ a -> Typ [a]
>    TPair :: Typ a -> Typ b -> Typ (a,b)

Now you can create an existential type like this:

> data Something = forall a. Something (Typ a) a

and you can extract the value if the type matches:

> data TEq a b where Refl :: TEq a a
> extract :: forall a. Typ a -> Something -> Maybe a
> extract ta (Something tb vb) = do
>    Refl <- eqTyp ta tb
>    return vb

This desugars into

] extract ta (Something tb vb) =
]    eqTyp ta tb >>= \x ->
]      case x of
]         Refl -> return vb
]         _ -> fail "pattern match failure"

which, since Refl is the only constructor for TEq, simplifies to

] extract ta (Something tb vb) = eqTyp ta tb >>= \Refl -> Just vb

The trick is that the pattern match on Refl proves on the right-hand
side that "a" is the same type as that held in the existential, so we
have successfully extracted information from the existential and can
return it to the caller without breaking encapsulation.  Here's the
helper function eqTyp; it's pretty mechanical:

> eqTyp :: Typ a -> Typ b -> Maybe (TEq a b)
> eqTyp TBool TBool = return Refl
> eqTyp TInt TInt = return Refl
> eqTyp (TFunc a1 b1) (TFunc a2 b2) = do
>    Refl <- eqTyp a1 a2
>    Refl <- eqTyp b1 b2
>    return Refl
> eqTyp (TList a1) (TList a2) = do
>    Refl <- eqTyp a1 a2
>    return Refl
> eqTyp (TPair a1 b1) (TPair a2 b2) = do
>    Refl <- eqTyp a1 a2
>    Refl <- eqTyp b1 b2
>    return Refl
> eqTyp _ _ = Nothing

Here's a simple test:

> test = Something (TFun TInt TBool) (\x -> x == 3)
> runTest = fromJust (extract (TFun TInt TBool) test) 5

runTest == False, of course.

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Daniil Elovkov
Ryan Ingram wrote:

> On Tue, Sep 8, 2009 at 12:44 PM, Daniil
> Elovkov<[hidden email]> wrote:
>> Existential is a perfect word, because it really is
>> data S = exists a. Show a => S [a].
>
> If you were going to make "exists" a keyword, I think you would write
> it like this:
>
>> data S = ConsS (exists a. Show a => [a])
>
> To contrast:
>
>> data GhcS = forall a. Show a => ConsGhcS [a]
>> data T = ConsT (forall a. Show a => [a])
>
> This gives these constructors:
>
>> ConsS :: forall a. (Show a => [a] -> S)
>> ConsGhcS :: forall a. (Show a => [a] -> S)  -- same
>> ConsT :: (forall a. Show a => [a]) -> T -- higher-rank type!

Yes, this last one can confuse somebody who tries to understand the
difference between existential quantification and first-class
polymorphism. Because it looks like the former, but really is the latter.

> T isn't very useful, it has to be able to provide a list of *any*
> instance of Show, so probably [] is all you get.  But you can do
> something similar:
>
>> data N = ConsN (forall a. Num a => [a])
>
> Now you get
>
>> ConsN :: (forall a. Num a => [a]) -> N
>
> and you can legally do
>
>> n = ConsN [1,2,3]
>
> since [1,2,3] == [fromInteger 1, fromInteger 2, fromInteger 3] ::
> forall a. Num a => [a]
>
> Conceptually, an "S" holds *some* instance of Show, so the user of a
> constructed S can only use methods of Show; they don't have any
> further knowledge about what is inside.  But a N holds *any* instance
> of Num, so the user of the data can pick which one they want to use;
> Integer, Rational, Double, some (Expr Int) instance made by an
> embedded DSL programmer, etc.

Well, that seems to be exactly how I worded it, but with the examples of
data constructor vs function signature, rather than 2 data constructors.

> Of course, there are some ways to recover information about what types
> are inside the existential using GADTs or Data.Dynamic.  But those
> need to be held in the structure itself.  For example:


This is quite amazing. What follows is almost a literal copy of my code,
which isn't open :) Even the names are very close!

In my version eqTyp is unify :)

Hmm, sometimes I think that Haskell allows expressing an intension in so
many ways (and I'm sure it's true), but this...

>> data Typ a where
>>    TBool :: Typ Bool
>>    TInt :: Typ Int
>>    TFunc :: Typ a -> Typ b -> Typ (a -> b)
>>    TList :: Typ a -> Typ [a]
>>    TPair :: Typ a -> Typ b -> Typ (a,b)
>
> Now you can create an existential type like this:
>
>> data Something = forall a. Something (Typ a) a
>
> and you can extract the value if the type matches:
>
>> data TEq a b where Refl :: TEq a a
>> extract :: forall a. Typ a -> Something -> Maybe a
>> extract ta (Something tb vb) = do
>>    Refl <- eqTyp ta tb
>>    return vb
>
> This desugars into
>
> ] extract ta (Something tb vb) =
> ]    eqTyp ta tb >>= \x ->
> ]      case x of
> ]         Refl -> return vb
> ]         _ -> fail "pattern match failure"
>
> which, since Refl is the only constructor for TEq, simplifies to
>
> ] extract ta (Something tb vb) = eqTyp ta tb >>= \Refl -> Just vb
>
> The trick is that the pattern match on Refl proves on the right-hand
> side that "a" is the same type as that held in the existential, so we
> have successfully extracted information from the existential and can
> return it to the caller without breaking encapsulation.  Here's the
> helper function eqTyp; it's pretty mechanical:
>
>> eqTyp :: Typ a -> Typ b -> Maybe (TEq a b)
>> eqTyp TBool TBool = return Refl
>> eqTyp TInt TInt = return Refl
>> eqTyp (TFunc a1 b1) (TFunc a2 b2) = do
>>    Refl <- eqTyp a1 a2
>>    Refl <- eqTyp b1 b2
>>    return Refl
>> eqTyp (TList a1) (TList a2) = do
>>    Refl <- eqTyp a1 a2
>>    return Refl
>> eqTyp (TPair a1 b1) (TPair a2 b2) = do
>>    Refl <- eqTyp a1 a2
>>    Refl <- eqTyp b1 b2
>>    return Refl
>> eqTyp _ _ = Nothing
>
> Here's a simple test:
>
>> test = Something (TFun TInt TBool) (\x -> x == 3)
>> runTest = fromJust (extract (TFun TInt TBool) test) 5
>
> runTest == False, of course.
>
>   -- ryan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Cristiano Paris
In reply to this post by z_axis
On Wed, Sep 2, 2009 at 7:16 AM, zaxis <[hidden email]> wrote:
>
> Isnot it clear without the 'forall' ?
> data Branch tok st a = Branch (PermParser tok st (b -> a)) (GenParser tok st
> b)
>
> thanks!

I elaborated on this and I wish to add my personal way of figuring out
what the "forall" keyword means.

When you define:

foo :: a -> a

you are actually defining a _function for every type of a_, which can
be read: for every a there exists a function foo which can operate on
it (universal quantification).

When you define something like:

foo :: forall a. a -> a

you are actually defining a _single_ function which must work for
every a (that's why we use the "forall" keyword). The difference is
subtle but the direct consequences of this are: a) that one function
can't use any information about a apart from the fact that it
eventually belongs to the type classes specified in the context, b) in
the case of [a] (or any other type of higher kind, * -> *, * -> * -> *
and so on) you can mix values of different types.

I hope I haven't written anything wrong :)

Cristiano
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Daniel Fischer-4
Am Dienstag 15 September 2009 23:13:59 schrieb Cristiano Paris:

> On Wed, Sep 2, 2009 at 7:16 AM, zaxis <[hidden email]> wrote:
> > Isnot it clear without the 'forall' ?
> > data Branch tok st a = Branch (PermParser tok st (b -> a)) (GenParser tok
> > st b)
> >
> > thanks!
>
> I elaborated on this and I wish to add my personal way of figuring out
> what the "forall" keyword means.
>
> When you define:
>
> foo :: a -> a
>
> you are actually defining a _function for every type of a_, which can
> be read: for every a there exists a function foo which can operate on
> it (universal quantification).
>
> When you define something like:
>
> foo :: forall a. a -> a

This is exactly the same type as

foo :: a -> a

(unless you're using ScopedTypeVariables and there's a type variable a in scope), since
type signatures are implicitly forall'd.

>
> you are actually defining a _single_ function which must work for
> every a (that's why we use the "forall" keyword). The difference is
> subtle but the direct consequences of this are: a) that one function
> can't use any information about a apart from the fact that it
> eventually belongs to the type classes specified in the context, b) in
> the case of [a] (or any other type of higher kind, * -> *, * -> * -> *
> and so on) you can mix values of different types.
>
> I hope I haven't written anything wrong :)
>
> Cristiano


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Cristiano Paris
On Tue, Sep 15, 2009 at 11:38 PM, Daniel Fischer
<[hidden email]> wrote:
> ...
>> foo :: forall a. a -> a
>
> This is exactly the same type as
>
> foo :: a -> a
>
> (unless you're using ScopedTypeVariables and there's a type variable a in scope), since
> type signatures are implicitly forall'd.

Yep, perhaps I used the wrong example. What about foo: (forall a. a) -> Int?

Cristiano
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re[2]: How to understand the 'forall' ?

Bulat Ziganshin-2
Hello Cristiano,

Wednesday, September 16, 2009, 12:04:48 PM, you wrote:

> Yep, perhaps I used the wrong example. What about foo: (forall a. a) -> Int?

it's a function that convert anything to integer. for example:

foo _ = 1

it's hard to find better examples, since haskell has very few
functions with fully polymorphic arguments


--
Best regards,
 Bulat                            mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re[2]: How to understand the 'forall' ?

David Menendez-2
On Wed, Sep 16, 2009 at 4:18 AM, Bulat Ziganshin
<[hidden email]> wrote:
> Hello Cristiano,
>
> Wednesday, September 16, 2009, 12:04:48 PM, you wrote:
>
>> Yep, perhaps I used the wrong example. What about foo: (forall a. a) -> Int?
>
> it's a function that convert anything to integer.

That would be forall a. a -> Int.

The only value of type (forall a. a) is _|_.

--
Dave Menendez <[hidden email]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Ryan Ingram
In reply to this post by Cristiano Paris
Here's the difference between these two types:

test1 :: forall a. a -> Int
-- The caller of test1 determines the type for test1
test2 :: (forall a. a) -> Int
-- The internals of test2 determines what type, or types, to instantiate the argument at

Or, to put it another way, since there are no non-bottom objects of type (forall a. a):
test1 converts *anything* to an Int.
test2 converts *nothing* to an Int

-- type-correct implementation
-- instantiates the (forall a. a) argument at Int
test2 x = x

-- type error, the caller chose "a" and it is not necessarily Int
-- test1 x = x

-- type-correct implementation: ignore the argument
test1 _ = 1

  -- ryan

On Wed, Sep 16, 2009 at 1:04 AM, Cristiano Paris <[hidden email]> wrote:
On Tue, Sep 15, 2009 at 11:38 PM, Daniel Fischer
<[hidden email]> wrote:
> ...
>> foo :: forall a. a -> a
>
> This is exactly the same type as
>
> foo :: a -> a
>
> (unless you're using ScopedTypeVariables and there's a type variable a in scope), since
> type signatures are implicitly forall'd.

Yep, perhaps I used the wrong example. What about foo: (forall a. a) -> Int?

Cristiano
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Cristiano Paris
On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <[hidden email]> wrote:
> Here's the difference between these two types:
>
> test1 :: forall a. a -> Int
> -- The caller of test1 determines the type for test1
> test2 :: (forall a. a) -> Int
> -- The internals of test2 determines what type, or types, to instantiate the
> argument at

I can easily understand your explanation for test2: the type var a is
closed under existential (?) quantification. I can't do the same for
test1, even if it seems that a is closed under universal (?)
quantification as well.

> Or, to put it another way, since there are no non-bottom objects of type
> (forall a. a):

Why?

> test1 converts *anything* to an Int.

Is the only possible implementation of test1 the one ignoring its
argument (apart from bottom of course)?

> test2 converts *nothing* to an Int
>
> -- type-correct implementation
> -- instantiates the (forall a. a) argument at Int
> test2 x = x

> -- type error, the caller chose "a" and it is not necessarily Int
> -- test1 x = x
>
> -- type-correct implementation: ignore the argument
> test1 _ = 1

Cristiano
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: How to understand the 'forall' ?

Dan Weston
There is no magic here. This is merely explicit type specialization from
the most general inferred type to something more specific. The
denotational semantics of a function whose type is specialized does not
change for those values belonging to the more specialized type.

f :: forall a. (Num a) => a -> a -> a
f x y = x + y

g :: Int -> Int -> Int
g x y = x + y

f and g denote (extensionally) the identical function, differing only in
their type. g is a specialization of f. It is possible that
(operationally) f could be slower if the compiler is not clever enough
to avoid passing a type witness dictionary.

h :: forall b. b -> Char
h = const 'a'

k :: () -> Char
k = const 'a'

data Void
m :: Void -> Char
m = const 'a'

n :: (forall a. a) -> Char
n = const 'a'

h, k, m, and n yield *identical* values for any input compatible with
the type of any two of the functions.

In constrast, whether a function is strict or non-strict is *not* a
function of type specialization. Strictness is not reflected in the type
system. Compare:

u x y = y `seq` const x y
v x y = const x y

Both have type forall a b. a -> b -> a but are denotationally different
functions:

u 2 undefined = undefined
v 2 undefined = 2

Cristiano Paris wrote:

> On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram <[hidden email]> wrote:
>> Here's the difference between these two types:
>>
>> test1 :: forall a. a -> Int
>> -- The caller of test1 determines the type for test1
>> test2 :: (forall a. a) -> Int
>> -- The internals of test2 determines what type, or types, to instantiate the
>> argument at
>
> I can easily understand your explanation for test2: the type var a is
> closed under existential (?) quantification. I can't do the same for
> test1, even if it seems that a is closed under universal (?)
> quantification as well.
>
>> Or, to put it another way, since there are no non-bottom objects of type
>> (forall a. a):
>
> Why?
>
>> test1 converts *anything* to an Int.
>
> Is the only possible implementation of test1 the one ignoring its
> argument (apart from bottom of course)?
>
>> test2 converts *nothing* to an Int
>>
>> -- type-correct implementation
>> -- instantiates the (forall a. a) argument at Int
>> test2 x = x
>
>> -- type error, the caller chose "a" and it is not necessarily Int
>> -- test1 x = x
>>
>> -- type-correct implementation: ignore the argument
>> test1 _ = 1
>
> Cristiano
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12