Fun with Type Functions

Third Haskell lecture of #laser12 Simon will introduce Type Functions (Lecture 1 and Lecture 2)

As soon as we have classes in Haskell, we would like to state that the result of a function has the same value as its arguments, something like this:

GNum a b
type SymTy a b :: *
(=) :: a -> a -> SumTy a b

The * here is a associated type of class GNum (inspiration taken from C++). Each method gets a type signature, each associated type gets a kind signature. Now we need “witnesses” for SunTy, matching the kind signature:

instance GNum Int Int where
type SumTy Int Int = Int
(+) x y = plusInt x y

instance GNum Int Float where
type SumTy Int Float = Float
(+) x y = plusFloat (intToFloat x) y

There could be more declarations, for instance a division might have a different kind signature: Int Int Float.

The SumTy we have defined now is a type-level function. The type checker simply rewrites SumTy Int Int –> Int whenever it can.

The result of this is that we can omit instances for incompatible types. Support we introduce Dollars, we can use type SumTy Dollar Dollar = Dollar and not specify a rule to add Dollar to Ints (since you wouldn’t want that) and it will not work. Nice!

It also results in optimization of data structures. Consider a finite map from keys to values and we want to data representation of the map to depend on the type of the key. With the type function, we can now do this, We can even create a dictionary with a pair of keys as key!

Martin Odersky does point out that this is sort of easy to do in OO, by using a factory class and subtyping.

Data parallel Haskell

If you have an array in Haskell, this is implemented as an array of pointers, which is not optimal for parallel programming. Suppose we have an array of pairs, we would prefer an pair of arrays. An with an array of arrays, we definitely won’t prefer pointers to arrays, since that is terrible for load-balancing. One option is the flattening transformation, but this requires a lot of tricky bookkeeping. This can now been defined as a pair of the arrays and the ‘bookkeeping array’.

Summary

Type families let you do type-level computations and they fit nicely with Type Classes.

Want to know more?

Have a look at the corresponding paper Fun with type functions, that Simon wrote with with Ken Shan, and Oleg Kiselyov. It is a tutorial on indexed type families, and associated types in Haskell.  Images in this blogs are taken form the presentation accompanying this paper. Or, watch the Channel 9 video about this paper.