Haskell GADT'显示'
这个代码
{-# 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) ++ ")"
无法编译时出现以下错误消息：
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.
GHCi发现，最后一行修正了问题并检查了Expr类型，结果发现，与其推断Eq类型为Eq a => (Expr a) -> (Expr a) -> Expr Bool ，实际上推断它是Eq a1 => (Expr a1) -> (Expr a1) -> Expr Bool用于data Expr a where ... 这解释了错误消息，因为instance Show a => Show (Expr a) where ...不会强制a1作为Show的实例。
但我不明白，为什么GHC选择这样做。 如果我不得不猜测，我会说这与Eq返回一个值有关，它不依赖于a ，因此GHC会“忘记” a ，一旦Eq返回Expr Bool 。 这是 - 至少有点 - 这里发生了什么？
另外，有没有一个干净的解决方案呢？ 我尝试了几件事，包括试图通过InstanceSigs和ScopedTypeVariables “强制”所需的类型，如下所示：
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)) ++ ")"
...
，但没有成功。 而且由于我仍然是一名Haskell新手，我甚至不确定，如果这可以以某种方式工作，由于我初步猜测为什么GHC不首先推断“正确”/所需类型。
编辑：
好的，所以我决定添加一个函数
extract (Eq x _) = x
到文件（没有类型签名），只是看看，它会有什么样的返回类型。 GHC再次拒绝编译，但是这一次，错误消息包含了一些关于skolem类型变量的信息。 快速搜索产生了这个问题，我认为这个问题正式化了，我认为这个问题是：一旦Eq :: Expr a -> Expr a -> Expr Bool返回一个Expr Bool ， a就会“超出范围”。 现在我们还没有关于a任何信息，因此extract将不得不使签名exists a. Expr Bool -> a exists a. Expr Bool -> a ，因为所有forall a. Expr Bool -> a forall a. Expr Bool -> a对于每a都不是真的。 但是由于GHC不支持exists ，类型检查失败。
一个选项不需要Show a超级约束。
instance Show (Expr a) where
showsPrec p (Eq x y) = showParen (p>9)
$ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y
当然这有点踢石头的路，因为现在你不能写
showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x
现在叶值不Show约束。 但是在这里你可以通过使Num约束更强大来解决这个问题：
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)
那么，这是一个很大的破解，在这一点上，你可能会很简单地使用它
data Expr a where
Val :: Double -> Expr Double
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
（或任何其他单一类型最适合您的号码要求）。 这不是一个好的解决方案。
为了保留在Expr叶片中存储任何类型的数字的能力，但是能够将它们限制为Show如果需要的话，您需要在约束上是多态的。
{-# 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
那你可以做
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
我只会解释这一点。
但我不明白，为什么GHC选择这样做。
问题是，可以使用Num和Eq实例编写自定义类型，但不能Show 。
newtype T = T Int deriving (Num, Eq) -- no Show, on purpose!
然后，这种类型检查：
e1 :: Expr T
e1 = Val (T 42)
如下所示：
e2 :: Expr Bool
e2 = Eq e1 e1
但是，应该清楚的是， e1和e2不能show 。 要打印这些，我们需要Show T ，这是缺少的。
此外，约束
instance Show a => Show (Expr a) where
-- ^^^^^^
在这里没用，因为我们有Show Bool ，但这不足以打印e2 :: Expr Bool 。
这是存在型问题：你得到你所支付的。 当我们构造e2 = Eq e1 e2我们只需要“支付”约束Eq T 因此，当我们匹配Eq ab我们只得到Eq t back（其中t是一个合适的类型变量）。 我们不知道Show t是否成立。 事实上，即使我们记得t ~ T ，我们仍然缺乏所需的Show T实例。
上一篇: Haskell GADT 'Show'
下一篇: Seemingly correct type signature refused in where block