Pattern Synonyms

A pattern synonym is a declaration that can be used on the left hand side (when pattern matching) as well as the right hand side (in expressions). For example:

data Nat : Set where
  zero : Nat
  suc  : Nat  Nat

pattern z    = zero
pattern ss x = suc (suc x)

f : Nat  Nat
f z       = z
f (suc z) = ss z
f (ss n)  = n

Pattern synonyms are implemented by substitution on the abstract syntax, so definitions are scope-checked but not type-checked. They are particularly useful for universe constructions.


Pattern synonyms can be overloaded as long as all candidates have the same shape. Two pattern synonym definitions have the same shape if they are equal up to variable and constructor names. Shapes are checked at resolution time and after expansion of nested pattern synonyms.

For example:

data List (A : Set) : Set where
  lnil  : List A
  lcons : A  List A  List A

data Vec (A : Set) : Nat  Set where
  vnil  : Vec A zero
  vcons :  {n}  A  Vec A n  Vec A (suc n)

pattern [] = lnil
pattern [] = vnil

pattern _∷_ x xs = lcons x xs
pattern _∷_ y ys = vcons y ys

lmap :  {A B}  (A  B)  List A  List B
lmap f []       = []
lmap f (x ∷ xs) = f x ∷ lmap f xs

vmap :  {A B n}  (A  B)  Vec A n  Vec B n
vmap f []       = []
vmap f (x ∷ xs) = f x ∷ vmap f xs

Flipping the arguments in the synonym for vcons, changing it to pattern _∷_ ys y = vcons y ys, results in the following error when trying to use the synonym:

Cannot resolve overloaded pattern synonym _∷_, since candidates
have different shapes:
  pattern _∷_ x xs = lcons x xs
    at pattern-synonyms.lagda.rst:51,13-16
  pattern _∷_ ys y = vcons y ys
    at pattern-synonyms.lagda.rst:52,13-16
(hint: overloaded pattern synonyms must be equal up to variable and
constructor names)
when checking that the clause lmap f (x ∷ xs) = f x ∷ lmap f xs has
type {A B : Set} → (A → B) → List A → List B


For each pattern pattern lhs = rhs, Agda declares a DISPLAY pragma refolding rhs to lhs (see The DISPLAY pragma for more details).