A totaly Epic backend for Agda

Abstract

Agda is a programming language that utilises dependent types which add the power to express properties about terms very precisely, but this also introduces a runtime performance overhead. This thesis presents a new compiler backend for Agda targeting Epic with the aim to use the types for optimising programs and for removing the overhead. One source of inefficiencies is in the data representation. Two ways to remove these inefficiencies are presented: Forcing, which deletes fields in constructors that may be inferred, and representing datatypes as primitive data, which is done by using machine integers for types on a certain form. Many terms in dependently typed languages have no computational content(observable at runtime). Three optimisations for getting rid of such terms are presented: Erasure, which erases types and unused arguments to functions, smashing, which replaces inefficient computations with a result that is the only observable one, and injection detection, which detects inefficient identity functions so that they can be replaced by faster versions. The results of doing the optimisations are benchmarked, and in some examples the runtime of an optimised program compared to an unoptimised one is almost one third and the produced executable size is halved. The code that is produced is also closer to efficient code written without using sexy types, and it does not take as long to compile it. This work makes it more feasible to write programs usable in the “real world” using Agda, and shows that it is perfectly possible to use dependently typed languages for programming.