[Haskell-cafe] The meaning of categories constructed from HASK

[Olaf Klinke]

Dear Dimitri,

I've never seen arrow or slice categories in a paper on functional programming.
Commutative squares are most frequently used in the definition of typeclasses, where the documentation usually reads: 
    Instances should satisfy: f.g = h.i
where f,g,h,i are some functions involved in the definition of the typeclass. Haskell can not stop you writing an instance violating the commutative square, however. 

Certain special arrow categories are useful, even in Haskell. For example the Eilenberg-Moore category of a monad m. Objects are arrows m a -> a and morphisms are commutative squares

     liftM f
m a ---------> m b
 |              |
 |              |
 v              v
 a ---------->  b
       f

Such an f is sometimes called "linear". For example, every instance of Data.Monoid comes with an arrow mconcat :: (Monoid a) => [a] -> a and commutative squares between two monoids are precisely the functions f where 
f mempty = mempty
and
f (x `mappend` y) = (f x) `mappend` (f y)

I'm sure you have looked at Control.Category in package base before asking this question. The Category typeclass defined there is not capable of expressing either of your examples, because: 

- The hom-set of a Category must be a HASK type (although not necessarily a function type)
- Each hom-set must be parametrised by two HASK types

The arrow category is not expressible, because we can not forge a HASK type that somehow specifies exacltly one function. Moreover, the cummutativity of a square is not expressible, that is, there is no HASK type consisting of all functions making a certain square commute.

The slice category is not expressible, for the same reason as above.

There are, however, interesting instances of Control.Category where the hom-set elements are not functions. For example, one could have memoized functions between stream types. The following goes back to Dirk Pattinson and Ulrich Berger, AFAIK. Suppose i is a type of tokens such that an infinite stream of i's encodes an element of type x. Likewise, let o be a type of tokens such that an infinite stream of o's encodes an element of type y. Now consider the type Mem below.

-- Run the following in ghci -XNoImplicitPrelude
import Control.Category
import Data.List (head,tail)

-- A memoized function [i] -> [o], representing a function x -> y.
-- Either requesting an input token or yielding an output token.
data Mem i o = Read (i -> Mem i o) | Write o (Mem i o)

instance Category Mem where
   id = Read (\i -> Write i id)
   f . g = case f of
     Write p f' -> Write p (f' . g)
     Read r -> case g of
       Write o g' -> (r o) . g'
       Read r' -> Read (\i -> f . (r' i))

-- run a memoized function. 
-- This is a functor from Mem to HASK.
runMem :: Mem i o -> [i] -> [o]
runMem f input = case f of 
  Write o f' -> o : runMem f' input
  Read r -> runMem (r (head input)) (tail input)

If there are only finitely many possible input tokens i, then one can replace Read (i -> Mem i o) by Read (Map i (Mem i o)) in which case the entire memoized function really is a tree.

Olaf