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