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

Tue Jan 20 08:06:11 EST 2009

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

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

> {-# 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
>         | abs x < 2^31 = let i :: Int32
>                              i = fromInteger x
>         | 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:

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

```