Monday, September 17, 2012

A kind for regions

With a new powerful kind system in GHC, there are many lurking opportunities for expressive programming. Here's one.

What is the kind of the ST type constructor? Currently, it's ST :: * -> * -> *.

It should not be. In ST s a, the parameter s is special. It is not meant to be a "real" type like Int. It is used only to control the scope of references. One day I'd like to see a separate kind for s.

kind Region
ST :: Region -> * -> *
STRef :: Region -> * -> *
runST :: (forall (s :: Region). ST s a) -> a

This way it's clear that in ST s a the types s and a are of different nature. Attempting to write ST s s is a kind error.