# Fun with Functional Dependencies

or (Draft) Types as Values in Static Computations in
Haskell

In the Proceedings of the Joint CS/CE Winter
Meeting, Varberg, Sweden, January 2001.
### Abstract

This
paper illustrates how Haskell's type class system can
be used to express computations. Since computations on the type
level are performed by the type checker, these computations are
static (i.e., performed at compile-time), and, since the type system
is decidable, they always terminate. Haskell thus provides a means
to express static computations, and has a clear distinction between
static and dynamic computations.

Instance declarations define predicates over types, or in the case
of multi-parameter classes, relations between types. With functional
dependencies, multi-parameter classes directly specify functions,
and thanks to them you can get the type checker to compute the
values of function applications, rather than just checking that the
result of an application is what you say it is.

This way of expressing computation gives us the power of a small,
first-order functional programming language, with pattern matching
and structural recursion. We can easily define things like booleans,
natural numbers, lists, and functions over these types. We give some
examples of completely static computations, the most elaborate one being
an implementation of insertion sort. We also give examples where
static and dynamic computations are mixed.

### Full paper

- Available as PDF. (140KB)
- Available as HTML. (24KB)
- Links: Citations (Google Scholar)

Thomas Hallgren
Last modified: Thu Dec 29 18:50:43 CET 2022