[Haskell-cafe] The meaning of categories constructed from HASK
Olaf Klinke
olf at aatal-apotheke.de
Sat Sep 24 22:15:33 UTC 2016
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
More information about the Haskell-Cafe
mailing list