haskell - `Eq` 的类型系列等效项？

Question

Type Families with Class显示:

据我不完全理解，这张幻灯片展示了实现 Eq 的 2 种方法:通过类型类或类型族。

我熟悉类型类，因此实现了 MyEq:

class MyEq a where 
    eq :: a -> a -> Bool

但是，当我尝试定义类型族版本时，它无法编译:

data Defined = Yes | No

type family IsEq (a :: *) :: Defined    

由于:

TypeEq.hs:30:30: error:
    • Type constructor ‘Defined’ cannot be used here
        (Perhaps you intended to use DataKinds)
    • In the kind ‘Defined’

请解释如何实现 Eq 类型类的 type family 版本。另外，请展示此类类型系列实例的实现(如果这个词正确的话)会很有帮助。

Answer 1

这有点简洁，很高兴偶然发现了这一点。有兴趣的，here是幻灯片和 here是纸。这是需要一些语言扩展的常见情况。

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, ConstraintKinds #-}

data Defined = Yes | No

type family IsEq (a :: *) :: Defined

type Eq a = IsEq a ~ Yes

然后，它的“实​​现”是这样的实例

type instance IsEq () = Yes      -- '()' is an instance of 'Eq'
type instance IsEq Int = Yes     -- 'Int' is an instance of 'Eq'
type instance IsEq [a] = IsEq a  -- '[a]' is an instance of 'Eq' is 'a' is

您可以在 GHCi 上“尝试”它们:

ghci> :kind! IsEq [Int]
IsEq [Int] :: Defined
= Yes

但是纸张和幻灯片实际上并不太担心实际提供相等函数。 (它提到将其存储在 Yes 字段中)。那么，如果它甚至没有准备好提供类方法，为什么这很有趣呢？因为

• 它提供了比重叠类更好的机制
• 回溯搜索比类型类更容易
• 它使得提前失败成为可能，并显示漂亮的错误消息(编码为 No 构造函数中的字段)