Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?

like image 402
Cubic Avatar asked Dec 08 '13 23:12

Cubic


1 Answers

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.

like image 94
Vitus Avatar answered Nov 16 '22 23:11

Vitus