Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-18 Thread TP
Chris Wong wrote:

 data Person :: Gender - * where
 Dead :: Person Gender  -- WHAT DO I PUT HERE
 Alive :: { name :: String
   , weight :: Float
   , father :: Person Gender } - Person Gender
 
 Here's the problem. In the line:
 
 Dead :: Person Gender
 
 you are referring to the Gender *type*, not the Gender kind.
 
 To refer to the kind instead, change this to:
 
 Dead :: forall (a :: Gender). Person a
 
 This means for all types A which have the kind Gender, I can give you
 a Person with that type. The Alive declaration and deriving clause
 can be fixed in a similar way.
 
 Also, to enable the forall syntax, you need to add
 
 {-# LANGUAGE ExplicitForAll #-}
 
 at the top of the file.

Thanks a lot for your help. I did not realize the possible usage of a::b 
to indicate any type a of kind b. So I have adapted my code, and the 
following version is working correctly:


{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: Person (a :: Gender)
Alive :: { name :: String
  , weight :: Float
  , father :: Person (a::Gender) } - Person (b :: Gender)

deriving instance Show (Person (a::Gender))

main = do

let a = Alive Joe 60 Dead :: Person Female
let b = Alive Jim 70 a :: Person Male


However, I have not managed to make the version with forall work. Below, the 
first occurrence of forall is ok, but the three following yield error.


{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExplicitForAll #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: forall (a :: Gender). Person a
Alive :: { name :: String
  , weight :: Float
  , father :: forall (a :: Gender). Person a } - forall (b :: 
Gender). Person b

deriving instance Show (forall (a :: Gender). Person a)

main = do

let a = Alive Joe 60 Dead :: Person Female
let b = Alive Jim 70 a :: Person Male


Thanks,

TP



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


Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-18 Thread Denis Kasak
On 18 May 2013 11:16, TP paratribulati...@free.fr wrote:
snip

   However, I have not managed to make the version with forall work.
Below, the
   first occurrence of forall is ok, but the three following yield error.

   
   {-# LANGUAGE GADTs #-}
   {-# LANGUAGE StandaloneDeriving #-}
   {-# LANGUAGE DataKinds #-}
   {-# LANGUAGE KindSignatures #-}
   {-# LANGUAGE FlexibleInstances #-}
   {-# LANGUAGE ExplicitForAll #-}

   data Gender = Male | Female
   data Person :: Gender - * where
   Dead :: forall (a :: Gender). Person a
   Alive :: { name :: String
 , weight :: Float
 , father :: forall (a :: Gender). Person a } - forall (b
::
   Gender). Person b

The foralls should be in front of all the data constructor parameters, like
with the
Dead constructor, since you want to quantify a and b over the whole type
signature:

data Person :: Gender - * where
Dead :: forall (a :: Gender). Person a
Alive :: forall (a :: Gender) (b :: Gender).
 { name :: String
 , weight :: Float
 , father :: Person a } - Person b

   deriving instance Show (forall (a :: Gender). Person a)

Again, you should quantify over Show as well:

deriving instance forall (a :: Gender). Show (Person a)

Note that all of this would work even without explicit quantification since
you
have already specified that Person accepts an argument of kind Gender. In
other
words, this works as expected:

data Person :: Gender - * where
Dead :: Person a
Alive :: { name :: String
 , weight :: Float
 , father :: Person b } - Person a

deriving instance Show (Person a)

You also probably want father :: Person Male, since a father cannot be
Female
(presumably!).

Regards,

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


Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-18 Thread TP
Denis Kasak wrote:

 Note that all of this would work even without explicit quantification
 since you
 have already specified that Person accepts an argument of kind Gender. In
 other
 words, this works as expected:
 
 data Person :: Gender - * where
 Dead :: Person a
 Alive :: { name :: String
  , weight :: Float
  , father :: Person b } - Person a
 
 deriving instance Show (Person a)

Thanks so much, it is now perfectly clear. A lot of things learned with this 
dummy example.

TP




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


[Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-17 Thread TP
Hi everybody,

I have a question about deriving automatically a Show instance when using 
GADT.
It works in this situation:


{-# LANGUAGE GADTs #-}

data Male
data Female

data Person gender where
Dead :: Person gender
Alive :: { name :: String
  , weight :: Float
  , father :: Person gender } - Person gender
 deriving Show

main = do

let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male

print a
print b


Indeed:

$ runghc test_show.hs 
Alive {name = Joe, weight = 60.0, father = Dead}
Alive {name = Jim, weight = 70.0, father = Alive {name = Joe, weight = 
60.0, father = Dead}}


But when I replace father :: Person gender by father :: Person gender2 
in the code (this is one of the advantages of GADT: with a classical 
algebraic data type declaration, gender2 would have to be a type variable 
for the data type), I obtain:

Can't make a derived instance of `Show (Person gender)':
  Constructor `Alive' must have a Haskell-98 type
  Possible fix: use a standalone deriving declaration instead
In the data declaration for `Person'

So I modify my code by removing deriving Show, and adding the line:

instance Show (Person gender)


But now, I obtain:

$ runghc test_show.hs 
GHC stack-space overflow: current limit is 536870912 bytes.
Use the `-Ksize' option to increase it.

Why (I imagine this is because there is an infinite loop in the construction 
of the show function)? Is there any workaround?

Thanks,

TP


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


Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-17 Thread Adam Gundry
Hi TP,

On 17/05/13 15:32, TP wrote:
| [...]
|
| So I modify my code by removing deriving Show, and adding the line:
| 
| instance Show (Person gender)
| 
|
| But now, I obtain:
|
| $ runghc test_show.hs
| GHC stack-space overflow: current limit is 536870912 bytes.
| Use the `-Ksize' option to increase it.
|
| Why (I imagine this is because there is an infinite loop in the
construction
| of the show function)? Is there any workaround?

To use standalone deriving, you need to write

 deriving instance Show (Person gender)

and everything will work fine. By writing

 instance Show (Person gender)

you are instead giving an instance with no methods, and the default
methods in the Show class contain a loop (so that one can define either
show or showsPrec).

Hope this helps,

Adam

P.S. You might like to check out the new DataKinds extension, which
would allow Male and Female to be data constructors rather than type
constructors.


-- 
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.

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


Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-17 Thread TP
Adam Gundry wrote:

[...]
 To use standalone deriving, you need to write
 
 deriving instance Show (Person gender)
 
 and everything will work fine. By writing
 
 instance Show (Person gender)
 
 you are instead giving an instance with no methods, and the default
 methods in the Show class contain a loop (so that one can define either
 show or showsPrec).

Thanks a lot. I did not remember that Standalone Deriving has a meaning as 
a GHC extension. My idea was correct, but the employed syntax was incorrect. 
Just for reference (future Google search by others), the corresponding link 
in the GHC documentation:

http://www.haskell.org/ghc/docs/7.6.2/html/users_guide/deriving.html

 P.S. You might like to check out the new DataKinds extension, which
 would allow Male and Female to be data constructors rather than type
 constructors.

Thanks a lot for pointing out this subject (it compells me to work on it - I 
am not an advanced user of GHC).
I have just tried to understand all this stuff about type and data 
constructor promotion:

http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/promotion.html

If I understand well, your idea is to avoid letting someone write:

let a = Alive Joe 60 Dead :: Person Int

which is nonsense (a Person cannot have a gender of type Integer), but 
legal code.
I have tried to use the technique described at the beginning of the article 
Given Haskell a Promotion, but I'm stuck. See the code below. My problem 
is that now Gender is a kind, no more a type, such that I cannot use it in 
the type definition of the GADT; but I am compelled to write something after 
::, and I cannot write for instance Dead :: Person Male because I want a 
dead person to be either a man or woman, of course. In fact, what I need is 
Gender both as a type and as a kind, if I am correct? What do I miss?

So the following version does not work:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

data Gender = Male | Female

data Person :: Gender - * where
Dead :: Person Gender  -- WHAT DO I PUT HERE
Alive :: { name :: String
  , weight :: Float
  , father :: Person Gender } - Person Gender

deriving instance Show (Person Gender)

main = do

let a = Alive Joe 60 Dead :: Person Male
let b = Alive Jim 70 a :: Person Male

print a
print b


How to modify it?

Thanks a lot,

TP


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


Re: [Haskell-cafe] question about GADT and deriving automatically a Show instance

2013-05-17 Thread Chris Wong
On Sat, May 18, 2013 at 9:11 AM, TP paratribulati...@free.fr wrote:

 So the following version does not work:
 
 [..]
 data Person :: Gender - * where
 Dead :: Person Gender  -- WHAT DO I PUT HERE
 Alive :: { name :: String
   , weight :: Float
   , father :: Person Gender } - Person Gender

Here's the problem. In the line:

Dead :: Person Gender

you are referring to the Gender *type*, not the Gender kind.

To refer to the kind instead, change this to:

Dead :: forall (a :: Gender). Person a

This means for all types A which have the kind Gender, I can give you
a Person with that type. The Alive declaration and deriving clause
can be fixed in a similar way.

Also, to enable the forall syntax, you need to add

{-# LANGUAGE ExplicitForAll #-}

at the top of the file.

Chris


--
Chris Wong, fixpoint conjurer
  e: lambda.fa...@gmail.com
  w: http://lfairy.github.io/

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