Re: [Haskell-cafe] use of the GHC universal quantifier

2008-07-10 Thread Galchin, Vasili 
Hi Ryan,

   Please see below.

Vasili


On Wed, Jul 9, 2008 at 4:03 AM, Ryan Ingram [EMAIL PROTECTED] wrote:

 Try {-# LANGUAGE RankNTypes #-}?

  [EMAIL PROTECTED]:~/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 [EMAIL PROTECTED]:
  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@haskell.org
  http://www.haskell.org/mailman/listinfo/haskell-cafe
 
 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] use of the GHC universal quantifier

2008-07-09 Thread 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 [EMAIL PROTECTED]:
 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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] use of the GHC universal quantifier

2008-07-08 Thread Galchin, Vasili 
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe