为什么扩展定义时我的功能依赖冲突会消失？

Question

我试图在Haskell中的类型级别实现Integers.首先,我实现了自然数

data Zero
data Succ a

然后我将其扩展为整数

data NegSucc a

我决定然后创建一个Increment增加整数的类.我是这样做的:

{-# Language FunctionalDependencies #-}
{-# Language UndecidableInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}

import Prelude ()

-- Peano Naturals --

data Zero
data Succ a

class Peano a
instance Peano Zero
instance (Peano a) => Peano (Succ a)

-- Integers --

data NegSucc a -- `NegSucc a` is -(a+1) so that 0 can only be expressed one way

class Integer a
instance (Peano a) => Integer a
instance (Peano a) => Integer (NegSucc a)

-- Arithmetic Operations --

class Increment a b | a -> b
instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero
instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

但是当我运行这个GHC抱怨时Functional dependencies conflict between instance declarations,并引用了我的所有三个增量实例.这个错误对我没有多大意义,我没有看到单独的声明之间有任何冲突.令我更加困惑的是,如果我将第一个实例更改为两个单独的实例

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

编译器完全停止抱怨.但是,定义的规则Peano a告诉我这两件事情应该是一样的.

为什么在编写单行版本时会出现函数依赖冲突,但在编写双行版本时却没有？

Answer 1

这个答案是对此评论的扩展,这使我了解正在发生的事情

在Haskell类型中,类是一个开放类,这意味着可以在声明之后创建类的新实例.

这意味着我们无法推断出它NegSucc a不是其成员Peano,因为它总是可以在以后声明它.

instance Peano (NegSucc a)

因此,当编译器看到

instance (Peano a) => Increment a (Succ a)
instance Increment (NegSucc Zero) Zero

它不可能知道NegSucc Zero不会是一个实例Peano.如果NegSucc Zero是的实例,Peano这将增加双方Zero和Succ (NegSucc Zero),这是一个函数依赖冲突.所以我们必须抛出错误.这同样适用于

instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a)

这里(NegSucc (Succ a))也可以是一个实例Peano.

它看起来好像没有冲突的原因是我们隐含地假设没有其他实例而Peano不是我们所知道的实例.当我将单个实例转换为两个新的意义时,我做出了正式的假设.

在新的代码中

instance (Peano a) => Increment (Succ a) (Succ (Succ a))
instance Increment Zero (Succ Zero)

无法向预先存在的类型类添加任何内容以使类型与多个冲突的实例匹配.