[Haskell-cafe] Deducing Show for GADTs
Brandon Moore
brandonm at yahoo-inc.com
Wed Jun 28 13:00:08 EDT 2006
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
More information about the Haskell-Cafe
mailing list