显然，Agda 中有一个称为阳性检查的功能，它显然可以保持系统声音even if type-in-type is enabled。
我很想知道这是关于什么的，但是the Agda Manual fails to answer the question, and only explains how to turn it off。
在一张午餐桌上，我无意中听到这是关于 polarity in type theory 的消息，但我所知道的仅此而已。我在网上找不到任何解释这个概念以及为什么它对保持健全性有用的东西。任何可理解的解释将不胜感激。
【问题讨论】：
标签： agda theorem-proving type-theory
首先，我必须澄清一个误解：启用输入类型时，积极性检查并不能保证正确性。因此，数据类型必须同时满足积极性检查和全域检查以保持稳健性。
现在，为了解释阳性检查，让我们先看一个没有阳性检查的反例：
-- 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，在构造类型论的模型（用来证明可靠性）时，可以用来对数据类型进行建模。
【讨论】：