在阿格达语中，似乎通常有两种方法可以细化一个集合。一种是简单地编写一个函数来检查属性是否成立，然后提升。例如：
has_true : List Bool -> Bool
has_true (true ∷ xs) = true
has_true (false ∷ xs) = has_true xs
has_true [] = false
Truthy : List Bool -> Set
Truthy list = T (has_true list)
在这里，Truthy list布尔列表至少有一个 true 元素的证明。另一种方法是直接将该属性编码为归纳类型：
data Truthy : List Bool -> Set where
Here : (x : Bool) -> (x ≡ true) -> (xs : List Bool) -> Truthy (x ∷ xs)
There : (x : Bool) -> (xs : List Bool) -> Truthy xs -> Truthy (x ∷ xs)
在这里，Truthy list也证明了同样的事情。
我相信我以前读过比较，但我不记得了。这些不同的风格有名字吗？使用一种样式与另一种样式相比有哪些优点和缺点？还有第三种选择吗？
到目前为止，您列出了定义谓词的两种方法：
A -> Bool功能。- 归纳谓词。
我还要补充一个：
A -> Set函数。也可以称为"递归定义"或"由大消除定义"。
第三个版本在阿格达语中如下：
open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Data.List
hastrue : List Bool → Set
hastrue [] = ⊥ -- empty type
hastrue (false ∷ bs) = hastrue bs
hastrue (true ∷ bs) = ⊤ -- unit type
首先，让我们谈谈使用这三个选项可以表示什么样的谓词。下面是一个 ASCII 表。*是代表是/否的通配符。
| P : A -> Set | P : A -> Bool | data P : A -> Set |
|-------------------|--------------|---------------|-------------------|
| Proof irrelevant | * | yes | * |
| Structural | yes | yes | * |
| Strictly positive | * | N/A | yes |
| Decidable | * | yes | * |
证明不相关意味着P x的所有证明都是平等的。在Bool情况下，一个证明通常是一些p : P x ≡ true，或者与IsTrue = λ b → if b then ⊤ else ⊥p : IsTrue (P x)，在这两种情况下，所有的证明都是相等的。我们可能希望也可能不希望谓词无关紧要。
结构意味着P x只能使用结构小于x的A元素来定义。函数总是结构性的，所以如果某些谓词不是，那么它只能归纳定义。
严格正意味着P不能递归出现在函数箭头的左侧。非严格正谓词不能归纳定义。证明相关的非严格正谓词的一个例子是对函数类型代码的解释：
data Ty : Set where
top : Ty
fun : Ty → Ty → Ty
⟦_⟧ : Ty → Set
⟦ top ⟧ = ⊤
⟦ fun A B ⟧ = ⟦ A ⟧ → ⟦ B ⟧ -- you can't put this in "data"
可决定性是不言自明的;A -> Bool函数必然是可判定的，这使得它们不适合不可判定或不能轻易写出结构Bool函数的谓词。可判定性的优点是排除了中间推理，如果没有假设或额外的可判定性证明，非Bool谓词定义是不可能的。
第二，关于阿格达/伊德里斯的实际影响。
您可以在归纳谓词的证明上进行相关模式匹配。对于递归谓词和布尔谓词，必须先对
A值进行模式匹配，以使谓词见证进行计算。有时，这使得归纳谓词很方便，例如，您可能有一个具有 10 个构造函数的枚举类型，并且您希望谓词仅保留一个构造函数。归纳定义的谓词允许您只匹配真实情况，而其他版本要求您始终匹配所有情况。另一方面，布尔谓词和递归谓词会在您知道
A元素具有给定形状后立即自动计算。这可以在 Agda 中使用，使类型推断自动填充证明，无需策略或实例。例如，类型为hastrue xs的洞或隐式参数可以通过对和单位类型的 eta 规则来解决，只要xs是具有已知含true前缀的列表表达式。这与布尔谓词类似。