functional-programming - 如何在 Kind-Lang 等纯函数式语言中使用代数数据类型对 Int 类型进行编码？

Question

在 Kind-Lang 等函数式语言助手中，自然数通常被形式化为具有两个构造函数的递归代数数据类型，zero 和 succ:

type Nat {
  zero
  succ(pred: Nat)
}

至于 Int 类型，它也包含负数，在 Kind 上对其进行编码的最佳方法是什么？

Answer 1

编码 Int 类型的一种简单方法是制作一对 Nat和一个标志。例如:

Int: Type
  Pair<Bool, Nat>

但是，该定义存在一个问题:它包含两个零( -0 和 +0 )，因此，为了与传统的 Int 集同构，我们需要考虑在符号为负。因此，例如， {false, 2}代表 -3 , {false, 3}代表 -4 ， 等等。
Agda 使用类似的编码，而不是 Bool , 每个符号都有一个构造函数。我们可以将其移植为:

// Int.pos(n) represents +n
// Int.neg(n) represents -(n + 1)
type Int {
  pos(n: Nat)
  neg(n: Nat)
}

两种表示都有效，但使用它们来编写算法和证明定理是复杂且容易出错的。例如，这里是 add为 Int :

Int.negate(a: Int): Int
  case a {
    pos: case a.nat {
      zero: Int.pos(Nat.zero)
      succ: Int.neg(a.nat.pred)
    }
    neg: Int.pos(Nat.succ(a.nat))
  }

Int.add(a: Int, b: Int): Int
  case a b {
    pos pos: Int.pos(Nat.add(a.nat, b.nat))
    neg neg: Int.neg(Nat.succ(Nat.add(a.nat, b.nat)))
    pos neg: if b.nat <? a.nat
      then Int.pos((a.nat - b.nat) - 1)
      else Int.neg(b.nat - a.nat)
    neg pos: Int.add(Int.pos(b.nat), Int.neg(a.nat))
  }

一个更好的替代方法，常用于立方语言，是表示 Int作为商。例如，在 Agda 中，我们可以这样写:

data Int : Set where
  mkInt : (pos neg : Nat) -> Int
  canon : (pos neg : Nat) -> mkInt (suc pos) (suc neg) = mkInt pos neg

这样，我们将整数表示为一对两个 nat，整数表示为第一个自然数减去第二个自然数。因此，例如， mkInt 5 2代表 3 , 和 mkInt 2 5代表 -3 .这种编码的问题在于它有很多方法来表示相同的 Int。例如， 2可以表示为 mkInt 2 0 , mkInt 3 1 , mkInt 4 2等等。因此，这种类型不会与整数同构。然而，由于第二个参数，当我们用一个标识相同项的商扩展集合时。
在 Kind 中，我们没有直接商，但是，由于使用 Self 编码来表示底层数据类型，我们能够构建计算构造函数或智能构造函数。这些构造函数与常规构造函数类似，不同之处在于，在某些情况下，它们不会“卡住”。相反，计算以达到规范形式。这样，我们就可以对 Int 进行编码。以与上述编码类似的方式键入，加上导致 mkInt (succ i) (succ j) 的规则减少到 mkInt i j ，直到一个尺寸为零。所以，我们可以这样写:

type Int {
  new(pos: Nat, neg: Nat) with {
    zero zero: new(zero, zero)             // stuck, thus canonical
    zero succ: new(zero, succ(neg.pred))   // stuck, thus canonical
    succ zero: new(succ(pos.pred), zero)   // stuck, thus canonical
    succ succ: Int.new(pos.pred, neg.pred) // non-stuck, thus computes
  }
}

遗憾的是，上面的语法还没有在 Kind 中实现，但我们可以构建 Int (和类似类型)直接通过手动编写自己的编码:

Int: Type
  int<P: Int -> Type> ->
  (new: (pos: Nat) -> (neg: Nat) -> P(Int.new(pos, neg))) ->
  P(int)

Int.new(pos: Nat, neg: Nat): Int
  (P, new)
  case pos {
    zero: new(Nat.zero, neg)                     
    succ: case neg {
      zero: new(Nat.succ(pos.pred), Nat.zero)
      succ: Int.new(pos.pred, neg.pred)(P, new)
    }!
  }: P(Int.new(pos, neg))

这个定义有效并允许我们有更简单的算法和证明。例如，这里是 Int.add对于这种新类型:

Nat.add(n: Nat, m: Nat): Nat
  case n {
    zero: m
    succ: Nat.succ(Nat.add(n.pred, m))
  }

Int.add(a: Int, b: Int): Int
  open a
  open b
  Int.new(Nat.add(a.pos, b.pos), Nat.add(a.neg, b.neg))

注意它只是重用 Nat.add .与商相比，关于此的证明 Int更简单，因为 mkInt 3 1和 mkInt 2 0根据定义变得平等。

two_is_two: mkInt 3 1 == mkInt 2 0
  refl