Thursday, November 8, 2007

Trendy Topics

There seem to be two important trends in the Haskell universe and I must admit, that I do not want to stay away from them either...
  • The first one is the exploration of category-theoretic concepts and their showing-off in the blogosphere. Generalizations of monads or the category type class are just two recent picks from the bottomless supply of ideas.
  • The second trend is more subtle and one has to dive into the recent ICFP papers to perceive it. I have already mentioned the Unimo framework, which guarantees the monad laws and allows to represent the monadic computation as a pure data structure which is then run by recursive analysis. Wouter Swierstra et al. introduced another concept to capture monads (also strongly resembling the free monad) and they have improved testing ability on their minds when doing this. The third paper that comes to my mind is about speeding up arrow computations by analysis and optimization of a data structure closely resembling arrows.
So I am not in bad company announcing that I am preparing a paper about thrists which are the moral equivalents of free categories. The rest of this article gives an appetizer about thrists.
data Thrist :: (* -> * -> *) -> * -> * -> * where
Nil :: Thrist p a a
Cons :: p a b -> Thrist p b c -> Thrist p a c
The definition makes it clear that Thrist is a GADT (I use the Haskell way of defining a GADT here, the paper will use the slightly different Ωmega syntax) and it is a curious mixture of listness and threadedness (this is the reason for its name). The types of the thrist elements must match up in a certain way, resembling function composition.
Indeed, instead of composing functions, we can put them into a thrist:
Cons ord $ Cons chr Nil
gives us an arrow thrist (Thrist (->) Char Char) only showing the start and end types, with the internal types abstracted away existentially.
Of course we have to supply an interpreter for this data structure to get the functionality (the semantics) of function composition, but this easy exercise is left to you.

But... What do thrists buy us?
Two very important things:
  • Unlike function composition, we can take the thrist apart, analyse and transform it, and
  • a vast field opens up with the first (p) parameter to the Thrist. It can be the pair constructor (,) or the LE (less-or-equal) proposition, there are many sensible instantiations -- especially with two-parameter user-defined GADTs.
Finally, the category-theoretic twist: think of the parameter p as the morphisms of a category C (with C's objects being the morphisms' domains and ranges) then Thrist p is essentially the free category of C, often written as C*.

I hope you enjoyed reading this in the same way as me writing it!