February 16, 2005

Paper Review: Associated Types with Class

I'm starting a new tradition with this entry, that of the paper review. There are two problems I face with my research reading: one, I don't do enough of it and two, I forget a lot of what I read within six months. Writing is two things to me: a way of organising ideas and a memory crutch. The aim is that by reviewing each paper I read I attack this second problem head on. If successful it may even encourage me to read more; I'll have more in my head to think about and that may just stimulate my curiosity.

Associated Types with Class. Manuel M.T. Chakravarty, Gabriele Keller, Simon Peyton Jones and Simon Marlow. In Proceedings of The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), pages 1-13, ACM Press, 2005.


POPL'05.

Synopsis

This paper presents a light-weight extension to Haskell that allows ad hoc overloading of types in much the same way that values can be overloaded in Haskell already. This similarity is highlighted syntactically by extending Haskell's type classes to allow local data type declarations. Here is an example:


class ArrayElem e where
data Array e
index :: Array e -> Int -> e

instance ArrayElem Int where
data Array Int = IntArray UIntArray
index (IntArray ar) i = indexUIntArray ar i

The most interesting thing to me was what sort of applications this idea has.


  • It can be used in self-optimising libraries. That is, although the interface to a library remains general the data representation can be made to vary depending on the types of data used. For instance, for a list we can store the elements of that list differently depending on whether they are integers or something more complicated.

  • Abstract interfaces. Disparate interfaces to libraries that have essentially the same functionality but work with different data types can now be unified under one common interface. For instance the function lookup works on association lists while lookupFM works on finite maps. Both provide equivalent functionality. Using associated types we can define a single interfaces and write instances for each data type. In a sense this just the flip-side of the self-optimising libraries. Before we asked, "how can we provide different implementations for a generic interface depending on the type of the data?" but with Abstract Interfaces we're asking, "how can we provide a generic interface for different implementations of a library?"

Much of the paper is then devoted to showing that type checking can be done on the associated types extension. They also show that an evidence translation to System F is possible without extending it.


Difficulties

  • I don't know enough about dictionaries. Implementing associated types are a straightforward extension of the dictionary passing implementation of type classes. I get the basic idea but some things are still unclear to me.

  • The type system is "all greek to me". I still don't know enough about formal type theory and associated proofs to be able to wade through this section. It felt like I was wallowing the moment I started.

Verdict

The significance of this paper is its light-weight nature. The problem of type indexed types has been tackled before many times but never with such syntactic elegance nor implementation simplicity.