Implementing and Optimizing a Simple, Dependently-Typed Language

Abstract

This thesis presents a compiler for the simple functional programming language LambdaPi, which includes dependent types. The compiler is written in Haskell and uses LLVM, a framework for building optimizing compiler backends. It can compile the complete standard library provided by LambdaPi’s authors into native machine code. It is not much of an optimizing compiler, but several obvious opportunities for improvement exist. First I discuss the theoretical background of project: the principles of dependent types and the languages which include them. I also give a brief overview of the LLVM system and of related work. The second section describes the process of implementation, which was done in stages from a trivial calculator language up to full LambdaPi. And finally we consider opportunities for optimization. Some of these stem from Edwin Brady’s [2005] analysis of Epigram, while others are lower-level and can be performed for us by LLVM.