Skip to content

Chapter 4: Translating Miranda into the enriched lambda calculus

Pattern Match

  • overlapping patterns
  • constant patterns
  • nested patterns
  • multiple arguments
  • non-exhaustive sets of equations
  • conditional equations
  • repeated variables


p = v
  | constant
  | constructor p1 ... p2

A pattern-matching lambda abstraction: $\lambda p . E$, where $p$ is a pattern.

Failed matching

We introduce a built-in value FAIL, which is returned when a pattern-match fails.

The $\parallel$ is an infix function, which:

For multiple argument matching, we add a reduction rule for FAIL


TR and guards:


& A_1, G_1 \ =\, & A_2, G_2 \ ... \ =\, & A_n, G_n \ \end{split}$$


(\texttt{IF } TE[![G_1]!]\,TE[![A_1]!] \ (\texttt{IF } TE[![G_1]!]\,TE[![A_1]!] \ ... \ (\texttt{IF } TE[![G_n]!]\,TE[![A_n]!]\texttt{ FAIL})...))



The ordinary product $A \times B = {(a, b) \,|\, a \in A, b \in B}$, which has bottom element $(\perp, \perp)$

The lifted product, $(A \times B)_\perp = (A \times B) \cup { \perp }$, which has bottom element $\perp \,\neq (\perp, \perp)$

The insight is that lazy product-matching corresponds to ordinary product, while strict product-matching corresponds to lifted product. To implement the ordinary product domain $(A \times B)$, we have to make $(\perp, \perp)$ indistinguishable from non-termination.


Case-expressions is a construct describing a simple form of pattern-matching which is more efficient.

Two points: simple (not nested), exhaustive (cover all constructors).