量化约束与(封闭)类型族 [英] Quantified constraints vs. (closed) type families

问题描述

我正在尝试使用此博客文章的方法来处理种类繁多的数据，而又不会晃动 Identity一般情况下的函子和量化约束推导:

I am trying to use this blogpost's approach to higher-kinded data without dangling Identity functors for the trival case together with quantified-constraint deriving:

{-# 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)

这会导致令人反感的错误消息:

This results in the infuriatingly self-contradicting error message:

无法推断 Show(HKD f a)从上下文中: forall显示一个=>显示(港元f a)

有没有办法做到这一点而又不费吹灰之力

Is there a way to do this without being long-winded about it and doing

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

?

推荐答案

tl; dr，要点: https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

tl;dr, gist: https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

首先，如果问题是避免重复代码，则大多数情况下仅使用泛型即可解决，而无需 QuantifiedConstraints .约束(Show(HKD f Int)，Show(HKD f Bool))可以从通用表示形式 Rep(Result f)中计算出来.通用数据包(免责声明:我写的)实现了这一点:

First, if the question is about avoiding repetitive code, this is mostly addressed by generics alone, without QuantifiedConstraints. The constraint (Show (HKD f Int), Show (HKD f Bool)) can be computed from the generic representation Rep (Result f). The generic-data package (disclaimer: that I wrote) implements this:

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 扩展名似乎为所有x提供了更自然的约束.显示(HKD f x):

Quantified constraints with type families

Nevertheless, the constraint (Show (HKD f Int), Show (HKD f Bool)) may be less than ideal for various reasons. The QuantifiedConstraints extension may seem to provide a more natural constraint forall x. Show (HKD f x):

• 将需要元组(显示(HKD f Int)，显示(HKD f Bool));

与该元组相反，当记录变大时，它的大小不会爆炸，也不会泄漏 Result 的字段类型，因为它们可能会发生变化.

contrary to that tuple, it does not blow up in size when the record gets big, and does not leak the field types of Result as they may be subject to change.

不幸的是，该约束实际上不是格式正确的.以下GHC问题详细讨论了该问题: https://gitlab.haskell.org/ghc/ghc/issues/14840 我还不了解所有原因，但总之:

Unfortunately, that constraint is actually not well-formed. The following GHC issue discusses the problem in detail: https://gitlab.haskell.org/ghc/ghc/issues/14840 I don't understand all of the reasons yet, but in brief:

• 在可预见的将来，由于理论和实践上的原因，量化约束将无法直接与类型族配合使用；

• Quantified constraints won't work directly with type families for the foreseeable future, for reasons both theoretical and practical;

但是对于大多数用例来说，都有一种解决方法.

But there is a workaround for most use cases.

量化约束应视为一种本地 instance ".然后，一般规则是，在任何实例的头部都不允许使用类型族("instance head" =以下 instance ... => HEAD where 中的 HEAD >).所以 forall a.表演(HKD f a)(被视为本地"实例(HKD f a))是非法的.

A quantified constraint should be viewed as a sort of "local instance". The general rule then is that type families are not allowed in the head of any instance ("instance head" = the HEAD in the following instance ... => HEAD where). So forall a. Show (HKD f a) (viewed as a "local" instance Show (HKD f a)) is illegal.

以下解决方案归功于Icelandjack(来源:来自票证的此评论链接较早；也感谢Ryan Scott进行了中继.)

The following solution is credited to Icelandjack (Source: this comment from the ticket linked earlier; thanks also to Ryan Scott for relaying it.)

我们可以定义另一个与 Show(HKD f a)相同的类:

We can define another class that's equivalent to 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.显示(HKD f x).但是如何使用它一点也不明显.例如，以下代码片段无法进行类型检查(注意:我们可以轻松地忽略歧义问题):

Now forall x. ShowHKD f x is a legal constraint that morally expresses the intended forall x. Show (HKD f x). But it's not at all obvious how to use it. For example, the following snippet fails to type check (note: we can easily ignore the ambiguity issues):

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 fx 等同于 Show(HKD fx)，当然可以用 Show(HKD f Int)实例化.那为什么拒绝呢?约束求解器的原因倒退:使用 show 首先需要约束 Show(HKD f Int)，但是求解器会立即卡住.它看到 forall x.在上下文中使用ShowHKD f x ，但是求解器不知道应该将 x 实例化为 Int .您应该想象一下，此时约束求解器不知道 Show 和 ShowHKD 之间的任何关系.它只想要一个 Show 约束，并且上下文中没有约束.

This is counterintuitive, because ShowHKD f x is equivalent to Show (HKD f x) which can of course be instantiated with Show (HKD f Int). So why is that rejected? The constraint solver reasons backwards: the use of show first requires a constraint Show (HKD f Int), but the solver is immediately stuck. It sees forall x. ShowHKD f x in the context, but there is no clue for the solver to know that it should instantiate x to Int. You should imagine that at this point, the constraint solver has no idea of any relationship between Show and ShowHKD. It just wants a Show constraint, and there is none in the context.

我们可以通过使用 ShowHKD fx (此处为 ShowHKD f Int )的所需实例化对函数主体进行注释来帮助约束求解器，如下所示:/p>

We can help the constraint solver as follows, by annotating the body of the function with the needed instantiation(s) of 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

此注释为主体 show 提供约束 ShowHKD f Int ，从而使超类可用 Show(HKDf Int)，因此可以立即满足 show 的要求.另一方面，注释需要从其上下文中获取约束 ShowHKD f Int ，该约束提供了 forall x.ShowHKD f x .这些约束 match ，并导致约束求解器适当地实例化 x .

This annotation provides the constraint ShowHKD f Int to the body show, which in turn makes the superclass available Show (HKD f Int) so show can be immediately satisfied. On the other side, the annotation requires the constraint ShowHKD f Int from its context, which provides forall x. ShowHKD f x. Those constraints match, and that leads the constraint solver to instantiate x appropriately.

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

With this, we can implement Show with a quantified constraint, using generics to fill out the body, and with some annotations to instantiate the quantified constraint, (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 :

As before, those constraints can be automated with generics, so the only thing that changes in this implementation from one type to another is the name 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 :

And with a bit more effort, we can have 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

这篇关于量化约束与(封闭)类型族的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！