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

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

Hi Olaf, Thank you very much for the thorough reply! If I understood your answer: - it seem these two derived categories are not easy to express in haskell because the objects of the constructed categories are arrows in HASK. - And although specific instances of such constructions (such as the Eilenberg-Moore category you point out) are useful, this is not so clear for the general case. I hope I got that right. Cheers, Dimitri On 24/09/16 4:15 PM, Olaf Klinke wrote:
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
-- 2E45 D376 A744 C671 5100 A261 210B 8461 0FB0 CA1F
participants (2)
-
Dimitri DeFigueiredo
-
Olaf Klinke