### Skapa referens, olika format (klipp och klistra)

**Harvard**

Andjelkovic, S. (2011) *A family of universes for generic programming*. Göteborg : Chalmers University of Technology

** BibTeX **

@mastersthesis{

Andjelkovic2011,

author={Andjelkovic, Stevan},

title={A family of universes for generic programming},

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.<br>
For example a universe with a code for functions can express datatypes such
as the Brouwer ordinals:<br><br>
data Ord : Set where<br>
zero : Ord<br>
suc : Ord ! Ord<br>
limit : (N ! Ord) ! Ord -- The function code is needed to
-- describe limit.<br><br>
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.<br>
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.<br>
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.},

publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},

place={Göteborg},

year={2011},

note={87},

}

** RefWorks **

RT Generic

SR Electronic

ID 146810

A1 Andjelkovic, Stevan

T1 A family of universes for generic programming

YR 2011

AB 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.<br>
For example a universe with a code for functions can express datatypes such
as the Brouwer ordinals:<br><br>
data Ord : Set where<br>
zero : Ord<br>
suc : Ord ! Ord<br>
limit : (N ! Ord) ! Ord -- The function code is needed to
-- describe limit.<br><br>
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.<br>
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.<br>
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.

PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/146810.pdf

OL 30