理解 Agda 的语法
Understanding the syntax of Agda
以下面为例
postulate DNE : {A : Set} → ¬ (¬ A) → A
data ∨ (A B : Set) : Set where
inl : A → A ∨ B
inr : B → A ∨ B
-- Use double negation to prove exclude middle
classical-2 : {A : Set} → A ∨ ¬ A
classical-2 = λ {A} → DNE (λ z → z (inr (λ x → z (inl x)))
我知道这是正确的，纯粹是因为 agda 的工作原理，但我是这门语言的新手，无法理解它的语法是如何工作的，如果有人能告诉我发生了什么，我将不胜感激上，谢谢:)
我有 haskell 的经验，虽然那是大约一年前的事了。
让我们从假设开始。语法很简单：
postulate name : type
这断言存在一些名为 name 的 type 类型的值。将其视为逻辑中的公理 - 被定义为真实且不受质疑的事物（在这种情况下由 Agda 提出）。
接下来是数据定义。 mixfix 声明有一个轻微的疏忽，所以我会修复它并解释它的作用。第一行：
data _∨_ (A B : Set) : Set where
引入了一个名为 _∨_ 的新类型（构造函数）。 _∨_ 接受两个 Set 类型的参数，然后 returns 一个 Set.
我会将其与 Haskell 进行比较。 A 和 B 或多或少等同于以下示例中的 a 和 b：
data Or a b = Inl a | Inr b
这意味着数据定义定义了多态类型（模板或泛型，如果您愿意的话）。 Set 是 Haskell 的 *.
的 Agda 等价物
下划线是怎么回事？ Agda 允许您定义任意运算符（前缀、后缀、中缀……通常只是用一个名称调用 - mixfix）。下划线只是告诉 Agda 参数在哪里。这最好用 prefix/postfix 运算符看到：
-_ : Integer → Integer -- unary minus
- n = 0 - n
_++ : Integer → Integer -- postfix increment
x ++ = x + 1
您甚至可以创建疯狂的运算符，例如：
if_then_else_ : ...
下一部分是数据构造函数本身的定义。如果您看过 Haskell 的 GADT，这或多或少是一回事。如果你还没有：
当你在 Haskell 中定义构造函数时，比如上面的 Inr，你只需指定参数的类型，然后 Haskell 计算出整个事物的类型，即Inr :: b -> Or a b。当你在 Agda 中编写 GADT 或定义数据类型时，你需要指定整个类型（这是有充分理由的，但我现在不会深入）。
因此，数据定义指定了两个构造函数，A → A ∨ B 类型的 inl 和 B → A ∨ B 类型的 inr。
有趣的部分来了：classical-2 的第一行是一个简单的类型声明。 Set 是怎么回事？当你在Haskell中写多态函数时，你只是用小写字母来表示类型变量，比如：
id :: a -> a
你真正的意思是：
id :: forall a. a -> a
而你真正的意思是：
id :: forall (a :: *). a -> a
即它不仅仅是任何一种 a，而是 a 是一种类型。 Agda 让你做这个额外的步骤并显式地声明这个量化（那是因为你可以量化更多的东西而不仅仅是类型）。
还有花括号？让我再次使用上面的 Haskell 示例。当你在某处使用 id 函数时，比如 id 5，你不需要指定 a = Integer.
如果您使用正常的括号，则每次调用 classical-2 时都必须提供实际类型 A。但是，大多数时候，类型可以从上下文中推导出来（很像上面的 id 5 示例），因此对于这些情况，您可以 "hide" 参数。然后 Agda 尝试自动填充它 - 如果它不能，它会抱怨。
最后一行：λ x → y 是 Agda 表达 \x -> y 的方式。这应该可以解释大部分内容，唯一剩下的就是花括号了。我很确定你可以在这里省略它们，但无论如何：隐藏的参数做他们所说的 - 他们隐藏。因此，当您定义从 {A} 到 B 的函数时，您只需提供 B 类型的内容（因为 {A} 是隐藏的）。在某些情况下，您需要知道隐藏参数的值，这就是这种特殊类型的 lambda 的作用：λ {A} → 允许您访问隐藏的 A!
以下面为例
postulate DNE : {A : Set} → ¬ (¬ A) → A
data ∨ (A B : Set) : Set where
inl : A → A ∨ B
inr : B → A ∨ B
-- Use double negation to prove exclude middle
classical-2 : {A : Set} → A ∨ ¬ A
classical-2 = λ {A} → DNE (λ z → z (inr (λ x → z (inl x)))
我知道这是正确的，纯粹是因为 agda 的工作原理，但我是这门语言的新手，无法理解它的语法是如何工作的，如果有人能告诉我发生了什么，我将不胜感激上，谢谢:)
我有 haskell 的经验，虽然那是大约一年前的事了。
让我们从假设开始。语法很简单：
postulate name : type
这断言存在一些名为 name 的 type 类型的值。将其视为逻辑中的公理 - 被定义为真实且不受质疑的事物（在这种情况下由 Agda 提出）。
接下来是数据定义。 mixfix 声明有一个轻微的疏忽，所以我会修复它并解释它的作用。第一行：
data _∨_ (A B : Set) : Set where
引入了一个名为 _∨_ 的新类型（构造函数）。 _∨_ 接受两个 Set 类型的参数，然后 returns 一个 Set.
我会将其与 Haskell 进行比较。 A 和 B 或多或少等同于以下示例中的 a 和 b：
data Or a b = Inl a | Inr b
这意味着数据定义定义了多态类型（模板或泛型，如果您愿意的话）。 Set 是 Haskell 的 *.
下划线是怎么回事？ Agda 允许您定义任意运算符（前缀、后缀、中缀……通常只是用一个名称调用 - mixfix）。下划线只是告诉 Agda 参数在哪里。这最好用 prefix/postfix 运算符看到：
-_ : Integer → Integer -- unary minus
- n = 0 - n
_++ : Integer → Integer -- postfix increment
x ++ = x + 1
您甚至可以创建疯狂的运算符，例如：
if_then_else_ : ...
下一部分是数据构造函数本身的定义。如果您看过 Haskell 的 GADT，这或多或少是一回事。如果你还没有：
当你在 Haskell 中定义构造函数时，比如上面的 Inr，你只需指定参数的类型，然后 Haskell 计算出整个事物的类型，即Inr :: b -> Or a b。当你在 Agda 中编写 GADT 或定义数据类型时，你需要指定整个类型（这是有充分理由的，但我现在不会深入）。
因此，数据定义指定了两个构造函数，A → A ∨ B 类型的 inl 和 B → A ∨ B 类型的 inr。
有趣的部分来了：classical-2 的第一行是一个简单的类型声明。 Set 是怎么回事？当你在Haskell中写多态函数时，你只是用小写字母来表示类型变量，比如：
id :: a -> a
你真正的意思是：
id :: forall a. a -> a
而你真正的意思是：
id :: forall (a :: *). a -> a
即它不仅仅是任何一种 a，而是 a 是一种类型。 Agda 让你做这个额外的步骤并显式地声明这个量化（那是因为你可以量化更多的东西而不仅仅是类型）。
还有花括号？让我再次使用上面的 Haskell 示例。当你在某处使用 id 函数时，比如 id 5，你不需要指定 a = Integer.
如果您使用正常的括号，则每次调用 classical-2 时都必须提供实际类型 A。但是，大多数时候，类型可以从上下文中推导出来（很像上面的 id 5 示例），因此对于这些情况，您可以 "hide" 参数。然后 Agda 尝试自动填充它 - 如果它不能，它会抱怨。
最后一行：λ x → y 是 Agda 表达 \x -> y 的方式。这应该可以解释大部分内容，唯一剩下的就是花括号了。我很确定你可以在这里省略它们，但无论如何：隐藏的参数做他们所说的 - 他们隐藏。因此，当您定义从 {A} 到 B 的函数时，您只需提供 B 类型的内容（因为 {A} 是隐藏的）。在某些情况下，您需要知道隐藏参数的值，这就是这种特殊类型的 lambda 的作用：λ {A} → 允许您访问隐藏的 A!