[Haskell-cafe] GATD and pattern matching
Daniel Fischer
daniel.is.fischer at web.de
Wed Jun 9 15:10:47 EDT 2010
On Wednesday 09 June 2010 20:37:22, Dupont Corentin wrote:
> Hello,
>
> I am making a little GATD:
> > {-# LANGUAGE GADTs#-}
> >
> > data Obs a where
> > Equal :: Obs a -> Obs a -> Obs Bool
> > Plus :: (Num a) => Obs a -> Obs a -> Obs a
>
> (etc..)
>
> > instance Show t => Show (Obs t) where
> > show (Equal a b) = (show a) ++ " Equal " ++ (show b)
> > show (Plus a b) = (show a) ++ " Plus " ++ (show b)
> >
> > instance Eq t => Eq (Obs t) where
> > a `Equal` b == c `Equal` d = (a == c) && (b == d)
> > a `Plus` b == c `Plus` d = (a == c) && (b == d)
>
> The Equal constructor causes me problems, while the Plus is fine:
>
> test3.lhs:8:26:
> Could not deduce (Show a) from the context (t ~ Bool)
> arising from a use of `show' at test3.lhs:8:26-31
> Possible fix:
> add (Show a) to the context of the constructor `Equal'
> In the first argument of `(++)', namely `(show a)'
> In the expression: (show a) ++ " Equal " ++ (show b)
> In the definition of `show':
> show (Equal a b) = (show a) ++ " Equal " ++ (show b)
>
>
> I guess this is because GADT refines type with pattern matching.
> Since Equal return type is Obs Bool and not Obs a, it cannot bind the
> type variable a to belong to Show.
Right. You can have
(+ 3) `Equal` sin :: Obs Bool
, but how would you show it?
You could add a (Show a) constraint to Equal.
>
> I don't see how to precise the type in the pattern match.
>
> I have another problem:
>
> test3.lhs:12:41:
> Couldn't match expected type `a' against inferred type `a1'
> `a' is a rigid type variable bound by
> the constructor `Equal' at test3.lhs:12:8
> `a1' is a rigid type variable bound by
> the constructor `Equal' at test3.lhs:12:23
> Expected type: Obs a
> Inferred type: Obs a1
> In the second argument of `(==)', namely `c'
> In the first argument of `(&&)', namely `(a == c)'
((+ 3) `Equal` sin) == (True `Equal` False)
Doesn't work.
And you can't make it work, because in
(a `Equal` b) == (c `Equal` d)
, a and b have the same type t1, and c and d have the same type t2 but the
two types t1 and t2 are generally different, so calling (==) on a and c has
no chance to type-check. With Equal forgetting the type parameter of its
arguments, I don't think it's possible.
>
>
> Cheers,
> Corentin
More information about the Haskell-Cafe
mailing list