我试图在
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时,抱怨函数依赖项在实例声明之间发生冲突,并引用了我的所有三个增量实例.这个错误对我来说没有多大意义,我没有看到单独的声明之间有任何冲突.更让我困惑的是,如果我将第一个实例更改为两个单独的实例
instance (Peano a) => Increment (Succ a) (Succ (Succ a)) instance Increment Zero (Succ Zero)
编译器完全停止抱怨.然而,定义Peano的规则告诉我这两件事情应该是一样的.
为什么在编写单行版本时会出现函数依赖冲突,但在编写双行版本时却没有?
这个答案是
this comment的扩展,这使我了解正在发生的事情
在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)