What does the `forall` mean ?

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

What does the `forall` mean ?

z_axis
import Text.ParserCombinators.Parsec

data PermParser tok st a = Perm (Maybe a) [Branch tok st a]
data Branch tok st a     = forall b. Branch (PermParser tok st (b -> a)) (GenParser tok st b)

I have hoogled the `forall` but i cannot find any appropriate answer!  

thanks!
e^(π.i) + 1 = 0
Reply | Threaded
Open this post in threaded view
|

Re: What does the `forall` mean ?

jfredett
Forall means the same thing as it means in math, it means "for any  
type -- call it `b` -- then the type of the following it `Branch  
(PermParser tok st (b -> a)`"

`tok`, `st` and `a` are all given by the declaration of the datatype  
itself.

Hope that makes sense,

/Joe

On Nov 11, 2009, at 7:24 PM, zaxis wrote:

>
> import Text.ParserCombinators.Parsec
>
> data PermParser tok st a = Perm (Maybe a) [Branch tok st a]
> data Branch tok st a     = forall b. Branch (PermParser tok st (b ->  
> a))
> (GenParser tok st b)
>
> I have hoogled the `forall` but i cannot find any appropriate answer!
>
> thanks!
>
> -----
> fac n = foldr (*) 1 [1..n]
> --
> View this message in context: http://old.nabble.com/What-does-the-%60forall%60-mean---tp26311291p26311291.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

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

Re: What does the `forall` mean ?

Dan Piponi-2
In reply to this post by z_axis
On Wed, Nov 11, 2009 at 4:24 PM, zaxis <[hidden email]> wrote:
> data Branch tok st a     = forall b. Branch (PermParser tok st (b -> a))
> (GenParser tok st b)
>
> I have hoogled the `forall` but i cannot find any appropriate answer!

That's an example of an existential type. What that line is saying is
that for any type b (ie. for all b) that you could pick, the
constructor called 'Branch' can take something of type 'PermParser tok
st (b -> a)' and something of type 'GenParser tok st b' and make
something of type 'Branch tok st a' out of it.

The reason it's called an existential type is something like this:
once you've constructed your thing of type 'Branch tok st a' you've
lost the information about what the type b was. So all you know is
that inside your thing is a pair of objects of type 'PermParser tok st
(b -> a)' and 'GenParser tok st b' but you don't know what b is. All
you know is that there exists some type 'b' that it was made of.

To use these types with ghc you need to use the compilation flag
-XExistentialQuantification.

There's more to be found here:
http://www.haskell.org/haskellwiki/Existential_type
--
Dan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: What does the `forall` mean ?

z_axis
Without `forall`, the ghci will complain: "Not in scope: type variable `b' "
It is clear now. thank you!

Dan Piponi-2 wrote
On Wed, Nov 11, 2009 at 4:24 PM, zaxis <z_axis@163.com> wrote:
> data Branch tok st a     = forall b. Branch (PermParser tok st (b -> a))
> (GenParser tok st b)
>
> I have hoogled the `forall` but i cannot find any appropriate answer!

That's an example of an existential type. What that line is saying is
that for any type b (ie. for all b) that you could pick, the
constructor called 'Branch' can take something of type 'PermParser tok
st (b -> a)' and something of type 'GenParser tok st b' and make
something of type 'Branch tok st a' out of it.

The reason it's called an existential type is something like this:
once you've constructed your thing of type 'Branch tok st a' you've
lost the information about what the type b was. So all you know is
that inside your thing is a pair of objects of type 'PermParser tok st
(b -> a)' and 'GenParser tok st b' but you don't know what b is. All
you know is that there exists some type 'b' that it was made of.

To use these types with ghc you need to use the compilation flag
-XExistentialQuantification.

There's more to be found here:
http://www.haskell.org/haskellwiki/Existential_type
--
Dan
_______________________________________________
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: What does the `forall` mean ?

Andrew Coppin
In reply to this post by Dan Piponi-2
Dan Piponi wrote:
> To use these types with ghc you need to use the compilation flag
> -XExistentialQuantification.
>  

Or, more portably, add {-# LANGUAGE ExistentialQuantification #-} at the
top of the source file. It should now compile in any computer that
supports this feature without any special command-line flags.

> There's more to be found here:
> http://www.haskell.org/haskellwiki/Existential_typ

Amusingly, half of this article is still the text that I wrote. ;-)

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

Re: What does the `forall` mean ?

Andrew Coppin
In reply to this post by jfredett
Joe Fredette wrote:
> Forall means the same thing as it means in math

