types - Agda 中的大小类型是什么？

Question

Agda 中的大小类型是什么？我试图阅读有关MiniAgda的论文，但由于以下几点未能继续：

1. 为什么数据类型在它们的大小上是通用的？据我所知，大小是归纳树的深度。
2. 为什么数据类型在它们的大小上是协变的，即 i <= j -> T_i <= T_j ？
3. >和模式是什么#意思？

Answer 1

1. 这个想法是一个大小的类型只是一个按大小索引的类型家族，它们本质上是序数。将归纳类型定义为sized data时，编译器会检查结果是否为具有正确大小的类型，例如，succinSNat将大小增加 1。这样，对于已调整大小的类型S (i : Size) -> S i本质上是S具有 size的元素i。对我来说看起来很奇怪的是为什么零的定义SNat是zero : (i : Size) -> SNat ($ i)而不是像zero : (i : Size) -> SNat ($ 0).
2. 对于大小归纳类型，这是有道理的，因为 T_i 是 T 中大小小于i 的元素的类型，因此如果 i ≤ j 则 T_i ≤ T_j；构造函数必须增加递归调用的大小。

3. 如第 2.3 节所述，#等价于 T_∞，即 T 中没有已知大小界限的元素类型；这是子类型预排序中 T_i 的顶部元素。模式 (i > j) 用于绑定大小 j，同时保留 j < i 的信息。论文中的减号示例清楚地说明了这一点：

   fun minus : [i : Size] -> SNat i -> SNat # -> SNat i
   { minus i (zero (i > j)) y = zero j
   ; minus i x (zero .#) = x
   ; minus i (succ (i > j) x) (succ .# y) = minus j x y
   }
   

   首先，签名意味着SNat #从最多 i 个大小的数字（这就是SNat i意思）中减去任何数字（是一个没有大小限制信息的数字）返回最多 i 个大小的数字；对于>模式，在最后一行中，我们使用它来匹配最多 j 的多个大小，并且由于子类型：递归调用类型检查SNat j ≤ SNat i。