Created on 2023-09-10.
Last modified on 2023-12-08.
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
[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
This can in principle be any signed fractional value, although we prefer them to
be non-negative 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
multiplication on natural numbers
is assigned the precedence level
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
using the keywords
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
_,_ 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
non-parametric operators. The general rule is that non-parametric 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
_,_. Examples of
non-parametric operators are
difference of integers
strict inequality on natural numbers
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.
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
embedding type formation
_↪_ consistent with
this, we consider them as relational operators and assign them a precedence
5, and usually define them to be right associative. Other
relational operators are assigned the precedence level
6 by default.
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.
Definitionally associative operators, e.g. function composition
_∘_, can be assigned any associativity.
Non-parametric 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 non-parametric exponentiation, we compute from right to left. I.e.
2 ^ 3 ^ 4should compute as
2 ^ (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 of
A + B + C, one uses a single
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 write
assoc : 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.
|50||Unary non-parametric 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|
|25||Parametric unary operators. This class is currently empty|
|20||Parametric exponentiative operators. This class is currently empty|
|17||Left homotopy whiskering |
|16||Right homotopy whiskering |
|15||Parametric multiplicative operators like |
|10||Parametric additive operators like |
|6||Parametric relational operators like |
|5||Directed function type-like formation operators, e.g. |
|3||The pairing operators |
|-∞||Function type formation |
- 2023-12-08. Fredrik Bakke. Improve generality of homotopy whiskering operations (#976).
- 2023-11-20. Fredrik Bakke. Fix some typos in the mixfix guide (#928).
- 2023-10-18. Egbert Rijke. Fix broken links in
- 2023-10-16. Fredrik Bakke and Egbert Rijke. The decidable total order on a standard finite type (#844).
- 2023-09-10. Fredrik Bakke.