A totaly Epic backend for Agda

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/146807
Download file(s):
File Description SizeFormat 
146807.pdfFulltext2.41 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: A totaly Epic backend for Agda
Authors: Fredriksson, Olle
Gustafsson, Daniel
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.
Keywords: Informations- och kommunikationsteknik;Datavetenskap (datalogi);Information & Communication Technology;Computer Science
Issue Date: 2011
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/146807
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.