What does \forall (∀) actually mean in a signature?

Question

From the bits and pieces of information I gathered about agda I'd (apparently erroneously) concluded that ∀ {A} was equivalent to {A : Set}. Now I noticed that

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

is invalid (something about Set\omega which in turn seems to be some internal something, but

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

is fine. Can anyone clear this up for me?

Answer 1

That's because ∀ {A} is actually just a syntactic sugar for {A : _}, which asks the compiler to fill A's type automatically.

This doesn't work quite well with just Sets, because you could have:

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

And indeed, all of those are valid types in your definition. ∀ really only makes sense when the thing that follows can be unambiguously determined by its use.

For example, consider this definition:

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

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

The type of A must be Set, because List only works with Sets.

However, because it's just a sugar for {A : _} that means it works with much more than just Sets.

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

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

Or perhaps the most common use case:

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

The type of a and b is Level; this is called universe polymorphism.