agda -\forall (∀) 在签名中实际上是什么意思？

Question

从我收集到的有关 agda 的零碎信息中，我(显然是错误地)得出的结论是 ∀ {A}相当于 {A : Set} .现在我注意到

flip : ∀ {A B C} -> (A -> B -> C) -> (B -> A -> C)

是无效的(关于 Set\omega 的东西又似乎是一些内部的东西，但是

flip : {A B C : Set} -> (A -> B -> C) -> (B -> A -> C)

很好。谁能帮我解决这个问题？

Answer 1

那是因为 ∀ {A}实际上只是 {A : _} 的语法糖，它要求编译器填写 A的类型自动。

仅使用 Set 就不能很好地工作s，因为你可以:

{A : Set}
{A : Set₁}
{A : Set₂}
-- etc.

事实上，所有这些都是您定义中的有效类型。 ∀只有当后面的东西可以通过它的用途明确地确定时，才真正有意义。

例如，考虑这个定义:

data List (A : Set) : Set where
  -- ...

map : ∀ {A B} → (A → B) → List A → List B
map = -- ...

A的类型必须是 Set , 因为 List仅适用于 Set s。

然而，因为它只是 {A : _} 的糖这意味着它不仅适用于 Set s。

_+_ : ℕ → ℕ → ℕ
_+_ = -- ...

comm : ∀ x y → x + y ≡ y + x
comm = -- ...

或者也许是最常见的用例:

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B

a的类型和 b是 Level ;这称为宇宙多态性。