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. The authors present a typed functional calculus that emphasizes the strong connection between the structure of whole pattern definitions and their types. In t...

Full description

Saved in:
Bibliographic Details
Main Authors: Breazu-Tannen, V., Kesner, D., Puel, L.
Format: Conference Proceeding
Language:English
Subjects:
Calculus
Functional programming
Information science
Joining processes
Logic design
Pattern matching
Redundancy
Runtime
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. The authors 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 nonexhaustive 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. The calculus is designed as a computational interpretation of the Gentzen sequent proofs for the intuitionistic propositional logic. The basic properties connecting typing and evaluation, subject reduction, and strong normalization are proved. The authors believe that this calculus offers a rational reconstruction of the pattern-matching features found in successful functional languages.< >
DOI:10.1109/LICS.1993.287581