Hello Haskellers, I'm having trouble writing a Read Instance for my GATD. Arg this GATD!! It causes me more problems that it solves ;) Especially with no automatic deriving, it adds a lot of burden to my code.
data Obs a where ProposedBy :: Obs Int -- The player that proposed the tested rule Turn :: Obs Turn -- The current turn Official :: Obs Bool -- whereas the tested rule is official 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 :: a -> Obs a
instance Read a => Read (Obs a) where readPrec = (prec 10 $ do Ident "ProposedBy" <- lexP return (ProposedBy)) +++ (prec 10 $ do Ident "Official" <- lexP return (Official)) (etc...)
Observable.lhs:120:8: Couldn't match expected type `Int' against inferred type `Bool' Expected type: ReadPrec (Obs Int) Inferred type: ReadPrec (Obs Bool) Indeed "ProposedBy" does not have the same type that "Official". Mmh how to make it all gently mix altogether? Best, Corentin
Hi Corentin I think Oleg Kiselyov is parsing / reading into a GADT here: http://okmij.org/ftp/tagless-final/tagless-typed.html See the section - Metatypechecking: Staged Typed Compilation into GADT using typeclasses http://okmij.org/ftp/Haskell/staged/TypeCheck.hs http://okmij.org/ftp/Haskell/staged/TermLift.hs His solution requires quite a bit of machinery - Template Haskell, a TypeCheck type class... Best wishes Stephen
It turns out that defining Read is somewhat tricky to do for a GADT.
Gershom Bazerman has some very nice slides on how to survive the process by
manual typechecking (much in the spirit of Oleg's meta-typechecking code
referenced by Stephen's follow up below)
He presented them at hac-phi this time around.
I will check with him to see if I can get permission to host them somewhere
and post a link to them here.
-Edward Kmett
On Fri, Jun 25, 2010 at 5:04 AM,
Hello Haskellers,
I'm having trouble writing a Read Instance for my GATD. Arg this GATD!! It causes me more problems that it solves ;) Especially with no automatic deriving, it adds a lot of burden to my code.
data Obs a where ProposedBy :: Obs Int -- The player that proposed the tested rule Turn :: Obs Turn -- The current turn Official :: Obs Bool -- whereas the tested rule is official 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 :: a -> Obs a
instance Read a => Read (Obs a) where readPrec = (prec 10 $ do Ident "ProposedBy" <- lexP return (ProposedBy)) +++ (prec 10 $ do Ident "Official" <- lexP return (Official)) (etc...)
Observable.lhs:120:8: Couldn't match expected type `Int' against inferred type `Bool' Expected type: ReadPrec (Obs Int) Inferred type: ReadPrec (Obs Bool)
Indeed "ProposedBy" does not have the same type that "Official". Mmh how to make it all gently mix altogether?
Best, Corentin
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
corentin.dupont＠ext.mpsa.com -
Edward Kmett -
Stephen Tetley