Re: [Haskell-cafe] What does the `forall` mean ?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 foralls 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 ma...@glyphic.com 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 foralls 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
On Sun, Nov 15, 2009 at 01:14:34AM +, 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
2009/11/12 Andrew Coppin andrewcop...@btinternet.com: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
Eugene Kirpichov wrote: 2009/11/12 Andrew Coppin andrewcop...@btinternet.com: 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
2009/11/12 Neil Brown nc...@kent.ac.uk: Eugene Kirpichov wrote: 2009/11/12 Andrew Coppin andrewcop...@btinternet.com: 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
On Thu, Nov 12, 2009 at 2:50 AM, Eugene Kirpichov ekirpic...@gmail.com 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
Eugene Kirpichov wrote: 2009/11/12 Andrew Coppin andrewcop...@btinternet.com: 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
2009/11/12 Ryan Ingram ryani.s...@gmail.com: On Thu, Nov 12, 2009 at 2:50 AM, Eugene Kirpichov ekirpic...@gmail.com 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
On Thu, Nov 12, 2009 at 8:52 PM, Andrew Coppin andrewcop...@btinternet.com 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
David Virebayre wrote: On Thu, Nov 12, 2009 at 8:52 PM, Andrew Coppin andrewcop...@btinternet.com 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does the `forall` mean ?
On Wed, Nov 11, 2009 at 4:24 PM, zaxis z_a...@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
Re: [Haskell-cafe] What does the `forall` mean ?
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_a...@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 - fac n = foldr (*) 1 [1..n] -- View this message in context: http://old.nabble.com/What-does-the-%60forall%60-mean---tp26311291p26314602.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
