理解代数数据类型的困难

Question

我不太确定这个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 = Zero | S nat以及add和mult函数,但不是addZ,subZ和multZ.

Answer 1

它只是整数.Nat代表一个自然数.ZInt表示整数.在Z a b如果a >= b再整一个- b,否则- (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中,我只能看到一个原因.通过这种方式,我们可以在类型级别上定义整数.