9

我正在尝试使用这篇博文的方法来处理更高种类的数据，而不会将普通情况下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)

?

4

2 回答 2

7

tl；博士，要点：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

或与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）。所以forall a. Show (HKD f a)（被视为“本地” instance Show (HKD f a)）是非法的。

量化约束走私者

以下解决方案归功于Icelandjack（来源：之前链接的票中的此评论；也感谢瑞恩斯科特转发它。）

我们可以定义另一个等价于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 x)which 当然可以用Show (HKD f Int). 那为什么会被拒绝呢？约束求解器向后推理：使用showfirst 需要一个约束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

该注释为body提供了约束，这反过来又使超类可用，因此可以立即得到满足。另一方面，注释需要来自其上下文的约束，它提供. 这些约束匹配，这导致约束求解器适当地实例化。ShowHKD f IntshowShow (HKD f Int)showShowHKD f Intforall x. ShowHKD f xx

使用量化约束导出 Show

有了这个，我们可以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

于 2020-06-05T21:33:29.230 回答
5

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

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

但这意味着Show实例 forf a不能依赖于a，这对于 specific 可能是正确的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)
于 2019-06-06T03:53:35.763 回答