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的规则告诉我这两件事情应该是一样的.

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

在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)

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

（编辑：安卓应用网）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!