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 :

...

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---tp25250783p252507... 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---tp25250783p252517... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

seems a bit understanding, i still need to think it for a while thanks! jkff wrote:

2009/9/2 zaxis :

...

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 :

...

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---tp25250783p252507... 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---tp25250783p252517... 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---tp25250783p252540... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

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

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

Ryan Ingram wrote:

On Tue, Sep 8, 2009 at 12:44 PM, Daniil Elovkov 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

Am Dienstag 15 September 2009 23:13:59 schrieb Cristiano Paris:

On Wed, Sep 2, 2009 at 7:16 AM, zaxis 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

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:Bulat.Ziganshin@gmail.com

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

On Tue, Sep 15, 2009 at 11:38 PM, Daniel Fischer 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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

On Thu, Sep 17, 2009 at 8:36 AM, Ryan Ingram 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.

In test1, the caller specifies "a" and then passes in an object of that type.

The witness?

In test2, the caller must pass in an object which is of all types, and test2 asks for that object to be instantiated at the type "Int"

"of all types" means "a value which belongs to all the sets of all the types", i.e. bottom?

...

...

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

Why?

Informally, because you can't create something that can be any type.

Yes, I misread the initial statement. I missed the "non-bottom" part :)

There's one way that doesn't entirely ignore its argument.

test4 x = seq x 1

But I don't like to talk about that one :)

:) Thank you Ryan, you were very explicative. I may say that the use of the System-F's notation, making everything explicit, clarifies this a bit. Cristiano

Cristiano Paris wrote:

On Wed, Sep 16, 2009 at 7:12 PM, Ryan Ingram 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.

It's not existential, it's rank-2 universal. The first function is saying that "for every type, a, there is a function, test1@a, taking a into Int". This is very different than the second function which says "there is a function, test2, taking values which belong to all types into Int". The test2 function is not polymorphic, instead it takes arguments which are polymorphic. Since _|_ is the only inhabitant of all types, it may be helpful to consider these functions instead: f :: forall a. (a -> a) -> Int g :: (forall a. a -> a) -> Int The function f takes a monomorphic function of type (a->a) for some predefined a. Which a? Well it can be any of them, but it can only be one of them at a time. That is, the invocation of f will make the a concrete. The function g takes a polymorphic function which, being polymorphic, will work for every a. That is, the invocation of g does not make the type concrete; only the invocation of the argument within the body of g will make the type concrete. Moreover, the argument must be able to be made concrete for every a, it can't pick and choose. This is different from existential quantification which means the argument works for some a, but it won't tell us which one. To put it another way, this is a valid definition of g: (\ r -> let _ = r Nothing ; _ r "hello" in 42) Since r is polymorphic, we can use it at two different types. Whereas if we gave this definition for f it wouldn't type check since we can't unify (Maybe a) and String.

...

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

Why?

By definition of Haskell semantics. The only value belonging to all types is _|_ (whether undefined or various exception bottoms). Perhaps it'd make more sense to look at another type. What values inhabit (forall a. Maybe a)? Well _|_ inhabits all types, so it's there. And Nothing doesn't say anything about a, so it's there too since it works for all a. And (Just _|_) is there since Just doesn't say anything about the type a and _|_ belongs to all types so it doesn't say anything about a either. And that's it. Any other value must say something about the type a, thus restricting it, and then it would no longer be universally quantified. -- Live well, ~wren