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:

  1. data Nat : Set where
  2.   zero : Nat
  3.   suc  : Nat → Nat
  5. pattern z    = zero
  6. pattern ss x = suc (suc x)
  8. f : Nat → Nat
  9. f z       = z
  10. f (suc z) = ss z
  11. 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.

Overloading

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:

  1. data List (A : Set) : Set where
  2.   lnil  : List A
  3.   lcons : A → List A → List A
  5. data Vec (A : Set) : Nat → Set where
  6.   vnil  : Vec A zero
  7.   vcons : ∀ {n} → A → Vec A n → Vec A (suc n)
  9. pattern [] = lnil
  10. pattern [] = vnil
  12. pattern _∷_ x xs = lcons x xs
  13. pattern _∷_ y ys = vcons y ys
  15. lmap : ∀ {A B} → (A → B) → List A → List B
  16. lmap f []       = []
  17. lmap f (x ∷ xs) = f x ∷ lmap f xs
  19. vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
  20. vmap f []       = []
  21. 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:

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

Refolding

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