A family of universes for generic programming

Visa enkel post
dc.contributor.authorAndjelkovic, Stevan
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T12:40:01Z
dc.date.available2019-07-03T12:40:01Z
dc.date.issued2011
dc.description.abstractDatatype-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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/146810
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectInformations- och kommunikationsteknik
dc.subjectDatavetenskap (datalogi)
dc.subjectInformation & Communication Technology
dc.subjectComputer Science
dc.titleA family of universes for generic programming
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
146810.pdf
Storlek:
715.22 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen