haskell - "Contraint is no smaller than the instance head"是什么意思以及如何解决

Question

我想写一些类似的东西:

{-# LANGUAGE FlexibleContexts,FlexibleInstances #-}

import Data.ByteString.Char8 (ByteString,pack)
import Data.Foldable (Foldable)

class (Show a) => Rows a where
    rRepr :: a -> [ByteString]
    rRepr = (:[]) . pack . show

instance (Foldable f,Show (f a)) => Rows (f a) where
    rRepr = const []

意思是 f a实例化 Rows如果 f实例化 Foldable和 f a实例化 Show .当我运行 ghc 我得到:

Constraint is no smaller than the instance head
  in the constraint: Show (f a)
(Use -XUndecidableInstances to permit this)
In the instance declaration for `Rows (f a)'

我有两个问题:

错误中的“较小”是什么意思，问题是什么？

在不使用 UndecidableInstances 的情况下定义我想要的东西的正确方法是什么？ ?

Answer 1

让我们玩一下编译器:我们有一个类型 (f a)我们想看看它是否是 Rows 的有效满足符约束。为此，我们需要发送一个证明 (f a)满足 Show (f a)也是。这不是问题，除非有人写

 instance Rows (f a) => Show (f a) where ...

在这种情况下，我又回到了我开始的地方。像这样编码无限循环有点愚蠢，但 Haskell 静态地确保它实际上是不可能的，除非你要求 UndecidableInstances .

通常，Haskell 确保“解析追逐”的每一步都会将类型的大小减少至少 1 个构造函数。这通过结构归纳得出了一个非常简单的证明，即我们最终会得到一个具有有限数量分辨率的裸类型。

这是过于严格的，显然一些实例解析步骤是有意义的、有用的和完整的，即使它们不会立即减少构造函数树。这种整体性限制适用于像 Agda 和 Coq 这样的语言，并且通常将您的算法操纵成一个通过结构归纳进行的算法是一个说明性的挑战。

那么我们该如何解决呢？一种方法是丢失 Show对 class 的约束定义使用像 Show1 这样的实例来自 prelude-extras .

class Show1 f where ...
show1 :: (Show1 f, Show a) => f a -> String  -- not an instance definition!

然后有 instance (Foldable f, Show1 f, Show a) => Rows (f a) where ...这在我的测试中有效。然后，您可以将默认实例编写为独立函数。

defRRepr :: Show a => a -> [ByteString]
defRRepr = (:[]) . pack . show

并在为 Show 编写实例定义时使用它能干的事。

另一种解决方案是使用 newtype包装器允许 Haskell 看到分辨率的“层”已被删除。

instance (Foldable f, Show (f a)) => Rows (FoldableRow f a) where
    rRepr = const [] . unFR

newtype FoldableRow f a = FR { unFR :: f a } deriving (Show)