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
Associativity¶
Consider the expression true ⇒ false ⇒ false
. Depending on whether _⇒_
is
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).