Universes For Generic Programs
Room: BBL room 471
Speaker: Joeri van Eekelen
Title: Universes for Generic Programs
Generic programming, as used in the Functional Programming community, is writing programs and
functions that work on many datatypes. This is done by examining the structure of the datatype definition. In dependently typed languages, we can use 'universes' to represent the structure of the datatype definition. Generic functions are then defined on this universe. In this talk, I'll show different universes, and how universe choice influences which datatypes can be represented.