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自动填充 's 类型。

这不适用于Sets，因为您可以：

{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只适用于Sets。

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

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

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; 这称为宇宙多态性。