什么"Contraint不小于实例头"意味着如何解决它

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实例化Rowsif finstanti Foldable和f ainstantiate 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从序幕,演员.

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)