<div dir="auto">I don't know any of this category theory stuff, but you write "I can not imagine a type constructor P where<div dir="auto">Maybe (P x y) ~ (Maybe x,Maybe y)". Unless there's some important condition missing from your statement, there indeed is such a constructor:</div><div dir="auto"><br></div><div dir="auto">data These a b = This a | That b | These a b</div><div dir="auto"><br></div><div dir="auto">Nothing -> (Nothing, Nothing)</div><div dir="auto">Just (This a) -> (Just a, Nothing)</div><div dir="auto">Just (That b) -> (Nothing, Just b)</div><div dir="auto">Just (These a b) -> (Just a, Just b)</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jan 9, 2021, 4:01 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> Hello!<br>
> <br>
> Finite maps from `"containers" Data.Map` look like they may form a<br>
> Cartesian closed category. So it makes sense to ask if the rule _α ⇸<br>
> (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds in such<br>
> categories does hold for finite maps. Note that, a map being a<br>
> functor, this also may be seen as _f (g α) ≡ g (f α)_, which would<br>
> work if maps were `Distributive` [1].<br>
> <br>
> It looks to me as though the following definition might work:<br>
> <br>
>     distribute = unionsWith union . mapWithKey (fmap . singleton)<br>
> <br>
> — And it works on simple examples. _(I checked the law `distribute ∘<br>
> distribute ≡ id` — it appears to be the only law required.)_<br>
> <br>
> Is this definition correct? Is it already known and defined<br>
> elsewhere?<br>
> <br>
> [1]: <br>
> <a href="https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distributive.html#t:Distributive" rel="noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distributive.html#t:Distributive</a><br>
<br>
Hi Ignat, <br>
<br>
TL;DR: No and no.<br>
<br>
The documentation says that every distributive functor is of the form<br>
(->) x for some x, and (Map a) is not like this. <br>
<br>
If Maps were a category, what is the identity morphism?<br>
<br>
Let's put the Ord constraint on the keys aside, Tom Smeding has already<br>
commented on that. Next, a Map is always finite, hence let's pretend<br>
that we are working inside the category of finite types and functions.<br>
Then the problems of missing identity and missing Ord go away. Once<br>
that all types are finite, we can assume an enumerator. That is, each<br>
type x has an operation<br>
enumerate :: [x]<br>
which we will use to construct the inverse of <br>
flip Map.lookup :: Map a b -> a -> Maybe b<br>
thereby showing that a Map is nothing but a memoized version of a<br>
Kleisli map (a -> Maybe b). Convince yourself that Map concatenation<br>
has the same semantics as Kleisli composition (<=<). Given a Kleisli<br>
map k between finite types, we build a Map as follows.<br>
\k -> Map.fromList (enumerate >>= (\a -> maybe [] (pure.(,) a) (k a)))<br>
<br>
With that knowledge, we can answer your question by deciding: Is the<br>
Kleisli category of the Maybe monad on finite types Cartesian closed?<br>
Short answer: It is not even Cartesian. <br>
There is an adjunction between the categories (->) and (Kleisli m) for<br>
every monad m, where<br>
* The left adjoint functor takes <br>
   types x to x,<br>
   functions f to return.f<br>
* The right adjoint functor takes <br>
   types x to m x,<br>
   Kleisli maps f to (=<<) f<br>
Right adjoint functors preserve all existing limits, which includes<br>
products. Therefore, if (Kleisli m) has binary products, then m must<br>
preserve them. So if P x y was the product of x and y in Kleisli m,<br>
then m (P x y) would be isomorphic to (m x,m y). This seems not to hold<br>
for m = Maybe: I can not imagine a type constructor P where<br>
Maybe (P x y) ~ (Maybe x,Maybe y).<br>
In particular, P can not be (,). The only sensible Kleisli projections<br>
from (x,y) would be fst' = return.fst and snd' = return.snd. Now think<br>
of two Kleisli maps f :: Bool -> Maybe x, g :: Bool -> Maybe y. Assume<br>
that f True = Just x for some x and g True = Nothing. In order to<br>
satisfy g True = (snd' <=< (f&&&g))True, the unique pair arrow (f&&&g)<br>
would need to map True to Nothing, but then f True = (fst' <=< (f&&&g))<br>
True can not hold. We conclude that (Kleisli Maybe) does not even have<br>
categorical products, so asking for Cartesian closure does not make<br>
sense. <br>
<br>
You might ask for a weaker property: For every type x, ((,) x) is a<br>
functor on (Kleisli Maybe). Indeed, the following works because ((,) x)<br>
is a polynomial functor. <br>
fmapKleisli :: Functor m => (a -> m b) -> (x,a) -> m (x,b)<br>
fmapKleisli f (x,a) = fmap ((,) x) (f a)<br>
Thus you may ask whether this functor has a right adjoint in the<br>
Kleisli category of Maybe. This would be a type constructor g with a<br>
natural isomorphism <br>
<br>
(x,a) -> Maybe b   ~   a -> Maybe (g b).<br>
<br>
The first thing that comes to mind is to try<br>
g b = x -> Maybe b and indeed djinn can provide two functions going<br>
back and forth that have the right type, but they do not establish an<br>
isomorphism. I doubt there is such a right adjoint g, but can not prove<br>
it at the moment. The idea is that a function (x,a) -> Maybe b may<br>
decide for Nothing depending on both x and a, and therefore the image<br>
function under the isomorphism must map every a to Just (g b) and delay<br>
the Nothing-decision to the g b. But for the reverse isomorphism you<br>
can have functions that do not always return Just (g b) and there is no<br>
preimage for these. <br>
<br>
Regards,<br>
Olaf<br>
<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>