what is a difference between existential quantification and polymorhic field?
Hello haskell-cafe, now i'm reading Haskell' proposals and found that these two things considered as different: http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification http://hackage.haskell.org/trac/haskell-prime/wiki/PolymorphicComponents can you please explain me what is the difference between data Ex = forall a. Num a => Ex a and data Po = Po (forall a. Num a => a) ? -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
[apologies to Bulat for the repeat posting] On Thu, Sep 21, 2006 at 12:05:23PM +0400, Bulat Ziganshin wrote:
now i'm reading Haskell' proposals and found that these two things considered as different:
http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification http://hackage.haskell.org/trac/haskell-prime/wiki/PolymorphicComponents
can you please explain me what is the difference between
data Ex = forall a. Num a => Ex a
and
data Po = Po (forall a. Num a => a)
Consider the types of the constructors: Ex :: forall a. (Num a) => a -> Ex Po :: (forall a. (Num a) => a) -> Po
Hello Ross, Thursday, September 21, 2006, 12:55:40 PM, you wrote:
data Ex = forall a. Num a => Ex a
and
data Po = Po (forall a. Num a => a)
Consider the types of the constructors:
Ex :: forall a. (Num a) => a -> Ex Po :: (forall a. (Num a) => a) -> Po
sorry, Ross, can you give me a more detailed explanation? it seems that Po argument is existential by itself, but i don't understand that all this mean also, ghc66 adds impredicative polymorphism. how it differs from unqualified existentials? -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
Hello Ross, Thursday, September 21, 2006, 12:55:40 PM, you wrote:
data Ex = forall a. Num a => Ex a
and
data Po = Po (forall a. Num a => a)
Consider the types of the constructors:
Ex :: forall a. (Num a) => a -> Ex Po :: (forall a. (Num a) => a) -> Po
sorry, Ross, can you give me a more detailed explanation? it seems that Po argument is existential by itself,
The Po argument is a polymorphic function, not an existential. As I understand it, the constructor Ex _is_ a polymorphic function, whereas the constructor Po (only) _takes_as_argument_ a polymorphic function. In the latter case you store a polymorphic function inside your data, whereas in the former case you construct (monomorphic) data in a polymorphic way, which means that during the process you loose the concrete type of the argument. Ben
Hello Bullat,
now i'm reading Haskell' proposals and found that these two things considered as different:
http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification http://hackage.haskell.org/trac/haskell-prime/wiki/PolymorphicComponents
can you please explain me what is the difference between
data Ex = forall a. Num a => Ex a
and
data Po = Po (forall a. Num a => a)
With existencial types you know what what the type of the thing you are packing is:
t = Ex (3 :: Int)
and you forget about it once it is packed. However, with polymophic components the following is a type error
t = Po ( 3 :: Int)
because you are required to provide a polymorphic value (forall a . Num a => a) and you have given it a value Int. However, the following is valid:
t1 = Po 3
since (3 :: forall a . Num a => a). So, perhaps an easy way to think about existencials is that they are almost like:
data Ex a = Ex a
except that the type "a" is lost as soon as you construct such a value. Where does this make a difference? Try the following two definitions:
addPo :: Po -> Po -> Po addPo (Po x) (Po y) = Po (x + y)
addEx :: Ex -> Ex -> Ex addEx (Ex x) (Ex y) = Ex (x + y)
The first one works, the second one doesn't. The reason that the first works is because "x" and "y" are polymorphic and thus they can be unified. This is more/less equivallent to:
addPo' :: (forall a . Num a => a) -> (forall a . Num a => a) -> (forall a . Num a => a) addPo' x y = x + y
The second does *not* work because when you created the values for the existencials you assumed some concrete types. So, "x" could be an Integer and "y" could be a Float and therefore, you should not be allowed to perform this operation.
also, ghc66 adds impredicative polymorphism. how it differs from unqualified existentials?
I have not tried ghc66, but I think one of the things you should be able to do and that is perhaps helpful for understanding existencial is:
myList :: [forall a . Num a => a] myList = [3 :: Int, 4 :: Float, 6 :: Integer]
which in previous versions of GHC would need to be written as:
myList :: [Ex] myList = [Ex (3 ::Int), Ex (4 :: Float), Ex (6 :: Integer)]
Hope this helps. Cheers, Bruno Oliveira
Hello Bullat,
also, ghc66 adds impredicative polymorphism. how it differs from unqualified existentials?
I have not tried ghc66, but I think one of the things you should be able to do and that is perhaps helpful for understanding existencial is:
myList :: [forall a . Num a => a] myList = [3 :: Int, 4 :: Float, 6 :: Integer]
which in previous versions of GHC would need to be written as:
myList :: [Ex] myList = [Ex (3 ::Int), Ex (4 :: Float), Ex (6 :: Integer)]
I took a look at the documentation and I think I told you the wrong thing here. I think this should be equivallent to:
myList :: [Po] myList = [Po 3, Po 4, Po 6]
which, in this case wouldn't be too useful (would it?). Having structures with polymorphic components is more useful when you have functions. The example they give is:
f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) f (Just g) = Just (g [3], g "hello") f Nothing = Nothing
However, the following (which would be the right way to express my example) would be handy to have as well:
myList :: [exists a . Num a => a] myList = [3 :: Int, 4 :: Float, 6 :: Integer]
but I don't think this is available in GHC 6.6. Can anyone confirm this? Cheers, Bruno Oliveira
participants (4)
-
Benjamin Franksen -
Bruno Oliveira -
Bulat Ziganshin -
Ross Paterson