Agda：通常/大括号如何相对于彼此以及“：”符号

如何解决Agda：通常/大括号如何相对于彼此以及“：”符号

我无法理解此语法。我在 Agda 教程手册中没有找到我的问题的答案。我发现的唯一一件事是 (x : A) -> (y : A) -> B 糖化为 (x : A)(y : A) -> B，而 (x y : A) -> B 糖化为 map : {A B : Set} -> (A -> B) -> List A -> List B，但这不是故事的全部。

困扰我的是类型声明：

map : {A B : Set} (A -> B) -> List A -> List B

很好，虽然

singleton : {A : Set} -> (x : A) → List A

不是。

参数之间带有箭头的版本

singleton : {A : Set}(x : A) → List A

很好，而没有箭头的相同表达

data _≡_ {a}{P : Set a} (x : P) : P → Set a where refl : x ≡ x

还是可以的。

参数之间带有':'的版本

data _≡_ :  ∀{a}{P : Set a} (x : P) →  P → Set a where
  refl :  x ≡ x

很好，虽然

onStateChange

不是。

在 Haskell 中只有普通的大括号，每个大括号用箭头分隔。在 Agda 中，有更多的语法糖，没有涉及太多。

解决方法

同时

data _≡_ :  ∀{a}{P : Set a} (x : P) →  P → Set a where
  refl :  x ≡ x

不是。

这个例子解析得很好；错误来自范围检查：

Not in scope:
  x at ...
when scope checking x

这个错误超出了这个问题的范围。但是，正如您似乎注意到的那样，您对 _≡_ 的两个假定定义之间有很多相似之处：∀ 符号告诉解析器接下来的内容应该作为参数列表进行解析（就像之前的冒号属于 _≡_)，但可以理解为 Curried 参数列表。 ∀ 的主要实际用途是区分 x → P x 和 ∀ x → P x。前者脱糖为(_ : x) → P x（即x是一种类型），后者脱糖为(x : _) → P x（即x代表某个个体，其类型推导来自 P 的类型）。

我认为您的其他测试用例现在大部分都可以解决了。以下没有加糖形式，因为 A → B 参数没有命名。

困扰我的是类型声明：

map : {A B : Set} -> (A -> B) -> List A -> List B

很好，虽然

map : {A B : Set} (A -> B) -> List A -> List B

不是。

你可以改为：

 map : {A B : Set} (f : A -> B) -> List A -> List B

或

 map : {A B : Set} (_ : A -> B) -> List A -> List B

如果你真的想要。