\ forall（∀）在簽名中究竟意味着什麼？

Question

從我收集的關於agda的信息中我可以得出結論∀ {A}相當於{A : Set}。現在我注意到，

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

是無效的（一些關於設置\歐米茄這又似乎是一些內部的東西，但

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

是罰款。任何人都可以清除此爲我？

Answer 1

這是因爲∀ {A}實際上只是爲{A : _}一個語法糖，它要求編譯器填充A的自動型。

這並不只Set的工作非常好，因爲你可以有：

{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作品。

但是，因爲它只是一個糖{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;這被稱爲宇宙多態性。