haskell – 当我扩展定义时,为什么我的功能依赖冲突会消失?

我试图在 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)

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

相关文章

适配器模式将一个类的接口转换成客户期望的另一个接口,使得原本接口不兼容的类可以相互合作。
策略模式定义了一系列算法族,并封装在类中,它们之间可以互相替换,此模式让算法的变化独立于使用算法...
设计模式讲的是如何编写可扩展、可维护、可读的高质量代码,它是针对软件开发中经常遇到的一些设计问题...
模板方法模式在一个方法中定义一个算法的骨架,而将一些步骤延迟到子类中,使得子类可以在不改变算法结...
迭代器模式提供了一种方法,用于遍历集合对象中的元素,而又不暴露其内部的细节。
外观模式又叫门面模式,它提供了一个统一的(高层)接口,用来访问子系统中的一群接口,使得子系统更容...