[Haskell-cafe] GATD and pattern matching
Dupont Corentin
corentin.dupont at gmail.com
Wed Jun 9 16:28:47 EDT 2010
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
More information about the Haskell-Cafe
mailing list