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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
