Abstract

Type systems have become more sophisticated in recent years. For example, Haskell extends Hindley-Milner type checking with type classes in order to handle ad-hoc polymorphism. In this talk, we consider another extension: dependent types - this extension allows types to depend on values. We take a look at programs which cannot easily be written in Haskell because of type limitations and present solutions using the new functional language Cayenne (proposed by Lennart Augustsson) which provides type checking for dependent types. The main case studies are: a core implementation of extensible records, and an attempt to define a parametrized form of zipWith; the latter will highlight some problems with programming in Cayenne.