agda - 什么是阳性检查？

Question

这个问题已经有答案了:

"Strictly positive" in Agda (1 个回答)

已关闭 5 年前。

显然，Agda中有一个名为积极性检查的功能，它显然可以保持系统健全even if type-in-type is enabled .

我很想知道这是关于什么的，但是the Agda Manual fails to answer the question, and only explains how to turn it off .

在午餐 table 上我无意中听到这是关于 polarity in type theory ，但这就是我所知道的全部。我在网上找不到任何可以解释这个概念以及为什么它对于保持健全性有用的内容。任何可以理解的解释将不胜感激。

Answer 1

首先，我必须澄清一个误解:启用 type-in​​-type 时，积极性检查并不能保证健全性。因此，数据类型必须满足正性检查和宇宙检查以保持健全性。

现在，为了解释积极性检查，让我们首先看一个不进行积极性检查的反例:

-- the empty type
data ⊥ : Set where

-- a non-positive type
data Bad : Set where
  bad : (Bad → ⊥) → Bad

假设允许这种数据类型，那么您可以轻松证明⊥:

bad-is-false : Bad → ⊥
bad-is-false (bad f) = f (bad f)

bad-is-true : Bad
bad-is-true = bad bad-is-false

boom : ⊥
boom = bad-is-false bad-is-true

根据 Curry-Howard 对应关系，Bad 的定义是:当且仅当 Bad 为假时，Bad 才为真。因此，它导致不一致也就不足为奇了。

积极性检查排除了诸如“Bad”之类的数据类型。一般来说，(严格)积极性标准表示数据类型 D 的每个构造函数 c 应该具有以下形式的类型

c : (x1 : A1)(x2 : A2) ... (xn : An) → D xs

其中每个参数的类型 Ai 要么是非递归的(即它不引用 D)，要么是 (y1 : B1)(y2 : B2) 的形式。 .. (ym : Bm) → D ys 其中每个 Bj 并不引用 D。

Bad 不满足此条件，因为构造函数 bad 的参数具有类型 Bad → ⊥，这两者都不是允许的形式。

“正性检查”这个名字(就像类型论中的许多东西一样)来自范畴论，特别是正内仿函数的概念。满足正性标准的数据类型的每个定义都是类型类别上的正内仿函数。这意味着我们可以构造initial algebra该endofunctor的，可用于在构建类型论模型(用于证明可靠性)时对数据类型进行建模。