Haskell GADT 'Show'
This code
{-# LANGUAGE GADTs #-}
data Expr a where
Val :: Num a => a -> Expr a
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
eval :: Expr a -> a
eval (Val x) = x
eval (Eq x y) = (eval x) == (eval y)
instance Show a => Show (Expr a) where
show (Val x) = "Val " ++ (show x)
show (Eq x y) = "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")"
fails to compile with the following error message:
Test.hs:13:32: error:
* Could not deduce (Show a1) arising from a use of `show'
from the context: Show a
bound by the instance declaration at test.hs:11:10-32
or from: (a ~ Bool, Eq a1)
bound by a pattern with constructor:
Eq :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
in an equation for `show'
at test.hs:13:11-16
Possible fix:
add (Show a1) to the context of the data constructor `Eq'
* In the first argument of `(++)', namely `(show y)'
In the second argument of `(++)', namely
`(show y) ++ ") (" ++ (show x) ++ ")"'
In the expression: "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")" Failed, modules loaded: none.
Commenting out the last line fixes the issue and inspecting the type of Expr in GHCi reveals, that, instead of inferring Eq to be of type Eq a => (Expr a) -> (Expr a) -> Expr Bool , GHC actually infers it to be Eq a1 => (Expr a1) -> (Expr a1) -> Expr Bool for data Expr a where ... . This explains the error message, since instance Show a => Show (Expr a) where ... won't enforce a1 to be an instance of Show .
However I do not understand, why GHC chooses to do so. If I had to make a guess, I'd say it has something to do with Eq returning a value, that doesn't depend on a at all and thus GHC "forgetting" about a , once Eq returns a Expr Bool . Is this - at least sort of - what is happening here?
Also, is there a clean solution to this? I tried several things, including trying to "force" the desired type via InstanceSigs and ScopedTypeVariables doing something like this:
instance Show a => Show (Expr a) where
show :: forall a. Eq a => Expr a -> String
show (Eq x y) = "Eq (" ++ (show (x :: Expr a)) ++ ") (" ++ (show (y :: Expr a)) ++ ")"
...
, but with no success. And since I'm still a Haskell novice, I'm not even sure, if this could somehow work anyways, due to my initial guess why GHC doesn't infer the "correct"/desired type in the first place.
EDIT:
Ok, so I decided to add a function
extract (Eq x _) = x
to the file (without a type signature), just to see, what return type it would have. GHC again refused to compile, but this time, the error message contained some information about skolem type variables. A quick search yielded this question, which (I think?) formalizes, what I believe the issue to be: Once Eq :: Expr a -> Expr a -> Expr Bool returns a Expr Bool , a goes "out of scope". Now we don't have any information left about a , so extract would have to have the signature exists a. Expr Bool -> a exists a. Expr Bool -> a , since forall a. Expr Bool -> a forall a. Expr Bool -> a won't be true for every a . But because GHC doesn't support exists , type-checking fails.
One option is not requiring a Show a superconstraint.
instance Show (Expr a) where
showsPrec p (Eq x y) = showParen (p>9)
$ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y
Of course this somewhat kicks the stone down the road, because now you can not write
showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x
anymore – now the leaf-value is not Show constrained. But here you can hack your way around this by making the Num constraint a bit stronger:
data Expr a where
Val :: RealFrac a => a -> Expr a
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
instance Show (Expr a) where
showsPrec p (Val x) = showParen (p>9) $ ("Val "++)
. showsPrec 10 (realToFrac x :: Double)
Well, that is a big hack, and at that point you might as well use simply
data Expr a where
Val :: Double -> Expr Double
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
(or whatever other single type best fits your number requirements). That's not a good solution.
To retain the ability to store numbers of any type in Expr leaves, yet be able to constrain them to Show if desired, you need to be polymorphic on the constraint.
{-# LANGUAGE ConstraintKinds, KindSignatures #-}
import GHC.Exts (Constraint)
data Expr (c :: * -> Constraint) a where
Val :: (Num a, c a) => a -> Expr a
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
Then you can do
instance Show (Expr Show a) where
showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x
showsPrec p (Eq x y) = showParen (p>9)
$ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y
I will only explain this point.
However I do not understand, why GHC chooses to do so.
The issue is, one can write a custom type with a Num and Eq instance, but no Show one.
newtype T = T Int deriving (Num, Eq) -- no Show, on purpose!
Then, this type checks:
e1 :: Expr T
e1 = Val (T 42)
as does this:
e2 :: Expr Bool
e2 = Eq e1 e1
However, it should be clear that e1 and e2 can not be show ed. To print these, we would need Show T , which is missing.
Further, the constraint
instance Show a => Show (Expr a) where
-- ^^^^^^
is useless here, since we do have Show Bool , but this is not enough to print e2 :: Expr Bool .
This is the problem of existential types: you get what you pay for. When we construct e2 = Eq e1 e2 we only have to "pay" the constraint Eq T . Hence, when we pattern match Eq ab we only get Eq t back (where t is a suitable type variable). We do not get to know whether Show t holds. Indeed, even if we did remember t ~ T , we would still lack the required Show T instance.
上一篇: 单次计算N次
下一篇: Haskell GADT'显示'