functional-programming - 如何用像 Kind-Lang 这样的纯函数语言用代数数据类型对 Int 类型进行编码?
问题描述
在像 Kind-Lang 这样的函数式语言助手中,自然数通常被形式化为具有两个构造函数的递归代数数据类型:zero 和 succ:
type Nat {
zero
succ(pred: Nat)
}
至于 Int 类型,它也包括负数,在 Kind 上编码的最佳方法是什么?
解决方案
编码 Int 类型的一种简单方法是制作一对 aNat
和一个符号。例如:
Int: Type
Pair<Bool, Nat>
但是,该定义存在一个问题:它包含两个零(-0
和+0
),因此,为了与传统的 Int 集合具有同构,我们需要考虑当符号为负时该数字加 1。因此,例如,{false, 2}
表示-3
、{false, 3}
表示-4
等。
Agda 使用类似的编码,而不是 a 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 中,我们没有直商,但是由于使用自编码来表示底层的数据类型,我们能够构建计算的构造函数或智能构造函数。这些构造函数与常规构造函数类似,只是在某些情况下,它们不会“卡住”。相反,计算达到规范形式。这样,我们可以Int
以与上面的编码类似的方式对类型进行编码,加上一个导致mkInt (succ i) (succ j)
reduce到的规则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
推荐阅读
- mysql - MySQL C API。从表中检索信息的问题解决方案
- windows - Powershell - 通过 Web 界面调用新网站 cmdlet 时不起作用
- azure - Azure 数据工厂自动重新触发失败的管道
- phpstorm - 在 PhpStorm 代码检查中忽略函数的多个定义
- macos - 使用--network = host在MacOS上运行docker容器时如何访问主机上的端口?
- python - 在熊猫数据框中附加两列的最小值
- python - 我正在尝试为 python3.7 获取项目
- javascript - 如何使用 Lodash 根据对象的嵌套属性值选择对象的属性?
- import - 在 teraform 中,有没有办法在不使用 CLI 命令的情况下使用 TF 文件刷新资源状态?
- python - bt - Python 的灵活回测 - 如何获得每个给定日期的总投资组合价值/结果?