Deducing Show for GADTs
Hi. I came a cross the following phenomena which, at least to me, occurs kind of awkward. The code below : data MyData a where DC1 :: (Show a ) => a -> MyData a instance Show (MyData a) where show (DC1 a ) = show a yields the ghci error : 'Could not deduce (Show a) from the context (Show (MyData a))' Adding a Show restriction for the instantiation as in instance Show a => Show (MyData a ) where show (DC1 a ) = show a makes the type checker happy. However, this means that all parametrised values over MyData must have a Show type which isn't necessarily what one wants. I would also like to point out that adding a 'wrapper type' as in data Wrap a = Wrap a data MyData a where DC1 :: (Show a ) => a -> MyData (Wrap a) instance Show (MyData a ) where show (DC1 a ) = show a works fine. Even though 'Wrap' does not derive Show. So, if anyone can give me some hints about the reason for this, I will appreciate it :) Thanks /Joel
On Wed, Jun 28, 2006 at 11:52:51AM +0200, Joel Bjrnson wrote:
Hi. I came a cross the following phenomena which, at least to me, occurs kind of awkward. The code below:
data MyData a where DC1 :: (Show a ) => a -> MyData a
GADTs don't yet work right with classes. :( The above, however, doesn't need to be expressed as a GADT, I believe you can write something like: data MyData a = (forall a. Show a) => DC1 a which (this is untested) should do what you want. -- David Roundy
On 6/28/06, David Roundy
On Wed, Jun 28, 2006 at 11:52:51AM +0200, Joel Bjrnson wrote:
Hi. I came a cross the following phenomena which, at least to me, occurs kind of awkward. The code below:
data MyData a where DC1 :: (Show a ) => a -> MyData a
GADTs don't yet work right with classes. :( The above, however, doesn't need to be expressed as a GADT, I believe you can write something like:
data MyData a = (forall a. Show a) => DC1 a
which (this is untested) should do what you want.
Only if "what he wants" is something that type checks, but doesn't do the same thing. ;-) In Joel's definition of MyData, values constructed with DC1 applied to a value of type b will have type MyData b. In your definition they will have type MyData a, for any a. In other words, your definition would be identical to the GADT data MyData a where DC1 :: forall a b . (Show b) => b -> MyData a As to Joel's question, this seems really really weird. In particular since adding the completely useless wrapper type solves the problem. In fact, giving DC1 any return type other than MyData a solves the problem. This has to be a bug of some sort. /Niklas
Joel Björnson wrote:
Hi. I came a cross the following phenomena which, at least to me, occurs kind of awkward. The code below :
data MyData a where DC1 :: (Show a ) => a -> MyData a
instance Show (MyData a) where show (DC1 a ) = show a
yields the ghci error : 'Could not deduce (Show a) from the context (Show (MyData a))'
...
I would also like to point out that adding a 'wrapper type' as in
data Wrap a = Wrap a
data MyData a where DC1 :: (Show a ) => a -> MyData (Wrap a)
instance Show (MyData a ) where show (DC1 a ) = show a
works fine. Even though 'Wrap' does not derive Show.
So, if anyone can give me some hints about the reason for this, I will appreciate it :)
I think your example is tranlated to something like this, making an new existential type for the "a" in Wrap a, and adding an equality constraint saying that the result type has to match a. data MyData a forall b . (Show b, a = Wrap b) => DC1 a That will work because b is an existential type, and pattern matching on existentially typed constructors lets you use the constraints (dictionaries) they carry around. I'm not sure how GHC works now, but the paper "System F with TypeEquality Conversions" says GHC is eventually going to change to an intermediate representation like this. You can even put a constraint on the entire argument to the type constructor, just as long as your constructor constraints that argument. data Ex a where Ex :: Show (a,b) => (a,b) -> Ex (a,b) It's more confusing when some parameters are constrained and some are not - it seems that a class constraint has to mention at least one constrained type to work. To finish your program, you could directly write the encoding that uses type equality. This GADT is evidence of type equality: data Equal a b where Refl :: Equal a a With it you can define data MyData a where DC1 :: (Show b) => Equal a b -> b -> MyData a and use values like this instance Show (MyData a) where show (DC1 Refl x) = show x It works: *Main> show (DC1 Refl [1,2]) "[1,2]" Brandon
participants (4)
-
Brandon Moore -
David Roundy -
Joel Björnson -
Niklas Broberg