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 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

Hello Maciej, i tried this out, but it didn't worked. Daniel, I added a (Show a) constraint to Equal:

data Obs a where Player :: Obs Integer Turn :: Obs Integer Official :: Obs Bool Equ :: (Show a, Eq a) => 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

It works for the Show instance, but not Eq. By the way, shouldn't the Show constraint be on the instance and not on the datatype declaration? I'd prefer to keep the datatype as generic as possible... There is really no way to make my Obs datatype an instance of Eq and Show?? I searched around a way to add type information on the pattern match like:

instance Show t => Show (Obs t) where show (Equal (a::Obs t) (b::Obs t)) = (show a) ++ " Equal " ++ (show b) show (Plus a b) = (show a) ++ " Plus " ++ (show b)

But it doesn't work. thanks for your help, Corentin On Thu, Jun 10, 2010 at 2:47 AM, Maciej Piechotka wrote:

On Wed, 2010-06-09 at 22:28 +0200, Dupont Corentin wrote:

...

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

Actually woops is here. Make it for example

Const :: (Show a, Eq a, ...) => 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

Regards

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Thu, Jun 10, 2010 at 11:14 PM, Daniel Fischer wrote:

On Thursday 10 June 2010 22:01:38, Dupont Corentin wrote:

...

Hello Maciej, i tried this out, but it didn't worked.

Daniel,

I added a (Show a) constraint to Equal:

...

data Obs a where Player :: Obs Integer Turn :: Obs Integer Official :: Obs Bool Equ :: (Show a, Eq a) => 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

It works for the Show instance, but not Eq. By the way, shouldn't the Show constraint be on the instance and not on the datatype declaration?

Can't be here, because of Equ :: Obs a -> Obs a -> Obs Bool

You forget the parameter a, and you can't recover it in the instance declaration. So you have to provide the Show instance for a on construction, i.e. put the constraint on the data constructor.

Anyway, is my Obs construction revelant at all? What i want to do is to provide an EDSL to the user to test things about the state of the game (for the Nomic game i'm making). Obs will be then embedded in another EDSL to construct Nomic's rules.

...

I'd prefer to keep the datatype as generic as possible...

There is really no way to make my Obs datatype an instance of Eq and Show??

Show can work (should with the constraint on Equ), Eq is hairy.

instance Show t => Show (Obs t) where show (Equ a b) = show a ++ " `Equal` " ++ show b show (Plus a b) = ... show (Konst x) = "Konst " ++ show x ...

For an Eq instance, you have the problem that

Equ (Konst True) (Konst False) and Equ Player Turn

both have the type Obs Bool, but have been constructed from different types, so you can't compare (Konst True) and Player. I don't see a nice way to work around that.

These is a dirty way: compare the string representation of the rules. They should be unique. Corentin

On Fri, Jun 11, 2010 at 12:46 AM, Felipe Lessa wrote:

 eqTypeable :: (Typeable a, Eq a, Typeable b, Eq b) => a -> b -> Bool  eqTypeable x y = case cast y of                     Just y' -> x == y'                     Nothing -> False

...or indeed: eqTypeable x y = cast x == Just y

Thanks all, it works fine (see below). I lamentably try to make the same for show:

showTypeable :: (Typeable a) => a -> String showTypeable x = case cast x of Just x' -> show x' Nothing -> ""

Because it really upsets me to add this show constraints to the Equ constructor ;) what if i want to make an Obs instance with non showable elements, with no intention to show it of course? Corentin

instance Typeable1 Obs where typeOf1 _ = mkTyConApp (mkTyCon "Obs") []

(===) :: (Typeable a, Typeable b, Eq b) => a -> b -> Bool (===) x y = cast x == Just y

data Obs a where Player :: Obs Player Official :: Obs Bool Equ :: (Eq a, Show a, Typeable a) => Obs a -> Obs a -> Obs Bool 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 And :: Obs Bool -> Obs Bool -> Obs Bool Or :: Obs Bool -> Obs Bool -> Obs Bool Not :: Obs Bool -> Obs Bool Konst :: (Show a, Eq a) => a -> Obs a

instance Show t => Show (Obs t) where show Player = "Player" show Official = "Official" show (Equ a b) = (show a) ++ " Eq " ++ (show b) show (Plus a b) = (show a) ++ " Plus " ++ (show b) show (Minus a b) = (show a) ++ " Minus " ++ (show b) show (Time a b) = (show a) ++ " Time " ++ (show b) show (Konst a) = " (Konst " ++ (show a) ++ ")" show (And a b) = (show a) ++ " And " ++ (show b) show (Or a b) = (show a) ++ " Or " ++ (show b) show (Not a) = " (Not " ++ (show a) ++ ")"

instance Eq t => Eq (Obs t) where Player == Player = True Official == Official = True Equ a b == Equ c d = (a,b) === (c,d) Plus a b == Plus c d = (a == c) && (b == d) Minus a b == Minus c d = (a == c) && (b == d) Time a b == Time c d = (a == c) && (b == d) And a b == And c d = (a == c) && (b == d) Or a b == Or c d = (a == c) && (b == d) Not a == Not b = (a == b) Konst a == Konst b = a == b _ == _ = False

On Friday, June 11, 2010, Felipe Lessa wrote:

On Sat, Jun 12, 2010 at 12:13:14AM +0200, Dupont Corentin wrote:

...

Thanks all, it works fine (see below).

I lamentably try to make the same for show:

...

showTypeable :: (Typeable a) => a -> String showTypeable x = case cast x of                      Just x' -> show x'                      Nothing -> ""

Because it really upsets me to add this show constraints to the Equ constructor ;) what if i want to make an Obs instance with non showable elements, with no intention to show it of course?

Ad hoc solution:

 class MaybeShow a where    maybeShow :: a -> Maybe String

 instance Show a => MaybeShow a where    maybeShow = Just . show

 instance MaybeShow a where    maybeShow = Nothing

 data MyData where    Something :: MaybeShow a => a -> MyData

 instance MaybeShow MyData where    maybeShow (Something x) =      fmap (\s -> "Something (" ++ s ++ ")") (maybeShow x)

Hahahaha :).  Try to guess without using GHC/GHCi:

 1) Which extensions are required to make the code compile.

OverlappingInstances (of course), and IncoherrentInstances, since neither instance is more specific than the other.

 2) After compiled, if it works as intended or not.

It's hard for me to concieve of a situation where something requiring IncoherrentInstances is work as intended, but maybe that's a failure of imagtination. -Antoine

Felipe Lessa wrote:

Well, I guess it can't be compiled at all :( [...] T.lhs:4:12: Duplicate instance declarations: instance [incoherent] (Show a) => MaybeShow a -- Defined at T.lhs:4:12-32 instance [incoherent] MaybeShow a -- Defined at T.lhs:7:12-22

Indeed, it can't be compiled because contexts don't work like that :)

I think this solution still requires OverlappingInstances and UndecidableInstances.

The standard solution for this kind of thing is to use a newtype wrapper to capture the Show constraint, define the Nothing instance for @a@, and use IncoherentInstances. It's ugly, but it works... mostly. It works best if you're in an architecture where everything is a functor--- e.g., if you're using the Data Types a la Carte[1] trick. That way you can enforce the discipline of using the newtype wrapper, since you'll have to be using some kind of functor wrapper to get things to typecheck. Otherwise, it can be too easy to forget to tag something as Showable, and then you'll end up using the default Nothing instance when you didn't mean to. [1] http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf -- Live well, ~wren