A family of universes for generic programming

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/146810
Download file(s):
File Description SizeFormat 
146810.pdfFulltext715.22 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: A family of universes for generic programming
Authors: Andjelkovic, Stevan
Abstract: Datatype-generic programming in the dependently typed setting can be achieved using the universe construction. The set of codes of the universe has an impact on the datatypes it can express and also on the set of supported datatype-generic functions. For example a universe with a code for functions can express datatypes such as the Brouwer ordinals: data Ord : Set where zero : Ord suc : Ord ! Ord limit : (N ! Ord) ! Ord -- The function code is needed to -- describe limit. It cannot support a meaningful datatype-generic decidable equality however, because generally equality of functions is undecidable. This problem often leads to the adaptation of several universes, for example one without a code for functions for which we can have decidable equality and another with a code for functions for which we can express datatypes such as the Brouwer ordinals. Both universes might support, for example, a datatypegeneric mapping and iteration function however, this leads to code duplication-defeating one of the very aims of datatype-generic programming. This work proposes a way around this problem by presenting a family of universes(or an indexed universe), where the index explains what class of datatypes that is supported. Datatype-generic functions which work over multiple classes of datatypes, such as mapping and iterating, are implemented using a polymorphic index. The entire development is carried out in Agda. It is at least partially compatible with levitation and ornamentation, which are recently proposed techniques for avoiding code duplication, both based on the universe construction.
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/146810
Collection:Examensarbeten för masterexamen // Master Theses



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