...which not everybody already knows about. ;-)

Even I am still not 100% sure how placing forall in different positions
does different things. But usually it's not something I need to worry
about. :-)

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

Re: What does the `forall` mean ?

Eugene Kirpichov
2009/11/12 Andrew Coppin <[hidden email]>:
> Joe Fredette wrote:
>>
>> Forall means the same thing as it means in math
>
> ...which not everybody already knows about. ;-)
>
> Even I am still not 100% sure how placing forall in different positions does
> different things. But usually it's not something I need to worry about. :-)

To me it does not look like it does different things: everywhere it
denotes universal polymorphism. What do you mean? I might be missing
something.

>
> _______________________________________________
> 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: What does the `forall` mean ?

Neil Brown-7
Eugene Kirpichov wrote:

> 2009/11/12 Andrew Coppin <[hidden email]>:
>  
>> Even I am still not 100% sure how placing forall in different positions does
>> different things. But usually it's not something I need to worry about. :-)
>>    
>
> To me it does not look like it does different things: everywhere it
> denotes universal polymorphism. What do you mean? I might be missing
> something.
>  
I think what he means is that this:

foo :: forall a b. (a -> a) -> b -> b

uses ScopedTypeVariables, and introduces the type-name a to be available
in the where clause of myid.  Whereas something like this:

foo2 :: (forall a. a -> a) -> b -> b

uses Rank2Types (I think?) to describe a function parameter that works
for all types a.  So although the general concept is the same, they use
different Haskell extensions, and one is a significant extension to the
type system while the other (ScopedTypeVariables) is just some more
descriptive convenience.

Thanks,

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

Re: What does the `forall` mean ?

Eugene Kirpichov
2009/11/12 Neil Brown <[hidden email]>:

> Eugene Kirpichov wrote:
>>
>> 2009/11/12 Andrew Coppin <[hidden email]>:
>>
>>>
>>> Even I am still not 100% sure how placing forall in different positions
>>> does
>>> different things. But usually it's not something I need to worry about.
>>> :-)
>>>
>>
>> To me it does not look like it does different things: everywhere it
>> denotes universal polymorphism. What do you mean? I might be missing
>> something.
>>
>
> I think what he means is that this:
>
> foo :: forall a b. (a -> a) -> b -> b
>
> uses ScopedTypeVariables, and introduces the type-name a to be available in
> the where clause of myid.  Whereas something like this:
>
> foo2 :: (forall a. a -> a) -> b -> b
>
> uses Rank2Types (I think?) to describe a function parameter that works for
> all types a.  So although the general concept is the same, they use
> different Haskell extensions, and one is a significant extension to the type
> system while the other (ScopedTypeVariables) is just some more descriptive
> convenience.
>

But that's not an issue of semantics of forall, just of which part of
the rather broad and universal semantics is captured by which language
extensions.

> Thanks,
>
> Neil.
>



--
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: What does the `forall` mean ?

Ryan Ingram
On Thu, Nov 12, 2009 at 2:50 AM, Eugene Kirpichov <[hidden email]> wrote:
> But that's not an issue of semantics of forall, just of which part of
> the rather broad and universal semantics is captured by which language
> extensions.

The forall for existential type quantification is wierd.

> data Top = forall a. Any a   -- existential
> data Bottom = All (forall a. a) -- rank 2

I think it makes much more sense in GADT syntax:

> data Top where
>    Any :: forall a. a -> Top
> data Bottom where
>    All :: (forall a. a) -> Bottom

where it's clear the forall is scoping the type of the constructor.

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

Re: What does the `forall` mean ?

Andrew Coppin
In reply to this post by Eugene Kirpichov
Eugene Kirpichov wrote:

> 2009/11/12 Andrew Coppin <[hidden email]>:
>  
>> Joe Fredette wrote:
>>    
>>> Forall means the same thing as it means in math
>>>      
>> ...which not everybody already knows about. ;-)
>>
>> Even I am still not 100% sure how placing forall in different positions does
>> different things. But usually it's not something I need to worry about. :-)
>>    
>
> To me it does not look like it does different things: everywhere it
> denotes universal polymorphism. What do you mean? I might be missing
> something.
>  

I just meant it's not immediately clear how

  foo :: forall x. (x -> x -> y)

is different from

 foo :: (forall x. x -> x) -> y

It takes a bit of getting used to.

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

Re: What does the `forall` mean ?

Eugene Kirpichov
In reply to this post by Ryan Ingram
2009/11/12 Ryan Ingram <[hidden email]>:

