为 Fix 编写 Eq 的实例 (Haskell)

Question

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

我的Fix：

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

我在Fix方面的List：

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

请注意，倒数第三行中的===绑定到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)

Answer 2

一种可能的方法是使用不可判定的实例来创建"递归实例"，可以这么说。

{-# LANGUAGE UndecidableInstances #-}
-- Fixed point of a Functor
newtype Fix f = In (f (Fix f))
instance Show (f (Fix f)) => Show (Fix f) where
showsPrec p (In x) = showParen (p > 10) $
("In " ++) . showsPrec 11 x
data ListF a r = NilF | ConsF a r 
deriving Show

上面，我们定义了showsPrec以便仅在需要时添加括号。幻数10对应于应用程序优先级级别，showParen有条件地添加括号。

请注意，必须使用deriving Show声明函子才能正常工作。

请注意此处棘手的约束解析。当检查Show ListF'时，GHC将其减少到Show (Fix ListF)，然后是Show (ListF (Fix ListF))，然后再次Show (Fix ListF)，但现在"喜结连理"并产生"递归实例"，而不是陷入无限循环。

---

或者，QuantifiedConstraints也可以工作，避免实例级递归。(不过，我们仍然需要不可判定的实例。

instance (forall a. Show a => Show (f a)) 
=> Show (Fix f) where
showsPrec p (In x) = showParen (p > 10) $
("In " ++) . showsPrec 11 x