[Haskell-cafe] A quick question about distribution of finite maps.

[Olaf Klinke]

> Hello!
> 
> Finite maps from `"containers" Data.Map` look like they may form a
> Cartesian closed category. So it makes sense to ask if the rule _α ⇸
> (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds in such
> categories does hold for finite maps. Note that, a map being a
> functor, this also may be seen as _f (g α) ≡ g (f α)_, which would
> work if maps were `Distributive` [1].
> 
> It looks to me as though the following definition might work:
> 
>     distribute = unionsWith union . mapWithKey (fmap . singleton)
> 
> — And it works on simple examples. _(I checked the law `distribute ∘
> distribute ≡ id` — it appears to be the only law required.)_
> 
> Is this definition correct? Is it already known and defined
> elsewhere?
> 
> [1]: 
> https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distributive.html#t:Distributive

Hi Ignat, 

TL;DR: No and no.

The documentation says that every distributive functor is of the form
(->) x for some x, and (Map a) is not like this. 

If Maps were a category, what is the identity morphism?

Let's put the Ord constraint on the keys aside, Tom Smeding has already
commented on that. Next, a Map is always finite, hence let's pretend
that we are working inside the category of finite types and functions.
Then the problems of missing identity and missing Ord go away. Once
that all types are finite, we can assume an enumerator. That is, each
type x has an operation
enumerate :: [x]
which we will use to construct the inverse of 
flip Map.lookup :: Map a b -> a -> Maybe b
thereby showing that a Map is nothing but a memoized version of a
Kleisli map (a -> Maybe b). Convince yourself that Map concatenation
has the same semantics as Kleisli composition (<=<). Given a Kleisli
map k between finite types, we build a Map as follows.
\k -> Map.fromList (enumerate >>= (\a -> maybe [] (pure.(,) a) (k a)))

With that knowledge, we can answer your question by deciding: Is the
Kleisli category of the Maybe monad on finite types Cartesian closed?
Short answer: It is not even Cartesian. 
There is an adjunction between the categories (->) and (Kleisli m) for
every monad m, where
* The left adjoint functor takes 
   types x to x,
   functions f to return.f
* The right adjoint functor takes 
   types x to m x,
   Kleisli maps f to (=<<) f
Right adjoint functors preserve all existing limits, which includes
products. Therefore, if (Kleisli m) has binary products, then m must
preserve them. So if P x y was the product of x and y in Kleisli m,
then m (P x y) would be isomorphic to (m x,m y). This seems not to hold
for m = Maybe: I can not imagine a type constructor P where
Maybe (P x y) ~ (Maybe x,Maybe y).
In particular, P can not be (,). The only sensible Kleisli projections
from (x,y) would be fst' = return.fst and snd' = return.snd. Now think
of two Kleisli maps f :: Bool -> Maybe x, g :: Bool -> Maybe y. Assume
that f True = Just x for some x and g True = Nothing. In order to
satisfy g True = (snd' <=< (f&&&g))True, the unique pair arrow (f&&&g)
would need to map True to Nothing, but then f True = (fst' <=< (f&&&g))
True can not hold. We conclude that (Kleisli Maybe) does not even have
categorical products, so asking for Cartesian closure does not make
sense. 

You might ask for a weaker property: For every type x, ((,) x) is a
functor on (Kleisli Maybe). Indeed, the following works because ((,) x)
is a polynomial functor. 
fmapKleisli :: Functor m => (a -> m b) -> (x,a) -> m (x,b)
fmapKleisli f (x,a) = fmap ((,) x) (f a)
Thus you may ask whether this functor has a right adjoint in the
Kleisli category of Maybe. This would be a type constructor g with a
natural isomorphism 

(x,a) -> Maybe b   ~   a -> Maybe (g b).

The first thing that comes to mind is to try
g b = x -> Maybe b and indeed djinn can provide two functions going
back and forth that have the right type, but they do not establish an
isomorphism. I doubt there is such a right adjoint g, but can not prove
it at the moment. The idea is that a function (x,a) -> Maybe b may
decide for Nothing depending on both x and a, and therefore the image
function under the isomorphism must map every a to Just (g b) and delay
the Nothing-decision to the g b. But for the reverse isomorphism you
can have functions that do not always return Just (g b) and there is no
preimage for these. 

Regards,
Olaf