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

[David Feuer]

I don't know any of this category theory stuff, but you write "I can not
imagine a type constructor P where
Maybe (P x y) ~ (Maybe x,Maybe y)". Unless there's some important condition
missing from your statement, there indeed is such a constructor:

data These a b = This a | That b | These a b

Nothing -> (Nothing, Nothing)
Just (This a) -> (Just a, Nothing)
Just (That b) -> (Nothing, Just b)
Just (These a b) -> (Just a, Just b)

On Sat, Jan 9, 2021, 4:01 PM Olaf Klinke <olf at aatal-apotheke.de> wrote:

> > 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
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210109/1fe0583e/attachment.html>