Personal tools
You are here: Home Events Abstract Archives 2000 Programming with dependent types

Programming with dependent types

Yorck Hünke Oxford University Computing Laboratory 4pm Tuesday 4 April 2000 Room 2511, JCMB, King's Buildings

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.

Document Actions