Operators.agda

-- This module introduces operators.

module Introduction.Operators where

-- Agda has a very flexible mechanism for defining operators, supporting infix,
-- prefix, postfix and mixfix operators.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- Any name containing underscores (_) can be used as an operator by writing
-- the arguments where the underscores are. For instance, the function _+_ is
-- the infix addition function. This function can be used either as a normal
-- function: '_+_ zero zero', or as an operator: 'zero + zero'.

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- A fixity declaration specifies precedence level (50 in this case) and
-- associativity (left associative here) of an operator. Only infix operators
-- (whose names start and end with _) have associativity.
infixl 50 _+_

-- The only restriction on where _ can appear in a name is that there cannot be
-- two underscores in sequence. For instance, we can define an if-then-else
-- operator:

data Bool : Set where
  false : Bool
  true  : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

-- if_then_else_ is treated as a prefix operator (ends, but doesn't begin with
-- an _), so the declared precedence determines how something in an else branch
-- should be parsed. For instance, with the given precedences
--   if x then y else a + b
-- is parsed as
--   if x then y else (a + b)
-- and not
--   (if x then y else a) + b

infix 10 if_then_else_

-- In Agda there is no restriction on what characters are allowed to appear in
-- an operator (as opposed to a function symbol). For instance, it is allowed
-- (but not recommended) to define 'f' to be an infix operator and '+' to be a
-- function symbol.

module BadIdea where

  _f_ : Nat -> Nat -> Nat
  zero  f zero  = zero
  zero  f suc n = suc n
  suc n f zero  = suc n
  suc n f suc m = suc (n f m)

  + : Nat -> Nat
  + n = suc n