[Haskell-cafe] A Finally Tagless Pi Calculus
Dupont Corentin
corentin.dupont at gmail.com
Wed Jun 9 14:32:29 EDT 2010
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.
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)'
Cheers,
Corentin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100609/cee5888b/attachment.html
More information about the Haskell-Cafe
mailing list