[Haskell-cafe] use of the GHC universal quantifier

[Ryan Ingram]

Try {-# LANGUAGE RankNTypes #-}?

"forall" does denote a universal quantifier, but because the 'implies'
of the function arrow, in logic, includes negation, you can use it to
emulate existential quantifiers.

> data Existential = forall a. Ex a

The type of the constructor Ex:
  Ex :: forall a. a -> Existential

Pattern matching on Ex brings "a" back into scope (with no information
about it, so this type isn't that useful on its own):

> use (Ex x) = 0 -- can't recover any useful information about x
> sample = Ex "sample"

However, you can use existential types to encode additional
information about the included data; for example:

> -- Ex2 :: forall a. Show a => a -> Exist2
> data Exist2 = forall a. Show a => Ex2 a

Now, pattern matching on Ex2 brings the Show instance into scope as well:

> sample2 = Ex2 "sample2"
> use2 (Ex2 x) = show x

You can also use higher rank polymorphism to encode existential types:

> -- Ex3 :: (forall a. (forall b. Show b => b -> a) -> a) -> Exist3
> -- note the rank-3 type on Ex3!
> newtype Exist3 = Ex3 (forall a. (forall b. Show b => b -> a) -> a)

> sample3 = Ex3 (\k -> k "sample3")
> use3 (Ex3 f) = f (\x -> show x)

  -- ryan

2008/7/8 Galchin, Vasili <vigalchin at gmail.com>:
> Hello,
>
>      It seems to me by its name that "forall" denotes a logical universal
> quantifier. In any case, hsql-1.7/Database/HSQL/Types.hs uses "forall" at
> line #134. I got a nasty build so I added {-# LANGUAGE
> ExistentialQuantification #-} at the top of the module. Now I get the
> following a coupleof lines up:
>
> Database/HSQL/Types.hs:131:5:
>     Illegal polymorphic or qualified type: forall a.
>                                            Int
>                                            -> FieldDef
>                                            -> FieldDef
>                                            -> CString
>                                            -> Int
>                                            -> IO a
>                                            -> IO a
>     In the definition of data constructor `Statement'
>     In the data type declaration for `Statement'
>
> If seems that GHC doesn't like "a". Why?
>
> Kind regards, Vasili
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>