agda - Agda 中类型归属的一般形式是什么？

Question

背景:我正在研究 Prabakhar Ragde 的 "Logic and Computation Intertwined" ，对计算直觉逻辑的绝妙介绍。在他的最后一章中，他介绍了使用 Agda 的一些基础知识。我已经成功安装了 Agda 并设法扭转了 emacs 的 ARM (它花了很多时间!)让 agda-mode 工作得很好，但我觉得我缺少各种类型归属形式的总结 Agda 。

具体来说，在 Agda 中完成一个证明而不让我的脑袋爆炸需要大量的类型归属——我们只是说现在有这个类型，好吗？——我发现自己缺少将类型与名称相关联的能力以统一的方式。我现在知道有两种方法可以做到这一点，但我觉得我似乎缺少一种更通用的方法。

• 方法一:在使用“where”形式时，可以使用双行说明进行类型归属。
• 方法 2:使用显式 lambda 时，我可以使用圆括号和冒号将类型赋予标识符。

以下说明了这两者(使用 或 的定义以及简单但未包括在内的否定，抱歉):

ex9 : ∀ (A B : Set) → ¬ (¬ (or A (¬ A)))
ex9 A B aornotaimpliesbottom = aornotaimpliesbottom (or-intro-2 nota)
  where nota : ¬ (A)
        nota = λ (a : A) → aornotaimpliesbottom (or-intro-1 a)

方法一用于指定nota的类型，方法二用于指定nota的参数类型。

不过，问题来了:如果我想在“表达式”位置使用类型归属怎么办？例如，如果我想指定术语 (or-intro-1 a) 的类型怎么办？我可以使用“where”子句将其拉出到自己的绑定(bind)中，但是……哦，实际上，这似乎行不通；将“where”嵌入到 lambda 中未按预期工作。哦!看起来“让”在那里工作。好的，无论如何，问题仍然存在:是否有更轻量级的方法来指定内联表达式的类型？

Answer 1

您可以按如下方式定义内联类型注释:

infixl 0 _∋_
_∋_ : ∀{i}(A : Set i) → A → A
A ∋ x = x

或者从标准库中导入:

open import Function using (_∋_)

然后 A ∋ exp 用作任何表达式的内联类型注释。例如，在您的代码中:

nota = λ (a : A) → aornotaimpliesbottom (or A (¬ A) ∋ or-intro-1 a)

您还可以插入内联类型注释，或者有效地查询代码中已有的表达式的类型，方法是先插入一个洞，如下所示:

nota = λ (a : A) → aornotaimpliesbottom (? ∋ or-intro-1 a)

然后在洞中按 C-c-s，这会使用默认推理来填充洞。

同样要记住 let 在句法上比 where 更灵活。您可以将 let 放在任何表达式中，但 where 仅适用于绑定(bind)范围(在顶层，紧接在模块声明下，或紧接在函数右侧)。