haskell - 为 Fix 编写一个 Eq 实例 (Haskell)

Question

我正在使用 Fix 为我正在处理的项目定义一些数据类型。我需要这些数据类型成为用于单元测试的相等类型类 Eq 的实例。我对如何为 Fix 或更具体的 List 编写 Eq 的实例感到困惑，该实例根据 Fix 定义>.

我的修复:

-- Fixed point of a Functor  
newtype Fix f = In (f (Fix f))                                                               
                                                                                             
out :: Fix f -> f (Fix f)                                                                    
out (In f) = f  

我的 List 在 Fix 方面:

data ListF a r = NilF | ConsF a r 

instance Functor (ListF a) where                                                          
       fmap _ NilF = NilF                                                                
       fmap f (ConsF a r) = ConsF a (f r)                                                
                                                                                            
type ListF' a = Fix (ListF a) 

Answer 1

@chi 的回答很好，但给你的是 Show 实例而不是 Eq 实例。

直接为 ListF' 编写一个 Eq 实例实际上非常简单。您可能只是想多了:

instance Eq a => Eq (ListF' a) where
  In (ConsF a as) == In (ConsF b bs) | a == b, as == bs      = True
  In NilF         == In NilF                                 = True
  In _            == In _                                    = False

你可以到此为止，但如果你排除了新类型的展开:

instance Eq a => Eq (ListF' a) where
  In f == In g = eqListF f g
    where eqListF (ConsF a as) (ConsF b bs) | a == b, as == bs      = True
          eqListF NilF         NilF                                 = True
          eqListF _            _                                    = False

并将eqListF变成一个实例:

instance Eq a => Eq (ListF' a) where
  In f == In g = f == g

instance (Eq a, Eq r) => Eq (ListF a r) where
  ConsF a as == ConsF b bs | a == b, as == bs      = True
  NilF       == NilF                               = True
  _          == _                                  = False

开始变得更清楚如何获得“通用”解决方案(对于 Fix f)，尽管除非您已经看到 Eq1，否则很难弄清楚这一点> 某个地方。

class Eq1 f where
  liftEq :: (a -> a -> Bool) -> (f a -> f a -> Bool)
instance Eq1 f => Eq (Fix f) where
  In f == In g = liftEq (==) f g

instance (Eq a) => Eq1 (ListF a) where
  liftEq (===) (ConsF a as) (ConsF b bs) | a == b, as === bs   = True
  liftEq _     NilF         NilF                               = True
  liftEq _     _            _                                  = False

请注意，倒数第三行中的 === 绑定(bind)到 liftEq 提升的 ==。

根据@chi 的回答，实际上可以通过利用相对较新的 QuantifiedConstraints 扩展来避免使用笨拙的 Eq1 实例。重写后的实例看起来像这样，ListF 的 Eq 实例比上面的 Eq1 实例自然得多:

instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) where
  In f == In g = f == g

instance (Eq a, Eq l) => Eq (ListF a l) where
  ConsF a as == ConsF b bs | a == b, as == bs   = True
  NilF       == NilF                            = True
  _          == _                               = False

更新并且，根据@DanielWagner 的评论，编译器可以为您完成所有这些工作。如果您以通常的方式为 ListF 派生 Eq 实例:

data ListF a r = NilF | ConsF a r deriving (Eq)

然后使用StandaloneDeriving，编译器将直接为ListF'a派生Eq实例:

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Eq a => Eq (ListF' a)

而且，更值得注意的是，它将推导出一般情况:

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
deriving instance (Eq (f (Fix f))) => Eq (Fix f)

不需要任何额外的实例。

这是完全手动版本的完整代码，首先使用传统的 Eq1 方法(并从 Data.Functor.Classes 中获取 class Eq1 >).

{-# LANGUAGE FlexibleInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r
type ListF' a = Fix (ListF a)

instance Eq1 f => Eq (Fix f) where
  In f == In g = liftEq (==) f g

instance (Eq a) => Eq1 (ListF a) where
  liftEq (===) (ConsF a as) (ConsF b bs) | a == b, as === bs    = True
  liftEq _     NilF         NilF                               = True
  liftEq _     _            _                                  = False

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)

然后使用 QuantifiedConstraints 版本:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r
type ListF' a = Fix (ListF a)

instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) where
  In f == In g = f == g

instance (Eq a, Eq l) => Eq (ListF a l) where
  ConsF a as == ConsF b bs | a == b, as == bs   = True
  NilF       == NilF                            = True
  _          == _                               = False

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)

最后是编译器衍生版本。

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r deriving (Eq)
type ListF' a = Fix (ListF a)

deriving instance (Eq (f (Fix f))) => Eq (Fix f)

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)