Exploring universe polymorphism in Omega

Abstract

Ωmega extends Haskell with novel features for practical functional programming: GADT's, extensible kinds, and type functions. With both extensible types and extensible kinds in place, there is a tendency for redundant datatype definitions; likewise for functions that operate over these structures. Universe polymorphism is a way to abstract over levels in the typing hierarchy, unifying these redundant constructs. In this paper, we use Ωmega's novel features to encode simplified models of Ωmega as an object language, and then use these models to begin exploring the design space for universe polymorphism in Ωmega.