agda 模式如何与相同类型的构造函数匹配？

Question

我已经开始阅读 Programming Language Foundations in Agda 这本书，但在尝试执行要求您编写一个 inc 函数的练习时感到困惑，该函数递增由以下表示的二进制数Bin 类型：

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

我开始将 inc 函数编写为

inc_ : Bin → Bin
inc ⟨⟩ = ⟨⟩
inc (x O) = {!!}
inc (x I) = {!!}

然后想：“如果 _O和 _I 构造函数具有相同的类型？”。我越想越糊涂，如果我们以 Nat 为例：

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

zero 和 succ 构造函数都产生一个 ℕ 类型的值，那么 Agda 如何知道 ℕ 类型的某些特定值是否与模式匹配我已经准备好 _+_?

等功能

_+_ : ℕ → ℕ → ℕ
zero + m = m
succ n-1 + m = succ (n-1 + m)

在我看来，唯一可行的方法是 Agda 跟踪用于创建每个值的 构造函数 ，然后允许在模式匹配中使用相同的构造函数？

我是 Agda 的新手，我正在努力了解类型、值、构造函数和模式匹配之间的关系。我非常感谢您解释这些与我问题中的 Bin 和 ℕ 示例有何关系。我已经尝试阅读一些额外的 articles/books/lecture 方面和 Agda 文档，但我找不到这个问题的答案。

Answer 1

这个问题首先出现在一个非常简单的类型——布尔值上：

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 值由它们构成的构造函数，并且完成此操作后，通过模式匹配进行分支相当于查看此标记。

agda 模式如何与相同类型的构造函数匹配？

How does agda pattern match with same typed constructors?

constructor

types

pattern-matching

agda