Extending the Quantitative Pattern-Matching Paradigm

TL;DR

This paper extends type systems based on non-idempotent intersection types to characterize termination and evaluate the complexity of functional languages with pattern matching, including effectful features, using a unified lambda calculus framework.

Contribution

It introduces a novel type system for pattern-matching functional languages that precisely characterizes termination and quantifies evaluation steps.

Findings

Type system characterizes termination of pattern-matching languages.

Type derivation size bounds evaluation steps.

Framework encodes various lambda calculus variants and effectful languages.

Abstract

We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) $\lambda$-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN $\lambda$-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form.