abstract - Agda 标准库 - 为什么更多属性没有标记为抽象？

Question

过去几个月我一直在 Agda 中工作，我刚刚遇到了 Agda 中的 abstract block ，它阻止了该 block 范围之外的术语的进一步规范化。

使用它来隐藏我的引理的工作方式大大减少了对我的程序进行类型检查所需的时间。纵观 Agda 标准库，abstract 几乎没有被使用。在我看来，任何 Properties 文件中的几乎所有内容(例如 Data.Nat.Properties)都可以在 abstract block 内，因为我无法想到推理的用途，例如，如何证明加法是可交换的。

这是抽象作为尚未进入标准库的新功能的情况吗？或者我遗漏了标记证明摘要的一些微妙之处或缺点？

Answer 1

abstract 用于抽象事物，它会阻塞计算，因此如果将证明放在 abstract block 中，您将无法在 中使用它们subst 或 rewrite 同时仍保留规范性:

module _ where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.Fin hiding (_+_)

abstract
  +0 : ∀ n -> n + 0 ≡ n
  +0  0      = refl
  +0 (suc n) = cong suc (+0 n)

zero′ : ∀ n -> Fin (suc n + 0)
zero′ n = subst (Fin ∘ suc) (sym (+0 n)) zero

fail : zero′ 2 ≡ zero
fail = refl

-- subst ((λ {.x} → Fin) ∘ suc) (sym (+0 2)) zero != zero of type Fin (suc 2 + 0)
-- when checking that the expression refl has type zero′ 2 ≡ zero

即abstract block 与 postulate block 具有相同的效果。

如果将 abstract 替换为 module _ where，文件将类型为 check。

安德烈亚斯·阿贝尔 wrote :

I think this "abstract" feature is little understood. We should schedule it for removal, giving a grace period of say 5 years. If no one has a written a technical paper about it until 2020, with a proper semantics and a description of its intended interaction with metas, we drop it.