如何为带双射函数依赖的Add1类定义多个实例？

问题背景 #

我定义了一个带双射函数依赖的Add1类，用来表示类型间的+1/-1映射：

class Add1 a b | a -> b , b -> a where
    add1 :: a -> b
    sub1 :: b -> a

同时定义了表示非负、非正的类型类，以及用来封装后继/前驱的类型：

class NonNegative a
class NonPositive a

data Succ a = Succ a
data Prev a = Prev a

当尝试定义以下两个实例时，编译器报函数依赖冲突错误：

instance NonNegative a => Add1 a (Succ a)
instance NonPositive a => Add1 (Prev a) a

错误信息如下：

Functional dependencies conflict between instance declarations:
  instance NonNegative a => Add1 a (Succ a)
    -- Defined at BijectiveFD.hs:13:10
  instance NonPositive a => Add1 (Prev a) a
    -- Defined at BijectiveFD.hs:14:10

单独定义任意一个实例都能正常工作，想知道如何同时定义这两个实例。

完整代码：

{-# LANGUAGE FunctionalDependencies #-}

class NonNegative a 
class NonPositive a

class Add1 a b | a -> b , b -> a where 
    add1 :: a -> b 
    add1 = u
    sub1 :: b -> a
    sub1 = u 
u = undefined

instance NonNegative a => Add1 a (Succ a) 
instance NonPositive a => Add1 (Prev a) a 

data Zero = Zero 

instance NonNegative Zero
instance NonPositive Zero

data Succ a = Succ a
data Prev a = Prev a

instance (NonNegative a) => NonNegative (Succ a)
instance (NonPositive a) => NonPositive (Prev a)

问题原因 #

Haskell的实例匹配逻辑是先匹配实例头部，再检查约束条件。对于Add1的双射函数依赖a -> b和b -> a，要求每个a只能对应唯一的b，每个b也只能对应唯一的a。

编译器会认为这两个实例存在冲突的可能性：假设存在某个类型x，既满足NonNegative x，又存在y使得Prev y = x且NonPositive y，那么Add1 x (Succ x)和Add1 x y会导致同一个a对应两个不同的b，违反函数依赖约束。即使实际代码中不存在这样的类型，编译器也会基于实例头部的模式匹配关系抛出错误。

解决方案 #

方案1：改用关联类型族（推荐） #

用类型族替代函数依赖，能更精确地表达类型间的映射关系，同时结合约束限制实例的适用范围：

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-}

class NonNegative a
class NonPositive a

class Add1 a where
    -- 关联类型：a对应的后继类型
    type SuccTy a
    add1 :: a -> SuccTy a
    sub1 :: SuccTy a -> a

data Zero = Zero
data Succ a = Succ a
data Prev a = Prev a

-- 非负类型的Add1实例：映射到Succ a
instance NonNegative a => Add1 a where
    type SuccTy a = Succ a
    add1 = Succ
    sub1 (Succ x) = x

-- 前驱类型的Add1实例：映射到原始类型a
instance NonPositive a => Add1 (Prev a) where
    type SuccTy (Prev a) = a
    add1 (Prev x) = x
    sub1 = Prev

类型族SuccTy直接绑定了每个a对应的目标类型，约束条件确保实例只会在符合条件的类型上生效，不会产生冲突。

方案2：使用重叠实例 #

开启重叠实例扩展，通过标注实例优先级来解决冲突，确保编译器能选择正确的实例：

{-# LANGUAGE FunctionalDependencies, FlexibleInstances, OverlappingInstances #-}

class NonNegative a
class NonPositive a

class Add1 a b | a -> b, b -> a where
    add1 :: a -> b
    sub1 :: b -> a

data Zero = Zero
data Succ a = Succ a
data Prev a = Prev a

-- 通用实例：非负类型映射到Succ a
instance {-# OVERLAPPABLE #-} NonNegative a => Add1 a (Succ a) where
    add1 = Succ
    sub1 (Succ x) = x

-- 更具体的实例：Prev a类型映射到a
instance {-# OVERLAPPING #-} NonPositive a => Add1 (Prev a) a where
    add1 (Prev x) = x
    sub1 = Prev

OVERLAPPING标注的实例优先级更高，当类型匹配Prev a时会优先选择该实例，其他非负类型则匹配通用实例，避免了函数依赖的冲突。

内容的提问来源于stack exchange，提问作者Ashok Kimmel