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!


Unknown said...

the Thrist type is declared of kind (* -> * -> *) -> * -> *, which takes two types, but you've passed three types to it in the given types for Nil and Cons. I think Thrist is supposed to have kind (* -> * -> *) -> * -> * -> *.

heisenbug said...

nick, thanks for the clarification, I shall correct this. The error came from *not* wanting to copy&paste the more general definition I have in Ωmega:

data Thrist :: forall (l :: *1) . (l ~> l ~> *) ~> l ~> l ~> * where
Nil :: Thrist k a a
Cons :: k a b -> Thrist k b c -> Thrist k a c
deriving List(l)

In the Haskellifying process one star got dropped :-(

Twan van Laarhoven said...

I just noticed that your Thrist type is the same as the FL (forward list) type used by darcs. There the two extra parameters are only used as phantom types, but the definition is otherwise exactly the same. The also define a RL type for reverse lists,

data RL a x z where
(:<:) :: a y z -> RL a x y -> RL a x z
NilRL :: RL a x x

With a reverse function of the type

reverseFL :: FL a x z -> RL a x z

See Darcs.Patch.Ordered for the implementation.

heisenbug said...

@twan: this is funny, I watched Heffalump's Darcs video the other day, and wanted to ask them if they had a use for thrists! Looks like they are already using them..

In my paper I also mention the reverse thrists (corresponding to RL). Unfortunately the paper is under construction 8 months now, and progressing really slowly.

Thanks for the link, I will mention Darcs in the paper.