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

[Olaf Klinke]

On Sat, 2021-01-09 at 22:26 +0100, MigMit wrote:
> Actually, it's pretty easy to construct a type `P x y`, so that Maybe
> (P x y) ~ (Maybe x, Maybe y). It would be
> 
> data OneOrBoth x y = Left' x | Right' y | Both x y
> 
> The isomorphism is, I think, obvious
> 
> iso1 :: Maybe (OneOrBoth x y) -> (Maybe x, Maybe y)
> iso1 Nothing = (Nothing, Nothing)
> iso1 (Just (Left' x)) = (Just x, Nothing)
> iso1 (Just (Right' y)) = (Nothing, Just y)
> iso1 (Just (Both x y)) = (Just x, Just y)
> 
> iso2 :: (Maybe x, Maybe y) -> Maybe (OneOrBoth x y)
> iso2 = -- left as an excersize for the reader
> 
> And indeed, "OneOrBoth" would be a cartesian product functor in the
> category of finite types (and maps).

I stand corrected. Below is the full code, in case anyone wants to play
with it. 

import Control.Arrow ((&&&))

-- due to David Feuer
data OneOrBoth x y = Left' x | Right' y | Both x y

iso2 :: (Maybe x,Maybe y) -> Maybe (OneOrBoth x y)
iso2 p = case p of
    (Nothing,Nothing) -> Nothing
    (Just x,Nothing) -> (Just (Left' x))
    (Nothing,Just y) -> (Just (Right' y))
    (Just x, Just y) -> (Just (Both x y))

-- (OneOrBoth x) is a functor on Kleisli Maybe
fmapKleisli :: (a -> Maybe b) ->
    OneOrBoth x a -> Maybe (OneOrBoth x b)
fmapKleisli k (Left' x) = Just (Left' x)
fmapKleisli k (Right' a) = fmap Right' (k a)
fmapKleisli k (Both x a) = fmap (Both x) (k a)

-- is OneOrBoth the cartesian product? Seems so:

pairKleisli :: (a -> Maybe x) -> 
    (a -> Maybe y) -> 
    a -> Maybe (OneOrBoth x y)
pairKleisli f g = iso2 . (f &&& g)

fstMaybe :: OneOrBoth x y -> Maybe x
fstMaybe (Left' x) = Just x
fstMaybe (Both x _) = Just x
fstMaybe (Right' _) = Nothing

sndMaybe :: OneOrBoth x y -> Maybe y
sndMaybe (Left' _) = Nothing
sndMaybe (Right' y) = Just y
sndMaybe (Both _ y) = Just y

> 
> But it won't be cartesian closed. If it were, then for any finite X
> and Y we should have
> 
> Maybe (X^Y) ~
> () -> Maybe (X^Y) ~
> OneOrBoth () Y -> Maybe X ~
> (() -> Maybe X, Y -> Maybe X, ((), Y) -> Maybe X) ~
> (Maybe X, Y -> Maybe X, Y -> Maybe X)
> 
> so
> 
> X^Y ~ (X, Y -> Maybe X, Y -> Maybe X)
> 
> But then
> 
> Z -> Maybe (X^Y) ~
> Z -> (Maybe X, Y -> Maybe X, Y -> Maybe X) ~
> (Z -> Maybe X, (Z, Y) -> Maybe X, (Z, Y) -> Maybe X) ~
> 
> and
> 
> OneOrBoth Z Y -> Maybe X ~
> (Z -> Maybe X, Y -> Maybe X, (Z, Y) -> Maybe X)
> 
> We see that those aren't the same, they have a different number of
> elements, so, no luck.

Doesn't this chain of isomorphisms require () to be the terminal
object, or did you take () as synonym for the terminal object in the
category? For example, there are several functions of the type 
Bool -> Maybe ().
So the terminal object in Kleisli Maybe would be Void, because Maybe
Void ~ (). We'd need to make fields in OneOrBoth strict to have an
isomorphism OneOrBoth Void a ~ a, just as the true categorical product
in (->) is the strict pair. 

Olaf

> 
> > On 9 Jan 2021, at 22:01, 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.