[Haskell-cafe] use of the GHC universal quantifier

[Galchin, Vasili]

Hi Ryan,

   Please see below.

Vasili


On Wed, Jul 9, 2008 at 4:03 AM, Ryan Ingram <ryani.spam at gmail.com> wrote:

> Try {-# LANGUAGE RankNTypes #-}?

      vigalchin at ubuntu:~/FTP/Haskell/hsql-1.7$ runhaskell Setup.lhs build
Preprocessing library hsql-1.7...
Building hsql-1.7...
[1 of 2] Compiling Database.HSQL.Types ( Database/HSQL/Types.hs,
dist/build/Database/HSQL/Types.o )

Database/HSQL/Types.hs:67:0:
    Can't make a derived instance of `Typeable SqlError'
      (You need -XDeriveDataTypeable to derive an instance for this class)
    In the data type declaration for `SqlError'


>
>
> "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

        Classical logic opposed to intuitionistic logic?
<<<<<<<<<<<<<<<<<<<<<<<<<<

>
>
> 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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080710/957e5aba/attachment.htm