Existencial quantification and polymorphic datatypes

newer
Haddock bug for strict unpacked...

Mauricio

20 Jan 2009 20 Jan '09

5:02 a.m.

Hi, I'm trying, without success, to understand the difference between existencial quantification and polymorphic datatypes. Can you give me a hint, or an example where one is valid and the other is not? Thanks, Maurício

Show replies by date

Lennart Augustsson

20 Jan 20 Jan

5:59 a.m.

New subject: Existencial quantification and polymorphic datatypes

Do you mean difference between data A a = A a and data B = B a -- leaving out the forall ? On Tue, Jan 20, 2009 at 10:02 AM, Mauricio wrote:

...

Hi,

I'm trying, without success, to understand the difference between existencial quantification and polymorphic datatypes. Can you give me a hint, or an example where one is valid and the other is not?

Thanks, Maurício

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Jon Fairbairn

6:01 a.m.

New subject: Existencial quantification and polymorphic datatypes

Mauricio writes:

...

I'm trying, without success, to understand the difference between existencial quantification and polymorphic datatypes.

Polymorphic types are universally quantified; so id:: forall t. t -> t means that id works for every type t. If haskell had a symbol for existential quantification, hid:: exists t. t -> t would mean that hid only works on some type t, but it doesn't say what it is (so you could only ever apply hid to undefined.

...

Can you give me a hint

Because being on the left of an arrow works something like negation, a type like (exists t. t -> t) -> bool can be written as forall t . (t -> t) -> bool -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2008-04-26)

ChrisK

8:06 a.m.

New subject: Existencial quantification and polymorphic datatypes

Mauricio wrote:

...

Hi,

I'm trying, without success, to understand the difference between existencial quantification and polymorphic datatypes. Can you give me a hint, or an example where one is valid and the other is not?

The first thing to ensure you know is that Haskell can have functions (usually in type classes) that have the Perl-like ability to return different types of values depending on the "context". The usual example for this is "fromInteger :: Num a => Integer -> a". Every integer in your source code is put through this function. If the number is used in an Int context then it makes and Int, if use in a Word8 context then it makes a Word8. The other way we talk about the type of context is that this is the type demanded by the user of the value. Concretely: x :: forall a. Num a => a x = fromInteger 1 The type of 'x' is any Num type chosen by the user. The critical thing here is that "fromInteger" does not get to choose the type. This is bounded or constrained polymorphism, the type 'a' is polymorphic but bounded by the Num constraint. Now I can refer to ghc's manual on existential quantification: http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions... So what about wanting to write a function "myNum" that returns some Num type that "myNum" gets to choose instead of the user demanding a type. We can do this with existential types, which usually is used with a data type (often a GADT) and here I call this SomeNum:

...

