A Typed Pattern Calculus

The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. We present a typed functional calculus that emphasizes the strong connection between the structure of whole pattern definitions and their types. In this calculus type-checking guarantees the absence of runtime errors caused by non-exhaustive pattern-matching definitions. Its operational semantics is deterministic in a natural way, without the imposition of ad-hoc solutions such as clause order or "best fit". In the spirit of the Curry-Howard isomorphism, we design the calculus as a computational interpretation of the Gentzen sequent proofs for the intuitionistic propositional logic. We prove the basic properties connecting typing and evaluation: subject reduction and strong normalization. We believe that this calculus offers a rational reconstruction of the pattern-matching features found in successful functional languages. CNRS and Laboratoire..