Re: [Haskell-cafe] 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 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
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
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
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
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
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
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