{-# LANGUAGE ExistentialQuantification #-} import Int import Data.Typeable data SomeNum = forall a. (Typeable a, Num a) => SomeNum a

myNum :: Integer -> SomeNum myNum x | abs x < 2^7 = let i :: Int8 i = fromInteger x in SomeNum i | abs x < 2^31 = let i :: Int32 i = fromInteger x in SomeNum i | otherwise = SomeNum x

display :: SomeNum -> String display (SomeNum i) = show i ++ " :: " ++ show (typeOf i)

main = do putStrLn (display (myNum (2^0))) putStrLn (display (myNum (2^8))) putStrLn (display (myNum (2^32)))

In GHCI I see

...

*Main> main main 1 :: Int8 256 :: Int32 4294967296 :: Integer

In the above you can see the polymorphism of the return type of fromInteger, it returns a Int8 or a Int32. You can see the polymorphism of the argument of "show", it takes an Int8 or Int32 or Integer. The latest ghc-6.10.1 also allows avoiding use of SomeNum, see impredicative-polymorphism: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension... So this next bit is very very new:

...

{-# LANGUAGE ExistentialQuantification, RankNTypes, ImpredicativeTypes #-}

...

displayNum :: [forall a. Num a => Integer -> a] -> String displayNum converts = unlines $ concatMap withF converts where withF :: (forall b. Num b => Integer -> b) -> [String] withF f = [ show (f 1 :: Int8) , show (f (2^10) :: Int32) , show (f (2^32) :: Integer) ]

The first argument to displayNum is a list of an existential type. Before ImpredicativeType this would have required defining and using a data type like SomeNum. So the latest ghc lets one avoid the extra data type. displayNum cannot "demand" any (Num b => Integer->b) function. The list holds SOME functions, but which one is unknowable to displayNum. The first argument of withF is polymorphic and while this requires RankNTypes (or Rank2Types) the type of withF is not existential. In withF the code demands three different types of results from the 'f'. This works because the return type of (f 1) is really (Num b => b) and this is polymorphic and any type 'b' which is a Num can be demanded. This can be tested with

...

putStr $ displayNum [ fromInteger , fromInteger . (2*) , fromInteger . (min 1000) ]

which passes in a list of three different conversion functions. In ghci the result is:

...

1 1024 4294967296 2 2048 8589934592 1 1000 1000

-- Chris

Mauricio

11:56 a.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

...

...
4294967296 :: Integer (...) In the above you can see the polymorphism of the return type of fromInteger, it returns a Int8 or a Int32.

You can see the polymorphism of the argument of "show", it takes an Int8 or Int32 or Integer.

The latest ghc-6.10.1 also allows avoiding use of SomeNum, see impredicative-polymorphism: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension...

Great, thanks! I'm enlightened :) But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a) ? Maurício

Gleb Alexeyev

12:09 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

Mauricio wrote:

...

But how is this:

data SomeNum = forall a. SN a

different from:

data SomeNum = SN (forall a. a)

In the first case the constructor SN can be applied to the monomorphic value of any type, it effectively hides the type of the argument. For example, you can have a list like [SN True, SN "foo", SN 42], because for all x SN x has type SomeNum. In the second case, SN can be applied only to polymorphic values, SN True or SN "foo" won't compile. The only thing that both types have in common - they are both useless. Polymorphic and existential types must have more structure to be useful - you cannot _construct_ SomeNum #2 and you cannot do anything to the value you _extract_ from SomeNum #1.

Gleb Alexeyev

12:19 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

I just thought that the shorter explanation could do better: the difference is in the types of the constructor functions. Code:

...

{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE RankNTypes #-} data SomeNum1 = forall a. SN1 a data SomeNum2 = SN2 (forall a. a)

ghci session: *Main> :t SN1 SN1 :: a -> SomeNum1 *Main> :t SN2 SN2 :: (forall a. a) -> SomeNum2 This is not the whole story, types of the bound variables you get on pattern matching differ too, but this makes the short explanation a bit longer :).

Jake McArthur

21 Jan 21 Jan

2:38 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Gleb Alexeyev wrote: | Mauricio wrote: | |> data SomeNum = SN (forall a. a) | | [...] | | you cannot do anything to the value you extract Maybe. Say you construct (SN x). If you later extract x, you can observe that it terminates (using seq, perhaps), assuming that it does terminate. You still can't really do anything with the value, but you can at least observe something about its computation. The uses of this may be obscure (I can't think of any right now), but I wouldn't say they necessarily don't exist. - - Jake -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkl3eb8ACgkQye5hVyvIUKnGZgCcDvZKVmqcwjdx97MkPu3I5r3n KsUAn0IlCTwyCH5h5QTyDPvM1MkX36Hz =Ocgm -----END PGP SIGNATURE-----

Jonathan Cast

3 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

On Wed, 2009-01-21 at 13:38 -0600, Jake McArthur wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

Gleb Alexeyev wrote: | Mauricio wrote: | |> data SomeNum = SN (forall a. a) | | [...] | | you cannot do anything to the value you extract

Maybe. Say you construct (SN x). If you later extract x, you can observe that it terminates (using seq, perhaps), assuming that it does terminate.

The definition you quoted is equivalent to data SomeNum where SN :: (forall a. a) -> SomeNum So if I say case y of SN x -> ... Then in the sequel (...) I can use x at whatever type I want --- it's polymorphic --- but whatever type I use it at, it cannot terminate. I think you meant to quote the definition data SomeNum = forall a. SN a which is equivalent to data SomeNum where SN :: forall a. a -> SomeNum in which case if I say case y of SN x -> ... then x is a perfectly monomorphic value, whose type happens to be a (fresh) constant distinct from all other types in the program. So I can't do anything useful with x, although as you say, it can be forced with seq. OTOH, you could do exactly the same thing with a normal judgment of type (), if you found a use for it. jcc

Jake McArthur

3:17 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Jonathan Cast wrote: | I think you meant to quote the definition | | data SomeNum = forall a. SN a Quite so. Thanks for clearing that up. - - Jake -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkl3gr8ACgkQye5hVyvIUKmiDgCfeH8fEn0+iDEMlQwtCHtMXAti vSoAnAwYibedZTR1YyzrcC0OTspXsjMX =Vagv -----END PGP SIGNATURE-----

ChrisK

20 Jan 20 Jan

1:10 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

...

Great, thanks! I'm enlightened :)

And no one had to hit you with a stick first!

...

But how is this:

data SomeNum = forall a. SN a

different from:

data SomeNum = SN (forall a. a)

?

At a glance they look the same to me — but only the first is accepted by ghc. There is also the GADT syntax:

...

data SomeNum where SomeNum :: forall a. (Typeable a, Num a) => a -> SomeNum

which is accepted by ghc with the LANGUAGE GADTs extension. The GADT is more than simple syntactic sugar, it allows for easier use this kind of existential type. -- Chris

Mauricio

2:51 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

...

...
But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a)

