Agda: How usual/curly braces are used relative to each other and to ':' sign

Question

I have trouble understanding this syntax. I didn't find the answer to my quesion in the Agda tutorial manual. The only thing I found was that (x : A) -> (y : A) -> B sugars to (x : A)(y : A) -> B which sugars into (x y : A) -> B, but this isn't the whole story.

What troubles me is that type declaration:

map : {A B : Set} -> (A -> B) -> List A -> List B

is fine, while

map : {A B : Set} (A -> B) -> List A -> List B

is not.

Version with arrow between arguments

singleton : {A : Set} -> (x : A) → List A

is fine, while the same expression without arrow

singleton : {A : Set}(x : A) → List A

is still fine.

The version with ':' between arguments

data _≡_  {a}{P : Set a} (x : P) : P → Set a where
  refl : x ≡ x

is fine, while

data _≡_ :  ∀{a}{P : Set a} (x : P) →  P → Set a where
  refl :  x ≡ x

is not.

In Haskell there is just regular braces, each separated with arrows. In Agda there is a lot more syntactic sugar, which isn't covered that much.

Answer 1

while

data _≡_ :  ∀{a}{P : Set a} (x : P) →  P → Set a where
  refl :  x ≡ x

is not.

This example parses fine; the error is from scope checking:

Not in scope:
  x at ...
when scope checking x

This error is beyond the scope of this question. As you seem to be noticing, though, there is a lot of similarity between your two putative definitions of _≡_: the ∀ symbol tells the parser that what follows should parse as a parameter list (like before the colon pertaining to the _≡_), but be understood as a list of Curried arguments. The main practical use of ∀ is to distinguish between x → P x and ∀ x → P x. The former desugars to (_ : x) → P x (i.e, x is a type), while the latter desugars to (x : _) → P x (i.e, x stands for some individual, and its type is deduced from the type of P).

I think your other test cases can now mostly be worked out. The following doesn't have a sugared form because the A → B argument isn't given a name.

What troubles me is that type declaration:

map : {A B : Set} -> (A -> B) -> List A -> List B

is fine, while

map : {A B : Set} (A -> B) -> List A -> List B

is not.

You could instead write:

 map : {A B : Set} (f : A -> B) -> List A -> List B

or

 map : {A B : Set} (_ : A -> B) -> List A -> List B

if you really wanted.