Skip to content

Research at St Andrews

A dependently typed calculus with pattern matching and erasure inference

Research output: Contribution to journalArticlepeer-review

DOI

Open Access permissions

Open

Author(s)

Matúš Tejiščák

School/Research organisations

Abstract

Some parts of dependently typed programs constitute evidence of their type-correctness and, once checked, are unnecessary for execution. These parts can easily become asymptotically larger than the remaining runtime-useful computation, which can cause normally linear-time programs run in exponential time, or worse. We should not make programs run slower by just describing them more precisely.

Current dependently typed systems do not erase such computation satisfactorily. By modelling erasure indirectly through type universes or irrelevance, they impose the limitations of these means to erasure. Some useless computation then cannot be erased and idiomatic programs remain asymptotically sub-optimal.

In this paper, we explain why we need erasure, that it is different from other concepts like irrelevance, and propose a dependently typed calculus with pattern matching with erasure annotations to model it. We show that erasure in well-typed programs is sound in that it commutes with reduction. Assuming the Church-Rosser property, erasure furthermore preserves convertibility in general.
We also give an erasure inference algorithm for erasure-unannotated or partially annotated programs and prove it sound, complete, and optimal with respect to the typing rules of the calculus.
Finally, we show that this erasure method is effective in that it can not only recover the expected asymptotic complexity in compiled programs at run time, but it can also shorten compilation times.
Close

Details

Original languageEnglish
Article number91
Pages (from-to)1-29
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume4
DOIs
Publication statusPublished - 2 Aug 2020

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

ID: 271054137

Top