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