2009/11/12 Andrew Coppin :

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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

2009/11/12 Neil Brown :

Eugene Kirpichov wrote:

...

2009/11/12 Andrew Coppin :

...

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

2009/11/12 Ryan Ingram :

On Thu, Nov 12, 2009 at 2:50 AM, Eugene Kirpichov 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

On Thu, Nov 12, 2009 at 8:52 PM, 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

It takes a bit of getting used to.

That still confuses me.

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?

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

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.

Mark Lentczner wrote:

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

They shouldn't. For data declarations there's the mix up that Lennart Augustsson brought up, but that's more of an issue with the implicit forall not being added in the first case. Basically, the implicit forall is always added at the front. So if I have some type T, then that's implicitly (forall a b c... . T). It's like constructing well-formed formulae in predicate calculus except that we're never allowed to have free variables, just like we can't have free variables in a well-formed expression of the lambda calculus. Since Hindley--Milner type inference can only deal with Rank-1 polymorphism we know all the quantifiers must be at the front, and since we know everything must be quantified we can just leave the quantifiers implicit. In GHC we can have Rank-N quantification but we need to give the signatures to tell the compiler we're using them. The reason I said "basically" is because Haskell also has some constructs which give type variables a larger scope than just the signature for a single function. Many of these (data, type, newtype, class) introduce a different kind of quantifier. The new quantifier is frequently written with iota and basically means that the variable is bound in the environment. Of course now that means we have to think about passing around an environment instead of just checking each signature in isolation. (There are other reasons why the compiler would have an environment for things, but now the user has to think about them too.) -- Live well, ~wren

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 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

----- fac n = foldr (*) 1 [1..n] -- View this message in context: http://old.nabble.com/What-does-the-%60forall%60-mean---tp26311291p26314602.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.