TP | 17 May 16:32 2013
Picon

question about GADT and deriving automatically a Show instance

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:

(Continue reading)

Adam Gundry | 17 May 17:44 2013
Picon
Picon

Re: question about GADT and deriving automatically a Show instance

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 `-K<size>' 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
(Continue reading)

TP | 17 May 23:11 2013
Picon

Re: question about GADT and deriving automatically a Show instance

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:
(Continue reading)

Chris Wong | 18 May 00:28 2013
Picon

Re: question about GADT and deriving automatically a Show instance

On Sat, May 18, 2013 at 9:11 AM, TP <paratribulations <at> 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.
(Continue reading)

TP | 18 May 11:16 2013
Picon

Re: question about GADT and deriving automatically a Show instance

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 
(Continue reading)

Denis Kasak | 18 May 12:19 2013
Picon

Re: question about GADT and deriving automatically a Show instance

On 18 May 2013 11:16, TP <paratribulations <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 18 May 16:23 2013
Picon

Re: question about GADT and deriving automatically a Show instance

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

Gmane