Haskell 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 的类型显示，GHC 不是将 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，一次@987654335 @ 返回 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 不能是showed。要打印这些，我们需要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 实例。