哈斯克尔GADT“Show'-实例类型变量扣除

Question

此代码

{-# 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类型，GHC实际上推断为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类型变量的信息。快速搜索产生了this question，这（我认为？）正式化，我认为这个问题是：一旦Eq :: Expr a -> Expr a -> Expr Bool返回Expr Bool,a“超出范围”。现在我们还没有任何有关a的信息，因此extract必须有签名exists a. Expr Bool -> a，因为forall a. Expr Bool -> a对于每个a都不是真的。但是由于GHC不支持exists，类型检查失败。

Answer 1

一个选项是而不是需要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 

Answer 2

我，只说明了这一点。

但是我不明白，为什么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 a b我们只得到Eq t背面（其中t是一个适当类型的变量）。我们不知道Show t是否成立。事实上，即使我们确实记得t ~ T，我们仍然会缺少所需的Show T实例。