量化约束与（封闭）类型族

我正在尝试使用这篇博文的方法是在不悬而未决的情况下获取更高级的数据Identity简单情况的函子与量化约束推导一起：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
module HKD2 where

import Control.Monad.Identity

type family HKD f a where
    HKD Identity a = a
    HKD f        a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)

这会导致令人恼火的自相矛盾的错误消息：

无法推断Show (HKD f a)从上下文来看：forall a. Show a => Show (HKD f a)

有没有一种方法可以做到这一点而不需要冗长地做

deriving instance (Show (HKD f Int), Show (HKD f Bool)) => Show (Result f)

?

长话短说，博士，要点：https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

样板约束

首先，如果问题是关于避免重复的代码，那么这主要是仅通过泛型来解决，而不需要QuantifiedConstraints。约束条件(Show (HKD f Int), Show (HKD f Bool))可以从通用表示计算Rep (Result f)。 generic-data 包（免责声明：我写的）实现了这一点：

data Result f = MkResult (HKD f Int) (HKD f Bool)
  deriving Generic

-- GShow0 and gshowsPrec from Generic.Data
instance GShow0 (Rep (Result f)) => Show (Result f) where
  showsPrec = gshowsPrec

or with DerivingVia:

-- Generically and GShow0 from Generic.Data
deriving via Generically (Result f) instance GShow0 (Rep (Result f)) => Show (Result f)

类型族的量化约束

尽管如此，约束(Show (HKD f Int), Show (HKD f Bool))可能由于各种原因不太理想。这QuantifiedConstraints扩展似乎提供了更自然的约束forall x. Show (HKD f x):

• 这将需要元组(Show (HKD f Int), Show (HKD f Bool));

• 与该元组相反，当记录变大时，它的大小不会膨胀，并且不会泄漏Result因为它们可能会发生变化。

不幸的是，这个约束实际上并不完善。以下 GHC 问题详细讨论了该问题：https://gitlab.haskell.org/ghc/ghc/issues/14840我还不明白所有的原因，但简而言之：

• 由于理论和实践的原因，在可预见的未来，量化约束不会直接适用于类型族；

• 但对于大多数用例都有一个解决方法。

量化约束应被视为一种“局部约束”instance”。一般规则是类型族不允许出现在任何实例的头部（“实例头部”=HEAD在下面的instance ... => HEAD where). So forall a. Show (HKD f a)（被视为“本地”instance Show (HKD f a)）是非法的。

量化约束走私者

以下解决方案归功于Icelandjack（来源：此评论来自之前链接的票证;也感谢 Ryan Scott 的转发。）

我们可以定义另一个类，它相当于Show (HKD f a):

class    Show (HKD f a) => ShowHKD f a
instance Show (HKD f a) => ShowHKD f a

Now forall x. ShowHKD f x是一种法律约束，在道德上表达了预期的forall x. Show (HKD f x)。但如何使用它并不明显。例如，以下代码片段无法进行类型检查（注意：我们可以轻松忽略歧义问题）：

showHKD :: forall f. (forall x. ShowHKD f x) => HKD f Int -> String
showHKD = show

-- Error:
-- Could not deduce (Show (HKD f Int)) from the context (forall x. ShowHKD f x)

这是违反直觉的，因为ShowHKD f x相当于Show (HKD f x)当然可以实例化为Show (HKD f Int)。那么为什么会被拒绝呢？约束求解器向后推理：使用show首先需要一个约束Show (HKD f Int)，但求解器立即卡住了。它看到forall x. ShowHKD f x在上下文中，但求解器没有任何线索知道它应该实例化x to Int。您应该想象，此时约束求解器不知道之间的任何关系Show and ShowHKD。它只是想要一个Show约束，并且上下文中没有约束。

我们可以通过如下方式帮助约束求解器，通过使用所需的实例化来注释函数体ShowHKD f x, here ShowHKD f Int:

showHKD :: forall f. (forall x. ShowHKD f x) => HKD f Int -> String
showHKD = show :: ShowHKD f Int => HKD f Int -> String

这个注释provides约束条件ShowHKD f Int对身体show，这反过来又使超类可用Show (HKD f Int) so show可以立刻得到满足。另一边是注释requires约束条件ShowHKD f Int从它的上下文来看，它提供了forall x. ShowHKD f x。那些限制match，这导致约束求解器实例化x适当地。

具有量化约束的导出显示

有了这个，我们就可以实现Show具有量化约束，使用泛型填充正文，并使用一些注释来实例化量化约束，(ShowHKD f Int, ShowHKD f Bool):

instance (forall a. Show a => ShowHKD f a) => Show (Result f) where
  showsPrec = gshowsPrec :: (ShowHKD f Int, ShowHKD f Bool) => Int -> Result f -> ShowS

和以前一样，这些约束可以使用泛型自动化，因此在此实现中从一种类型到另一种类型的唯一变化是名称Result:

instance (forall a. Show a => ShowHKD f a) => Show (Result f) where
  showsPrec = gshowsPrec :: ShowHKDFields f (Rep (Result HKDTag)) => Int -> Result f -> ShowS

-- New definitions: ShowHKDFields and HKDTag; see gist at the end.

只要多一点努力，我们就可以拥有DerivingVia too:

deriving via GenericallyHKD Result f instance (forall a. Show a => ShowHKD f a) => Show (Result f)

-- New definition: GenericallyHKD; see gist.

完整要点：https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439