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
Patterns
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})...))
$$
Strictness
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
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).