Why? [tt-0001]

strictly positive 是 data type 中對 constructor 的一種特殊要求形成的屬性，這是因為如果一個語言可以定義出不是 strictly positive 的 data type，就可以在 type as logic 中定義出任意邏輯，形成不一致系統。

現在我們知道為什麼我們想知道一個 data type 是不是 strictly positive 了！了解完 strictly positive 的必要性後，我們用例子來理解什麼是不一致的系統，第一個例子是 not-bad ：

Example. Not Bad [tt-0004]

data Bad
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             bad : (Bad → Bottom) → Bad

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           notBad : Bad → Bottom
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           notBad (bad f) = f (bad f)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           isBad : Bad
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           isBad = bad notBad

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           absurd : Bottom
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           absurd = notBad isBad

Bottom ( $\bot$ ) 本來應該是不可能有任何元素的，即不存在 x 滿足 x : Bottom 這個 judgement，但我們卻成功的建構出 notBad isBad : Bottom。如此一來我們的型別對應到的邏輯系統就有了缺陷。

Example. Loop [tt-0005]

現在我們關心一下第二個例子 loop（修改自 Certified Programming with Dependent Types）：

data Term
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             abs : (Term → Term) → Term

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           app : Term → Term → Term
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           app (abs f) t = f t

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           w : Term
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           w = abs (λ x → app x x)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           loop : Term
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           loop = app w w

loop 的計算永遠都不會結束，然而證明器用到的 dependent type theory 卻允許型別依賴 loop 這樣的值，因此就能寫出讓 type checker 無法停止的程式。換句話說，證明器仰賴的性質缺失。事實上 Term 跟 Bad 的問題就是違反了 strictly positive 的性質，或許也有人已經發現了兩者 constructor 型別的相似之處。接下來我們來看為什麼這樣的定義會製造出不一致邏輯。

原理 [tt-0002]

首先我們需要理解以下兩條規則

$B \subseteq B'$ 蘊含 $(A \Rightarrow B) \subseteq (A \Rightarrow B')$
$A \subseteq A'$ 蘊含 $(A' \Rightarrow B) \subseteq (A \Rightarrow B')$

根據這兩條規則，我們說 arrow type $A \Rightarrow B$

contravariant in $A$ （或 $A$ varies negatively）
covariant in $B$ （或 $B$ varies positively

所以我們稱 $A$ 為 negative position、 $B$ 為 positive position

實作 [tt-0003]

而 strictly positive 就是說，inductive family $D$ 自己不可以出現在 negative position

在 Agda 的文件中也有解釋：任何 constructor 都形如

(y_1 : B_1) \to \dots \to (y_m : B_m) \to D

而每個 $B_i$ 都可以不提到 $D$ 或是形如

(z_1 : C_1) \to \dots \to (z_m : C_m) \to D

$C_j$ 不可以等於 $D$

文章到這邊告一段落，也解決了我這一年來對證明器實作的最大疑問之一，進一步的解答可以參考 https://cs.stackexchange.com/questions/55646/strict-positivity/55674#55674