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

Question

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

使用它来隐藏我的引理的工作大大减少了对我的程序进行类型检查所需的时间。浏览 Agda 标准库，但几乎没有使用 abstract。在我看来，任何 Properties 文件（例如 Data.Nat.Properties）中的几乎所有内容都可以在 abstract 块中，因为我想不出推理的用途，例如，如何证明加法是可交换的。

这是否是抽象作为尚未进入标准库的新功能的情况？还是我遗漏了标记校样 abstract 的一些细微之处或缺点？

Answer 1

abstract 用于抽象事物，它会阻塞计算，因此如果您将证明放在 abstract 块中，您将无法在 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 块与 postulate 块具有相同的效果。

如果将 abstract 替换为 module _ where，文件将进行类型检查。

安德烈亚斯·阿贝尔 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.

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

Agda standard library - why are more properties not marked abstract?

standard-library

abstract

agda