Erasure in dependently typed programming

Abstract

It is important to reduce the cost of correctness in programming. Dependent types
and related techniques, such as type-driven programming, offer ways to do so.

Some parts of dependently typed programs constitute evidence of their typecorrectness
and, once checked, are unnecessary for execution. These parts can easily
become asymptotically larger than the remaining runtime-useful computation, which
can cause linear-time algorithms run in exponential time, or worse. It would be
unnacceptable, and contradict our goal of reducing the cost of correctness, to make
programs run slower by only describing them more precisely.

Current systems cannot 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.

This dissertation explains why we need erasure, that it is different from other
concepts like irrelevance, and proposes two ways of erasing non-computational data.
One is an untyped flow-based useless variable elimination, adapted for dependently
typed languages, currently implemented in the Idris 1 compiler.

The other is the main contribution of the dissertation: a dependently typed core
calculus with erasure annotations, full dependent pattern matching, and an algorithm
that infers erasure annotations from unannotated (or partially annotated) programs.
I show that erasure in well-typed programs is sound in that it commutes with
single-step reduction. Assuming the Church-Rosser property of reduction, I show
that properties such as Subject Reduction hold, which extends the soundness result
to multi-step reduction. I also show that the presented erasure inference is sound
and complete with respect to the typing rules; that this approach can be extended
with various forms of erasure polymorphism; that it works well with monadic I/O
and foreign functions; and that it is effective in that it not only removes the runtime
overhead caused by dependent typing in the presented examples, but can also shorten
compilation times.

Date of Award	29 Jul 2020
Original language	English
Awarding Institution	University of St Andrews
Supervisor	Edwin Charles Brady (Supervisor)