Wolfram Kahl, Jacques Carette, Xiaoheng Ji
in Tarmo Uustalu (ed.),
Mathematics of Program Construction, MPC 2006, Springer-Verlag, LNCS 4014,
pages 253--273
(BibTeX)
The pattern matching calculi introduced by the first author are a refinement of the λ-calculus that integrates mechanisms appropriate for fine-grained modelling of non-strict pattern matching.
While related work in the literature
only uses a single monad, typically Maybe,
for matchings,
we present an axiomatic approach
to semantics of these pattern matching calculi using two monads,
one for expressions and one for matchings.
Although these two monads only need to be relatively lightly coupled, this semantics implies soundness of all core PMC rules, and is a useful tool for exploration of the design space for pattern matching calculi.
Using lifting and Maybe monads,
we obtain standard Haskell semantics,
and by adding another level of Maybe to both,
we obtain a denotational semantics
of the ``matching failure as exceptions'' approach
of Erwig and Peyton Jones.
Using list-like monads opens up
interesting extensions in the direction of functional-logic programming.
A long version of this paper, containing all the proofs, is available as SQRL report Nr. 33