[Haskell-cafe] GATD and pattern matching

[Dupont Corentin]

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 <daniel.is.fischer at web.de>wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100609/e91fb225/attachment.html