...

At a glance they look the same to me — but only the first is accepted by ghc.

Following the link you pointed in the last message, I found this at 8.8.4.1: data T a = T1 (forall b. b -> b -> b) a If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't: data T a = forall b. T1 (b->b->b) a (The last one I think I understand well after the previous message, although I see no use for this particular form, since after pattern match there's no other 'b' value to which we could aply that function field.) Link for convenience: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension... Maurício

David Menendez

3:14 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

On Tue, Jan 20, 2009 at 2:51 PM, Mauricio wrote:

...

...
...
But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a)

...
At a glance they look the same to me — but only the first is accepted by ghc.

Following the link you pointed in the last message, I found this at 8.8.4.1:

data T a = T1 (forall b. b -> b -> b) a

If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't:

data T a = forall b. T1 (b->b->b) a

In the first example, T stores a function which works for every type. In the second example, T stores a function which works on a specific type. So with the first definition, you can do something like this: foo :: T1 a -> (Bool, Int) foo (T1 f _) = (f True False, f 1 2) But you can't really do anything useful with the second example.

...

(The last one I think I understand well after the previous message, although I see no use for this particular form, since after pattern match there's no other 'b' value to which we could aply that function field.)

Here's a more useful example of existential quantification: data Stream a = forall b. Stream (b -> a) (b -> b) b head :: Stream a -> a head (Stream h t b) = h b tail :: Stream a -> Stream a tail (Stream h t b) = Stream h t (t b) -- Dave Menendez http://www.eyrie.org/~zednenem/

Luke Palmer

4 p.m.

New subject: Existencial quantification and polymorphic datatypes (actually, components...)

On Tue, Jan 20, 2009 at 1:14 PM, David Menendez wrote:

...

On Tue, Jan 20, 2009 at 2:51 PM, Mauricio wrote:

...
...
...
But how is this: data SomeNum = forall a. SN a different from: data SomeNum = SN (forall a. a)

...
At a glance they look the same to me — but only the first is accepted by ghc.

Following the link you pointed in the last message, I found this at 8.8.4.1:

data T a = T1 (forall b. b -> b -> b) a

The constructor here is irrelevant. The function here can do anything a top-level function of type: something :: b -> b -> b I like to think about quantification in this regard in terms of isomorphisms. Think about what a function of type forall b. b -> b -> b can do. It cannot do anything with its arguments, because it must work on all types, so it only has one choice to make: it can return the first argument, or it can return the second argument. So, forall b. b -> b -> b is isomorphic to Bool. For symmetry, the constructor T1 has type: T1 :: (forall b. b -> b -> b) -> a -> T1 a

...

...
If I understand properly, it can be activated with -XPolymorphicComponents. It's different from my example, but I would like to know what it does that this can't:

data T a = forall b. T1 (b->b->b) a

The constructor T1 here has type: T1 :: forall b. (b -> b -> b) -> a -> T1 a See the difference? You can pass the latter a function of any type you choose, eg. (Int -> Int -> Int) or ((Bool -> Bool) -> (Bool -> Bool) -> (Bool -> Bool)). So when somebody gets a T from you, they have no idea what type the function you gave it was, so they can only use it in limited ways (in this case, nothing useful at all can be done with it). Here's another existential type: data T' a = forall b. T' (b -> a) b Here, a T' contains a value of some type b -- who knows what it is -- and a function to get from that value to an a. Since we don't know anything about b, all we can do is to apply the function. T' a is isomorphic to a. But it might have different operational behavior; e.g. maybe a is a huge list which is cheaply generated from some small generator value (of type b). Then if you pass a T' around, it's the same as passing that big list around, except for you don't cache the results of the list, improving memory performance. It's like inverse memoization. Not all existential types are for inverse memoization, this is just one case. I found it easiest to reason about these with the types of the constructors, and thinking about what non-quantified type they are isomorphic to. Luke

5965

Age (days ago)

5966

Last active (days ago)

List overview

Download

13 comments

9 participants

participants (9)

ChrisK
David Menendez
Gleb Alexeyev
Jake McArthur
Jon Fairbairn
Jonathan Cast
Lennart Augustsson
Luke Palmer
Mauricio