如何解决agda 模式如何与相同类型的构造函数匹配?
我已经开始阅读 Programming Language Foundations in Agda 书,但在尝试执行要求您编写 inc
函数的练习时感到困惑,该函数增加由以下 {{} 表示的二进制数1}} 类型:
Bin
我开始编写我的 data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
函数
inc
然后想:“如果 inc_ : Bin → Bin
inc ⟨⟩ = ⟨⟩
inc (x O) = {!!}
inc (x I) = {!!}
和 { {1}} 构造函数具有相同的类型?”。如果我们以 Bin
为例:
x O
x I
和 _O
构造函数都产生 _I
类型的值,那么 Agda 如何知道 Nat
类型的某个特定值是否与我拥有的模式匹配data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
?
zero
在我看来,唯一可行的方法是 Agda 跟踪用于创建每个值的 构造函数,然后允许在模式匹配中使用相同的构造函数?
我对 Agda 非常陌生,并试图围绕类型、值、构造函数和模式匹配之间的关系进行思考。我非常感谢参考我的问题中的 succ
和 ℕ
示例来解释这些之间的关系。我曾尝试阅读一些额外的文章/书籍/讲座和 Agda 文档,但我找不到这个问题的答案。
解决方法
这个问题首先出现在一个非常简单的类型——布尔值中:
data Bool : Set where
true : Bool
false : Bool
我们可以通过模式匹配从Bool
中写出函数,例如:
not : Bool → Bool
not true = false
not false = true
Bool
与其他编程语言中的类似类型一样,是一种具有两个规范居民的类型:true
和 false
。 Bool
值存储 1 位信息。在运行时,也为了类型检查时的计算,我们可以想象在指定的内存位置中有一个位表示该值是true
还是false
。
就 data
声明而言,出现这一点是因为 Bool
有两个构造函数。类似地,ℕ
有两个构造函数,因此它也会包含一个指示值是 zero
还是 suc
的位(如果它是 suc
,还会有是指向其余数字的指针)。对于 Bin
,我们将存储 0、1 或 2,以指示我们是否有 ⟨⟩
、_O
或 _I
。
模式匹配依赖的正是这些额外的信息(这里的示例为一或两位)。事实上,类型通常会被擦除,因此模式匹配无法使用它们。因此,not
本质上被编译为类似于以下伪 C 的内容。
int* not(int* b) {
switch (*b) { // Look at the tag of b.
case 0: // If b is true,int* r = malloc(sizeof(int)); // Allocate a new boolean;
*r = 1; // Set the value of the new boolean to false;
return r; // Return the new boolean.
case 1: // If b is false,int* r = malloc(sizeof(int)); // Allocate a new boolean;
*r = 0; // Set the value of the new boolean to false;
return r; // Return the new boolean.
}
}
与此同时,_+_
上的 ℕ
函数将被编译为类似:
int* add(int* n,int* m) {
switch (*n) { // Look at the tag of n.
case 0: // If n is zero,return m; // Return m.
case 1: // If n is a suc,int* r = malloc(2 * sizeof(int)); // Allocate space for a suc cell;
*r = 1; // Indicate that it is a suc by setting the tag to 1;
*(r+1) = add(n+1,m); // After the tag is a pointer,set to the result of the recursive call to add.
return r; // Return the new ℕ.
}
}
注意这里的n+1
是指n
的标签之后的内存位置,即指向n
的前驱(Agda代码中的n-1
) .为简单起见,我假设 sizeof(int) = sizeof(int*)
,并且可以将指针存储在 int
类型中。关键的细节是我们总是用它们构成的构造函数来标记 data
值,并且完成此操作后,通过模式匹配进行分支相当于查看此标记。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。