Thanks for your response. How would you do it? I design this GATD for a game i'm making:
data Obs a where Player :: Obs Integer Turn :: Obs Integer Official :: Obs Bool Equ :: Obs a -> Obs a -> Obs Bool --woops!! Plus :: (Num a) => Obs a -> Obs a -> Obs a Time :: (Num a) => Obs a -> Obs a -> Obs a Minus :: (Num a) => Obs a -> Obs a -> Obs a Konst :: a -> Obs a And :: Obs Bool -> Obs Bool -> Obs Bool Or :: Obs Bool -> Obs Bool -> Obs Bool
For example I can design an Observable like that: myObs = Player `Equ` (Konst 1) `And` Official These Observables will then be processed during gameplay. I would like to be able to do in ghci:
show myObs Player `Equ` (Konst 1) `And` Official
and:
myObs == myObs True
Corentin
On Wed, Jun 9, 2010 at 9:10 PM, Daniel Fischer
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