> On Thu, Nov 12, 2009 at 2:50 AM, Eugene Kirpichov <[hidden email]> wrote:
>> But that's not an issue of semantics of forall, just of which part of
>> the rather broad and universal semantics is captured by which language
>> extensions.
>
> The forall for existential type quantification is wierd.
>
>> data Top = forall a. Any a   -- existential
>> data Bottom = All (forall a. a) -- rank 2
>

Hm, you're right. I didn't even remember you could define existential
types without GADT syntax.

I also find the GADT syntax much better for teaching people what an ADT is.

> I think it makes much more sense in GADT syntax:
>
>> data Top where
>>    Any :: forall a. a -> Top
>> data Bottom where
>>    All :: (forall a. a) -> Bottom
>
> where it's clear the forall is scoping the type of the constructor.
>
>  -- ryan
>



--
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: What does the `forall` mean ?

David Virebayre
In reply to this post by Andrew Coppin
On Thu, Nov 12, 2009 at 8:52 PM, Andrew Coppin
<[hidden email]> wrote:

> I just meant it's not immediately clear how

>  foo :: forall x. (x -> x -> y)

> is different from

> foo :: (forall x. x -> x) -> y

> It takes a bit of getting used to.

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

Re: What does the `forall` mean ?

Andrew Coppin
David Virebayre wrote:

> On Thu, Nov 12, 2009 at 8:52 PM, Andrew Coppin
> <[hidden email]> wrote:
>
>  
>> I just meant it's not immediately clear how
>>    
>
>  
>>  foo :: forall x. (x -> x -> y)
>>    
>
>  
>> is different from
>>    
>
>  
>> foo :: (forall x. x -> x) -> y
>>    
>
>  
>> It takes a bit of getting used to.
>>    
>
> That still confuses me.
>  

The difference is when the x variable gets bound - but to comprehend
that, you have to realise that x gets bound at some point, which is
non-obvious...

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

Re: What does the `forall` mean ?

Steffen Schuldenzucker
In reply to this post by Andrew Coppin
Andrew Coppin wrote:
>
> I just meant it's not immediately clear how
>
>  foo :: forall x. (x -> x -> y)
>
> is different from
>
> foo :: (forall x. x -> x) -> y

Uhm, I guess you meant

foo :: forall x. ((x -> x) -> y)

VS.

foo :: (forall x. x -> x) -> y


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

Re: What does the `forall` mean ?

Sean Leather
In reply to this post by Andrew Coppin
 
I just meant it's not immediately clear how

 foo :: forall x. (x -> x -> y)

is different from

foo :: (forall x. x -> x) -> y

It takes a bit of getting used to.

Those are different functions all together, so perhaps you meant these.

  foo :: forall x y. (x -> x) -> y
  bar :: forall y. (forall x . x -> x) -> y

While neither function is seemingly useful, the second says that the higher-order argument must be polymorphic. I see two options:

  bar id
  bar undefined

The first has these and many more:

  foo (+1)
  foo show
  foo ($)
  ...

Sean

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

Re: What does the `forall` mean ?

Mark Lentczner
On Nov 12, 2009, at 2:59 PM, Sean Leather wrote:
>   foo :: forall x y. (x -> x) -> y
>   bar :: forall y. (forall x . x -> x) -> y
>
> While neither function is seemingly useful, the second says that the higher-order argument must be polymorphic. I see two options:

AHA! This is the bit of insight I needed! My confusion over forall was I thought that I understood that all Haskell types were as if there was a forall for all free type variables in front of the expression. For example, I think the following are the same:

        fizz :: a -> String -> [a]
        fizz :: forall a. a -> String -> [a]

So why would you need forall? The example Sean explained is that if you want to control the scope of the existential quantification. And you can only "push the scope inward", since the outer most scope basically "forall"s all the free type variables (after type inference, I suppose.)

I also think I understand that the implicit 'forall' inherent in Haskell falls at different places in various constructs, which also had me confused. For example, while the above two function type declarations are equivalent, these two data declarations aren't:

        data Fizzle a = Fizzle (b -> (a, b)) a
        data Fizzle a = forall b. Fizzle (b -> (a, b)) a

This would be because the implicit 'forall' is essentially to the left of the 'data Fizzle a' section. I'm guessing that the same holds true for type and newtype constructs.

Have I got this all correct?

Would I be correct in thinking: The difference between these two is that the type b can be "fixed" upon application of amy to the first two arguments (given context), whereas bob applied to two arguments MUST return a function that is applicable to every type.

        amy :: Int -> a -> b -> [Either a b]
        bob :: Int -> a -> (forall b. b) -> [Either a b]

