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: $ 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 `-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? Thanks, TP
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 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.
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
On Sat, May 18, 2013 at 9:11 AM, TP
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.fairy@gmail.com w: http://lfairy.github.io/
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
On 18 May 2013 11:16, TP
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
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
participants (4)
-
Adam Gundry -
Chris Wong -
Denis Kasak -
TP