Summary of my talk at the workshop on
The concept of a universe was introduced by Per Martin-Löf to model reflection in Intuitionistic Type Theory. It roughly corresponds to inaccessible cardinals in conventional set theory.
In programming we are interested in much smaller universes, modelling a collection of datatypes over which we want to use in generic programming. Sich a universe is given by a type of codes for types, Data : * and a family of values, indexed by data, Val : Data -> *.
The smallest universe, dubbed the microscopic universe by Helmut Schwichtenberg, has just two types, e.g. Data=Bool and only Val True is inhabited. The names So and oh were suggested by Conor. It is hardly useful in programming but plays an important role in Type Theory, by providing a means to prove inequalities like true /= false. Categorically it corresponds to disjoint or extensive coproducts.
More relevant for programming is the universe of finite types, based on the family Fin : Nat -> *, which is frequently used in dependently typed programming, even without thinking of it as a universe. The epigram code above contains implementations of coproductes (+), products (x) and exponentials (->) by generic programming. The universe of finite types is useful for implementing systems with a fixed, finite size, e.g. hardware.
Better known in generic programming is the universe of regular types, which contains codes for the types generated by 0,+,1,x,mu. There are a number of well known programs which are generic for that universe, e.g. generic equality and generic mapp. Another example, which I wasn't able to finish due to problems with epigram are derivatives which can be used to implement the zipper. Peter Morris has implemented a version of equality whose correctness can be seen in its type (eq a b : a=b + (a=b) -> Zero).
We can go for bigger universes, e.g. we may add coinductive types (nu) to obtain the universe of Buechi types, or add constant exponentation (C ->) to obtain all strictly positive types. Other modifications are to allow higher kinds (we have done this already in our paper on generic programming within dependently typed programming, note that this is pre-epigramm). Certainly, we would like to include dependent types in our universe, but this seems to require mutual dependent families not yet implemented in Epigram.
While dependently typed programming provides the perfect environment for generic programming, we also need generic programming to be able to provide reusable library code when the more precise type system leads to a proliferation of types, eg. lists, vectors, proofs of transitive closure,...