Mixfix operators in agda-unimath

Created on 2023-09-10.
Last modified on 2024-04-11.

This document outlines our choices of conventions for setting precedence levels and associativity of mixfix operators in Agda, and provides guidelines for this.

Mixfix operators in Agda

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.

Operator classes

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.

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.

Special rules for assigning precedence levels

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.

Function type like formation operators

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.

Pairing operators

The pairing operators _,_ and _,ω_ are assigned a low precedence level of 3, below any of the above defined classes.

Reasoning syntaxes

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.

Subtractive operators

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.

Assigning associativities

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 - 3 is 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 ^ 4 should 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 inl.

• 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 H is only ever well-typed when associated to the right.

Full table of assigned precedences

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 2024-03-19. Fredrik Bakke. chore: fix some typos in the library (#1083).
• 2024-02-08. Fredrik Bakke. Computational identity types (#1015).
• 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
• 2023-12-12. Fredrik Bakke. Some minor refactoring surrounding Dedekind reals (#983).