理解代数数据类型的困难答案

【问题标题】：Difficulties in understanding algebraic data type理解代数数据类型的困难
【发布时间】：2016-12-12 10:06:09
【问题描述】：

我不太确定这个 ZInt 实际描述的是什么。

data Nat = Zero | S Nat
data ZInt = Z Nat Nat deriving Show

addZ :: ZInt -> ZInt -> ZInt
addZ (Z a b) (Z c d) = Z (add a c) (add b d)

with
add ::  Nat -> Nat -> Nat
add a Zero  = a
add a (S b) = S (add a b)

mult :: Nat -> Nat -> Nat
mult _ Zero  = Zero
mult a (S b) = add a (mult a b)

乍一看，我认为这可能是复数的表示，添加虚部和实部（在函数 addZ 中）而不显示形式

a+b*i

但是在这个函数中发生了什么？

 subZ :: ZInt -> ZInt -> ZInt 
 subZ (Z a b) (Z c d) = Z (add a d) (add b c)

multZ :: ZInt -> ZInt -> ZInt
multZ (Z a b) (Z c d) = Z (add (mult a d) (mult c b)) (add (mult a c) (mult b d))

所以我确实理解数据 Nat = 零 | S Nat 以及 add 和 mult 函数，但不是 addZ、subZ 和 multZ。

【问题讨论】：

标签： haskell data-structures functional-programming algebraic-data-types

【解决方案1】：

这只是整数。 Nat 代表一个自然数。 ZInt 代表一个整数。在 Z a b 中，如果 a >= b 则整数是 a - b else -(b - a)。

例如：

ZInt representation | Traditional representation
Z Zero Zero         | 0
Z (S Zero) Zero     | 1
Z Zero (S Zero)     | -1
Z (S Zero) (S Zero) | 0
...

正如我们所见，将negate 转换为整数，您只需在其表示中交换Nat 值：

negate :: ZInt -> ZInt
negate (Z n m) = Z m n

我们可以这样定义subZ：

a `subZ` b = a `addZ` negate b

此表示不规范，Z (S Zero) (S Zero) 与Z Zero Zero 是相同的整数。所以，我们可以这样定义规范形式：

canonical :: ZInt -> ZInt
canonical (Z (S n) (S m)) = canonical (Z n m)
canonical x               = x

用这种方式定义整数的原因是什么？

首先，它在数学上很清楚。如果有人定义了名为N 的自然数集，我们可以轻松地将名为Z 的整数集定义为Z = N * N，其中(*) 是两个集合的乘积。

在 Haskell 中，我只能看到一个原因。通过这种方式，我们可以在类型级别定义整数。

【讨论】：

-(b-a) 与(a-b) 相同。
@bereal 否，因为a 和b 是自然数，如果a < b 则未定义a - b 的结果。
“一对坚果”。嗯，这是一种可能的解释。
@n.m. “一对坚果”是技术角度。逻辑上是整数（这个结论来源于函数定义）
canonical 可以通过首先列出两个非零的情况来简化。其他两种情况然后减少到canonical x = x。

【解决方案2】：

首先，ZInt 将每个整数表示为一对有序的自然数。 @freestyle 涵盖了这种表示如何运作良好；我将详细介绍算术运算符如何利用这种编码。

addZ、subZ 和 multZ 只是在操作代表每个整数的自然数对。

addZ (Z a b) (Z c d) = Z (add a c) (add b d)
(a - b) + (c - d) == a - b + c - d
                  == a + c - b - d
                  == (a + c) - (b + d)

subZ (Z a b) (Z c d) = Z (add a d) (add b c)
(a - b) - (c - d) == a - b - c + d
                  == a + d - b - c
                  == (a + d) - (b + c)

multZ (Z a b) (Z c d) = Z (add (mult a d) (mult c b)) (add (mult a c) (mult b d))
(a - b) * (c - d) == ac - ad - bc + bd
                  == ac + bd - ad - bc
                  == (ac + bd) - (ad + bc)

请注意，multZ 的给定定义可能会导致符号错误；应该是

multZ (Z a b) (Z c d) = Z (add (mult a c) (mult b d)) (add (mult a d) (mult b c))

（为了清楚起见，它还应该使用mult b c 而不是mult c b，即使自然数的乘法是可交换的。）

【讨论】：