Extending the Quantitative Pattern-Matching Paradigm
<|reference_start|>Extending the Quantitative Pattern-Matching Paradigm: 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.<|reference_end|>
@article{alves2024extending,
    title={Extending the Quantitative Pattern-Matching Paradigm},
    author={Sandra Alves, Delia Kesner, and Miguel Ramos},
    journal={arXiv preprint arXiv:2408.11007},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.11007},
    primaryClass={cs.PL cs.LO}
}