This document outlines our choices of conventions for setting precedence levels and associativity of mixfix operators in Agda, and provides guidelines for this.
Infix operators in Agda are binary operators that take arguments on either side.
For example, addition is commonly written in infix notation as 1 + 2. Mixfix
operators are operators with longer names potentially containing multiple
components, where the arguments appear between the components. For example, the
commutator [a,b] is a common mixfix operator. The purpose of introducing infix
and mixfix operators in Agda is to make the code more readable by using commonly
accepted notation for widely used operators.
Mixfix operators can each be assigned a
precedence level.
This can in principle be any signed fractional value, although we prefer them to
be nonnegative integral values. The higher this value is, the higher precedence
the operator has, meaning it is evaluated before operators with lower
precedence. By default in Agda, an operator is assigned a precedence level of
20.
For instance,
multiplication on natural numbers _*ℕ_
is assigned the precedence level 40, and
addition on natural numbers _+ℕ_
is assigned the precedence level 35. Therefore, the expression x +ℕ y *ℕ z
is parsed as x +ℕ (y *ℕ z).
In addition to a precedence level, every infix operator can be defined to be
either left or right
associative
using the keywords infixl and infixr. It can be beneficial to define
associativity of operators to avoid excessively parenthesized expressions. The
parenthization should, however, never be omitted when this can make the code
more ambiguous or harder to read.
For instance, since the
pairing operator _,_ is defined to
associate to the right, the expression a , b , c is parsed as a , (b , c).
By default, an operator does not associate to either side.
We divide the different operators into broad classes, each assigned a range of
possible precedence levels. In broad terms, we discern between parametric and
nonparametric operators. The general rule is that nonparametric operator has
higher precedence than parametric operators. Parametric operators are operators
that take a universe level as one of their arguments. We consider an operator to
be parametric even if it only takes a universe level as an implicit argument.
Examples are the
cartesian product type former_×_,
the identity type former _＝_, and the
pairing operator _,_. Examples of
nonparametric operators are
difference of integers _-ℤ_,
strict inequality on natural numbers _<-ℕ_,
and
multiplication of Eisenstein integers _*ℤ[ω]_.
Within these two classes, we make a further distinction between relational, additive, multiplicative, exponentiative, and unary operators, each with a higher precedence than the previous one. All together, we assign ranges as outlined below.
| Relations | Additive | Multiplicative | Exponentiative | Unary | |
|---|---|---|---|---|---|
| Parametric Operators | 5-9 | 10-14 | 15-19 | 20-24 | 25-29 |
| Nonparametric Operators | 30-34 | 35-39 | 40-44 | 45-49 | 50-54 |
Note that the default precedence level (20) falls within the range of
exponentiative parametric operators.
As a rule of thumb, the lowest value in a range is assigned by default. The notable exceptions are outlined below.
In this section, we outline special rules for assigning precedence levels to particular classes of operators. Please make sure to update this section if new rules are implemented.
In Agda, the arrow notation _→_ for function type formation is directly
handled by the parser, hence it has hardcoded precedence and right
associativity. In particular, it has lower precedence than any user-declared
operator. To make other directed arrow notations like
pointed function type formation _→∗_ and
embedding type formation _↪_ consistent with
this, we consider them as relational operators and assign them a precedence
level of 5, and usually define them to be right associative. Other
relational operators are assigned the precedence level 6 by default.
The pairing operators _,_ and
_,ω_ are assigned a low precedence
level of 3, below any of the above defined classes.
Reasoning syntaxes, like
equational-reasoning, is defined using
Agda's mixfix operators, and should have lower precedence than all other
operators (notably except for the built-in _→_). The precedence value range
0-1 is reserved for these.
We consider the class of subtractive operators as a subclass of additive
operators. These include operators like
difference of integers _-ℤ_.
Subtractive operators will usually have higher precedence than additive
operators, so that expressions like a - b + c are parsed as (a - b) + c.
Below, we outline a list of general rules when assigning associativities.
-
Strictly associative operators, e.g. function composition
_∘_, can be assigned any associativity. -
Nonparametric arithmetic operators are often naturally computed from left to right. For instance, the expression
1 - 2 - 3is computed as(1 - 2) - 3 = -1 - 3 = -4, hence should be left associative. This applies to addition, subtraction, multiplication, and division. Note that for nonparametric exponentiation, we compute from right to left. I.e.2 ^ 3 ^ 4should compute as2 ^ (3 ^ 4). Hence it will usually be right associative. -
Arithmetic type formers such as coproduct type formation
_+_and cartesian product type formation_×_, are natural to parse from left to right in terms of their introduction/elimination rules. Therefore, they are commonly associated to the right. This means that for instance to map into the left-hand argument ofA + B + C, one uses a singleinl. -
Weakly associative operators, meaning operators that are associative up to identification, may still be practical to define an associativity for, for cases when the particular association does not matter and you still want to apply the operator multiple times. For instance, when performing an equality proof by a string of concatenations. For this reason, we define identification concatenation
_∙_and homotopy concatenation_∙h_to be left associative. Please note that parenthization should still only be omitted when the association is of no importance, even if your expression is left associated regardless. For instance, one should never writeassoc : p ∙ q ∙ r ＝ p ∙ (q ∙ r)
-
Unique well-typed associativity. When an operator only has one well-typed associativity, then one can define it to have that associativity. For instance, with homotopy left whiskering,
f ·l g ·l His only ever well-typed when associated to the right.
| Precedence level | Operators |
|---|---|
| 50 | Unary nonparametric operators. This class is currently empty |
| 45 | Exponentiative arithmetic operators |
| 40 | Multiplicative arithmetic operators |
| 36 | Subtractive arithmetic operators |
| 35 | Additive arithmetic operators |
| 30 | Relational arithmetic operators like_≤-ℕ_ and _<-ℕ_ |
| 25 | Parametric unary operators like ¬_ and ¬¬_ |
| 20 | Parametric exponentiative operators. This class is currently empty |
| 17 | Left homotopy whiskering _·l_ |
| 16 | Right homotopy whiskering _·r_ |
| 15 | Parametric multiplicative operators like _×_,_×∗_, _∧_, _∧∗_, _*_, function composition operators like _∘_,_∘∗_, _∘e_, and _∘iff_, concatenation operators like _∙_ and _∙h_ |
| 10 | Parametric additive operators like _+_, _∨_, _∨∗_, list concatenation, monadic bind operators for the type checking monad |
| 6 | Parametric relational operators like _＝_, _~_, _≃_, _⇔_, and _↔_, elementhood relations, subtype relations |
| 5 | Directed function type-like formation operators, e.g. _⇒_, _↪_, _→∗_, _↠_, _↪ᵈ_, and _⊆_ |
| 3 | The pairing operators _,_ and _,ω_ |
| 0-1 | Reasoning syntaxes |
| -∞ | Function type formation _→_ |