"Contraint is no smaller than the instance head"意味着什么以及如何解决它



我想写这样的东西:

{-# 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实例化Foldablef 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的情况下定义我想要的东西的正确方法是什么?

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

 instance Rows (f a) => Show (f a) where ...
在这种情况下,我

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


通常,Haskell确保"分辨率追逐"的每一步都会将类型的大小至少减少1个构造函数。这导致了一个非常简单的结构归纳证明,我们最终将得到有限数量的分辨率的裸类型。

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


那么我们如何解决它呢?一种方法是失去对class定义的Show约束,使用类似 prelude-extras 的 Show1 实例。

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)

最新更新