Mixfix Operators

A type name, function name, or constructor name can comprise one or more name parts if we separate them with underscore characters _, and the resulting name can be used as an operator. From left to right, each argument goes in the place of each underscore _.

For instance, we can join with underscores the name parts if, then, and else into a single name if_then_else_. The application of the function name if_then_else_ to some arguments named x, y, and z can still be written as:

  • a standard application by using the full name if_then_else_ x y z

  • an operator application by placing the arguments between the name parts if x then y else z, leaving a space between arguments and part names

  • other sections of the full name, for instance leaving one or two underscores:

    • (if_then y else z) x

    • (if x then_else z) y

    • if x then y else_ z

    • if x then_else_ y z

    • if_then y else_ x z

    • (if_then_else z) x y

Examples of type names, function names, and constructor names as mixfix operators:

  1. -- Example type name _⇒_
  2. _⇒_   : Bool → Bool → Bool
  3. true  ⇒ b = b
  4. false ⇒ _ = true
  6. -- Example function name _and_
  7. _and_ : Bool → Bool → Bool
  8. true and x = x
  9. false and _ = false
  11. -- Example function name if_then_else_
  12. if_then_else_ : {A : Set} → Bool → A → A → A
  13. if true then x else y = x
  14. if false then x else y = y
  16. -- Example constructor name _∷_
  17. data List (A : Set) : Set where
  18.   nil  : List A
  19.   _∷_ : A → List A → List A

Precedence

Consider the expression false and true ⇒ false. Depending on which of _and_ and _⇒_ has more precedence, it can either be read as (false and true) ⇒ false (which is true), or as false and (true ⇒ false) (which is false).

Each operator is associated to a precedence, which is a floating point number (can be negative and fractional!). The default precedence for an operator is 20.

Note

Please note that -> is directly handled in the parser. As a result, the precedence of -> is lower than any precedence you may declare with infixl and infixr.

If we give _and_ more precedence than _⇒_, then we will get the first result:

  1. infix 30 _and_
  2. -- infix 20 _⇒_ (default)
  4. p-and : {x y z : Bool} →  x and y ⇒ z  ≡  (x and y) ⇒ z
  5. p-and = refl
  7. e-and : false and true ⇒ false  ≡  true
  8. e-and = refl

But, if we declare a new operator _and’_ and give it less precedence than _⇒_, then we will get the second result:

  1. _and’_ : Bool → Bool → Bool
  2. _and’_ = _and_
  3. infix 15 _and’_
  4. -- infix 20 _⇒_ (default)
  6. p-⇒ : {x y z : Bool} →  x and’ y ⇒ z  ≡  x and’ (y ⇒ z)
  7. p-⇒ = refl
  9. e-⇒ : false and’ true ⇒ false  ≡  false
  10. e-⇒ = refl

Fixities can be changed when importing with a renaming directive:

  1. open M using (_∙_)
  2. open M renaming (_∙_ to infixl 10 _*_)

This code brings two instances of the operator _∙_ in scope:

  • the first named _∙_ and with its original fixity

  • the second named _*_ and with the fixity changed to act like a left associative operator of precedence 10.

Associativity

Consider the expression true ⇒ false ⇒ false. Depending on whether _⇒_ associates to the left or to the right, it can be read as (false ⇒ true) ⇒ false = false, or false ⇒ (true ⇒ false) = true, respectively.

If we declare an operator _⇒_ as infixr, it will associate to the right:

  1. infixr 20 _⇒_
  3. p-right : {x y z : Bool} →  x ⇒ y ⇒ z  ≡  x ⇒ (y ⇒ z)
  4. p-right = refl
  6. e-right : false ⇒ true ⇒ false  ≡  true
  7. e-right = refl

If we declare an operator _⇒’_ as infixl, it will associate to the left:

  1. infixl 20 _⇒’_
  3. _⇒’_ : Bool → Bool → Bool
  4. _⇒’_ = _⇒_
  6. p-left : {x y z : Bool} →  x ⇒’ y ⇒’ z  ≡  (x ⇒’ y) ⇒’ z
  7. p-left = refl
  9. e-left : false ⇒’ true ⇒’ false  ≡  false
  10. e-left = refl

Ambiguity and Scope

If you have not yet declared the fixity of an operator, Agda will complain if you try to use ambiguously:

  1. e-ambiguous : Bool
  2. e-ambiguous = true ⇒ true ⇒ true
  1. Could not parse the application true ⇒ true ⇒ true
  2. Operators used in the grammar:
  3.   ⇒ (infix operator, level 20)

Fixity declarations may appear anywhere in a module that other declarations may appear. They then apply to the entire scope in which they appear (i.e. before and after, but not outside).

Operators in telescopes

Agda does not yet support declaring the fixity of operators declared in telescopes, see Issue #1235 <https://github.com/agda/agda/issues/1235&gt;.

However, the following hack currently works:

  1. module _ {A : Set} (_+_ : A → A → A) (let infixl 5 _+_; _+_ = _+_) where