[Haskell-cafe] Re: Existencial quantification and polymorphic datatypes

[ChrisK]

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.html#existential-quantification

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-extensions.html#impredicative-polymorphism

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