Thanks for helping me understand...
        - Mark

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

Re: What does the `forall` mean ?

Lennart Augustsson
Of the two declarations
>        data Fizzle a = Fizzle (b -> (a, b)) a
>        data Fizzle a = forall b. Fizzle (b -> (a, b)) a
only the second one is allowed (with some suitable extension).

Personally I think the first one should be allowed as well, with the
same meaning as the second one.
Some people thought it was to error prone not to have any indication
when an existential type is introduced,
so instead we are now stuck with a somewhat confusing keyword.

  -- Lennart

On Sat, Nov 14, 2009 at 4:55 PM, Mark Lentczner <[hidden email]> wrote:

> On Nov 12, 2009, at 2:59 PM, Sean Leather wrote:
>>   foo :: forall x y. (x -> x) -> y
>>   bar :: forall y. (forall x . x -> x) -> y
>>
>> While neither function is seemingly useful, the second says that the higher-order argument must be polymorphic. I see two options:
>
> AHA! This is the bit of insight I needed! My confusion over forall was I thought that I understood that all Haskell types were as if there was a forall for all free type variables in front of the expression. For example, I think the following are the same:
>
>        fizz :: a -> String -> [a]
>        fizz :: forall a. a -> String -> [a]
>
> So why would you need forall? The example Sean explained is that if you want to control the scope of the existential quantification. And you can only "push the scope inward", since the outer most scope basically "forall"s all the free type variables (after type inference, I suppose.)
>
> I also think I understand that the implicit 'forall' inherent in Haskell falls at different places in various constructs, which also had me confused. For example, while the above two function type declarations are equivalent, these two data declarations aren't:
>
>        data Fizzle a = Fizzle (b -> (a, b)) a
>        data Fizzle a = forall b. Fizzle (b -> (a, b)) a
>
> This would be because the implicit 'forall' is essentially to the left of the 'data Fizzle a' section. I'm guessing that the same holds true for type and newtype constructs.
>
> Have I got this all correct?
>
> Would I be correct in thinking: The difference between these two is that the type b can be "fixed" upon application of amy to the first two arguments (given context), whereas bob applied to two arguments MUST return a function that is applicable to every type.
>
>        amy :: Int -> a -> b -> [Either a b]
>        bob :: Int -> a -> (forall b. b) -> [Either a b]
>
> Thanks for helping me understand...
>        - Mark
>
> _______________________________________________
> 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: What does the `forall` mean ?

Felipe Lessa
On Sun, Nov 15, 2009 at 01:14:34AM +0000, Lennart Augustsson wrote:

> Of the two declarations
> >        data Fizzle a = Fizzle (b -> (a, b)) a
> >        data Fizzle a = forall b. Fizzle (b -> (a, b)) a
> only the second one is allowed (with some suitable extension).
>
> Personally I think the first one should be allowed as well, with the
> same meaning as the second one.
> Some people thought it was to error prone not to have any indication
> when an existential type is introduced,
> so instead we are now stuck with a somewhat confusing keyword.

I think you are able to say

  data Fizzle a where
    Fizzle :: (b -> (a,b)) -> a -> Fizzle a

Cheers,

--
Felipe.


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

Re: What does the `forall` mean ?

Sean Leather
In reply to this post by Mark Lentczner

On Sat, Nov 14, 2009 at 17:55, Mark Lentczner wrote:
Would I be correct in thinking: The difference between these two is that the type b can be "fixed" upon application of amy to the first two arguments (given context), whereas bob applied to two arguments MUST return a function that is applicable to every type.

       amy :: Int -> a -> b -> [Either a b]
       bob :: Int -> a -> (forall b. b) -> [Either a b]

Here are the same functions using fresh variables where necessary plus an additional function:

  amy :: forall a b. Int -> a -> b -> [Either a b]
  bob :: forall a b. Int -> a -> (forall c. c) -> [Either a b]
  cat :: forall a  . Int -> a -> (forall b. b -> [Either a b])

First, note that the types of amy and cat are equivalent. Since function arrows are right-associative and since there are no conflicting variables b outside the scope of forall b, the quantification can easily be pushed to the outside as in amy. (I don't know if cat is what you meant to have for bob, so I thought I'd add it just in case.)

As for bob, the only third argument it can take is bottom (undefined or error). And that argument has no effect on the types instantiated for a or b. (Using a fresh variable c helps make that more evident at a glance.)

Sean

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