量化约束与(封闭)类型族

Question

我正在尝试使用这篇博文的方法来处理更高级的数据，而不会为三元情况悬空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)

？

Answer 1

tl;博士，要点：https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

样板约束

首先，如果问题是关于避免重复代码，这主要由泛型单独解决，没有QuantifiedConstraints。约束(Show (HKD f Int), Show (HKD f Bool))可以从泛型表示Rep (Result f)计算。通用数据包(免责声明：我写的)实现了这一点：

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

或带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"。一般规则是不允许在任何实例的头中使用类型族("实例头"=以下instance ... => HEAD where中的HEAD)。因此，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

现在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 Int)实例化的Show (HKD f x)。那么为什么被拒绝呢？约束求解器倒推：首先使用show需要一个约束Show (HKD f Int)，但求解器立即卡住。它在上下文中看到forall x. ShowHKD f x，但求解器不知道它应该实例化x以Int。您应该想象，此时约束求解器不知道Show和ShowHKD之间的任何关系。它只需要一个Show约束，上下文中没有约束。

我们可以像下面这样帮助约束求解器，通过使用所需的ShowHKD f x实例化来注释函数的主体，这里ShowHKD f Int：

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

这个注解提供了主体show的约束ShowHKD f Int，这反过来又使超类可用Show (HKD f Int)以便show可以立即得到满足。另一方面，注释需要约束ShowHKD f Int其上下文，这提供了forall x. ShowHKD f x。这些约束匹配，这会导致约束求解器适当地实例化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：

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

Answer 2

我不认为你可以做这样的事情，但我肯定是错的。在您的示例中，您缺少一个额外的约束Show (f a)以使其完整：

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

但这意味着Showf a的实例不能依赖于a，这对于特定f可能是正确的，但不是一般的。

编辑

但与此同时，可以在没有TypeFamilies的情况下写出这样的东西：

data Bar f = MkBar (f Int)
deriving instance (forall a . Show a => Show (f a)) => Show (Bar f)

所以，我不确定为什么GHC无法弄清楚。

编辑 2

这是一个有趣的观察结果，它编译：

type family HKD f a where
-- HKD Identity a = a
HKD f Int = Int
HKD f a = f a
data Result f = MkResult
{ foo :: HKD f Int
, bar :: HKD f Bool
}
deriving instance (forall a. Show a => Show (f a)) => Show (Result f)

并按预期工作：

λ> show $ MkResult 5 (Just True)
"MkResult {foo = 5, bar = Just True}"

因此，看起来匹配f以某种方式弄乱了类型检查器。

值得注意的是，即使对于简化的示例，限制为Show (HDK f a)也会给出与问题中相同的编译时错误：

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