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

[Dimitri DeFigueiredo]

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