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:
-- Example type name _⇒_
_⇒_ : Bool → Bool → Bool
true ⇒ b = b
false ⇒ _ = true
-- Example function name _and_
_and_ : Bool → Bool → Bool
true and x = x
false and _ = false
-- Example function name if_then_else_
if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y
-- Example constructor name _∷_
data List (A : Set) : Set where
nil : List A
_∷_ : A → List A → List A
Precedence¶
Consider the expression true and false ⇒ false
.
Depending on which of _and_
and _⇒_
has more precedence,
it can either be read as (false and true) ⇒ false = true
,
or as false and (true ⇒ false) = true
.
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:
infix 30 _and_
-- infix 20 _⇒_ (default)
p-and : {x y z : Bool} → x and y ⇒ z ≡ (x and y) ⇒ z
p-and = refl
e-and : false and true ⇒ false ≡ true
e-and = refl
But, if we declare a new operator _and’_
and give it less precedence than
_⇒_
, then we will get the second result:
_and’_ : Bool → Bool → Bool
_and’_ = _and_
infix 15 _and’_
-- infix 20 _⇒_ (default)
p-⇒ : {x y z : Bool} → x and’ y ⇒ z ≡ x and’ (y ⇒ z)
p-⇒ = refl
e-⇒ : false and’ true ⇒ false ≡ false
e-⇒ = refl
Fixities can be changed when importing with a renaming
directive:
open M using (_∙_)
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:
infixr 20 _⇒_
p-right : {x y z : Bool} → x ⇒ y ⇒ z ≡ x ⇒ (y ⇒ z)
p-right = refl
e-right : false ⇒ true ⇒ false ≡ true
e-right = refl
If we declare an operator _⇒’_
as infixl
, it will associate to the left:
infixl 20 _⇒’_
_⇒’_ : Bool → Bool → Bool
_⇒’_ = _⇒_
p-left : {x y z : Bool} → x ⇒’ y ⇒’ z ≡ (x ⇒’ y) ⇒’ z
p-left = refl
e-left : false ⇒’ true ⇒’ false ≡ false
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:
e-ambiguous : Bool
e-ambiguous = true ⇒ true ⇒ true
Could not parse the application true ⇒ true ⇒ true
Operators used in the grammar:
⇒ (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>.
However, the following hack currently works:
module _ {A : Set} (_+_ : A → A → A) (let infixl 5 _+_; _+_ = _+_) where