<div dir="auto"><div>I just don't want to take credit for anyone else's work. I have a very vague recollection that Emily Pillmore may have looked at some related categorical stuff, but I could easily be mistaken.<br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jan 10, 2021, 2:16 AM 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">On Sat, 2021-01-09 at 18:04 -0500, David Feuer wrote:<br>
> `These` is not my own invention. It's in the `these` package.<br>
<br>
Then please interpret my "due to David Feuer" as "brought into this<br>
discussion by David Feuer". I wonder whether These has ever been linked<br>
to categorical products in Kleisli Maybe before. There are<br>
Data.These.Combinators.justHere and justThere which are the same as my<br>
fstMaybe and sndMaybe. But combinators resulting in pairKleisli and<br>
iso1 seem to be missing from the these package. <br>
<br>
Olaf<br>
<br>
> <br>
> On Sat, Jan 9, 2021, 5:41 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>><br>
> wrote:<br>
> <br>
> > On Sat, 2021-01-09 at 22:26 +0100, MigMit wrote:<br>
> > > Actually, it's pretty easy to construct a type `P x y`, so that<br>
> > > Maybe<br>
> > > (P x y) ~ (Maybe x, Maybe y). It would be<br>
> > > <br>
> > > data OneOrBoth x y = Left' x | Right' y | Both x y<br>
> > > <br>
> > > The isomorphism is, I think, obvious<br>
> > > <br>
> > > iso1 :: Maybe (OneOrBoth x y) -> (Maybe x, Maybe y)<br>
> > > iso1 Nothing = (Nothing, Nothing)<br>
> > > iso1 (Just (Left' x)) = (Just x, Nothing)<br>
> > > iso1 (Just (Right' y)) = (Nothing, Just y)<br>
> > > iso1 (Just (Both x y)) = (Just x, Just y)<br>
> > > <br>
> > > iso2 :: (Maybe x, Maybe y) -> Maybe (OneOrBoth x y)<br>
> > > iso2 = -- left as an excersize for the reader<br>
> > > <br>
> > > And indeed, "OneOrBoth" would be a cartesian product functor in<br>
> > > the<br>
> > > category of finite types (and maps).<br>
> > <br>
> > I stand corrected. Below is the full code, in case anyone wants to<br>
> > play<br>
> > with it.<br>
> > <br>
> > import Control.Arrow ((&&&))<br>
> > <br>
> > -- due to David Feuer<br>
> > data OneOrBoth x y = Left' x | Right' y | Both x y<br>
> > <br>
> > iso2 :: (Maybe x,Maybe y) -> Maybe (OneOrBoth x y)<br>
> > iso2 p = case p of<br>
> >     (Nothing,Nothing) -> Nothing<br>
> >     (Just x,Nothing) -> (Just (Left' x))<br>
> >     (Nothing,Just y) -> (Just (Right' y))<br>
> >     (Just x, Just y) -> (Just (Both x y))<br>
> > <br>
> > -- (OneOrBoth x) is a functor on Kleisli Maybe<br>
> > fmapKleisli :: (a -> Maybe b) -><br>
> >     OneOrBoth x a -> Maybe (OneOrBoth x b)<br>
> > fmapKleisli k (Left' x) = Just (Left' x)<br>
> > fmapKleisli k (Right' a) = fmap Right' (k a)<br>
> > fmapKleisli k (Both x a) = fmap (Both x) (k a)<br>
> > <br>
> > -- is OneOrBoth the cartesian product? Seems so:<br>
> > <br>
> > pairKleisli :: (a -> Maybe x) -><br>
> >     (a -> Maybe y) -><br>
> >     a -> Maybe (OneOrBoth x y)<br>
> > pairKleisli f g = iso2 . (f &&& g)<br>
> > <br>
> > fstMaybe :: OneOrBoth x y -> Maybe x<br>
> > fstMaybe (Left' x) = Just x<br>
> > fstMaybe (Both x _) = Just x<br>
> > fstMaybe (Right' _) = Nothing<br>
> > <br>
> > sndMaybe :: OneOrBoth x y -> Maybe y<br>
> > sndMaybe (Left' _) = Nothing<br>
> > sndMaybe (Right' y) = Just y<br>
> > sndMaybe (Both _ y) = Just y<br>
> > <br>
> > > But it won't be cartesian closed. If it were, then for any finite<br>
> > > X<br>
> > > and Y we should have<br>
> > > <br>
> > > Maybe (X^Y) ~<br>
> > > () -> Maybe (X^Y) ~<br>
> > > OneOrBoth () Y -> Maybe X ~<br>
> > > (() -> Maybe X, Y -> Maybe X, ((), Y) -> Maybe X) ~<br>
> > > (Maybe X, Y -> Maybe X, Y -> Maybe X)<br>
> > > <br>
> > > so<br>
> > > <br>
> > > X^Y ~ (X, Y -> Maybe X, Y -> Maybe X)<br>
> > > <br>
> > > But then<br>
> > > <br>
> > > Z -> Maybe (X^Y) ~<br>
> > > Z -> (Maybe X, Y -> Maybe X, Y -> Maybe X) ~<br>
> > > (Z -> Maybe X, (Z, Y) -> Maybe X, (Z, Y) -> Maybe X) ~<br>
> > > <br>
> > > and<br>
> > > <br>
> > > OneOrBoth Z Y -> Maybe X ~<br>
> > > (Z -> Maybe X, Y -> Maybe X, (Z, Y) -> Maybe X)<br>
> > > <br>
> > > We see that those aren't the same, they have a different number<br>
> > > of<br>
> > > elements, so, no luck.<br>
> > <br>
> > Doesn't this chain of isomorphisms require () to be the terminal<br>
> > object, or did you take () as synonym for the terminal object in<br>
> > the<br>
> > category? For example, there are several functions of the type<br>
> > Bool -> Maybe ().<br>
> > So the terminal object in Kleisli Maybe would be Void, because<br>
> > Maybe<br>
> > Void ~ (). We'd need to make fields in OneOrBoth strict to have an<br>
> > isomorphism OneOrBoth Void a ~ a, just as the true categorical<br>
> > product<br>
> > in (->) is the strict pair.<br>
> > <br>
> > Olaf<br>
> > <br>
> > > > On 9 Jan 2021, at 22:01, Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>><br>
> > > > wrote:<br>
> > > > <br>
> > > > > Hello!<br>
> > > > > <br>
> > > > > Finite maps from `"containers" Data.Map` look like they may<br>
> > > > > form<br>
> > > > > a<br>
> > > > > Cartesian closed category. So it makes sense to ask if the<br>
> > > > > rule<br>
> > > > > _α ⇸<br>
> > > > > (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds<br>
> > > > > in<br>
> > > > > such<br>
> > > > > categories does hold for finite maps. Note that, a map being<br>
> > > > > a<br>
> > > > > functor, this also may be seen as _f (g α) ≡ g (f α)_, which<br>
> > > > > 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 .<br>
> > > > > singleton)<br>
> > > > > <br>
> > > > > — And it works on simple examples. _(I checked the law<br>
> > > > > `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>
> > > > > <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>
> > > > Hi Ignat,<br>
> > > > <br>
> > > > TL;DR: No and no.<br>
> > > > <br>
> > > > The documentation says that every distributive functor is of<br>
> > > > the<br>
> > > > 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<br>
> > > > already<br>
> > > > commented on that. Next, a Map is always finite, hence let's<br>
> > > > pretend<br>
> > > > that we are working inside the category of finite types and<br>
> > > > functions.<br>
> > > > Then the problems of missing identity and missing Ord go away.<br>
> > > > Once<br>
> > > > that all types are finite, we can assume an enumerator. That<br>
> > > > is,<br>
> > > > 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<br>
> > > > a<br>
> > > > Kleisli map (a -> Maybe b). Convince yourself that Map<br>
> > > > concatenation<br>
> > > > has the same semantics as Kleisli composition (<=<). Given a<br>
> > > > Kleisli<br>
> > > > map k between finite types, we build a Map as follows.<br>
> > > > \k -> Map.fromList (enumerate >>= (\a -> maybe [] (pure.(,) a)<br>
> > > > (k<br>
> > > > a)))<br>
> > > > <br>
> > > > With that knowledge, we can answer your question by deciding:<br>
> > > > Is<br>
> > > > the<br>
> > > > Kleisli category of the Maybe monad on finite types Cartesian<br>
> > > > closed?<br>
> > > > Short answer: It is not even Cartesian.<br>
> > > > There is an adjunction between the categories (->) and (Kleisli<br>
> > > > m)<br>
> > > > 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<br>
> > > > includes<br>
> > > > products. Therefore, if (Kleisli m) has binary products, then m<br>
> > > > must<br>
> > > > preserve them. So if P x y was the product of x and y in<br>
> > > > Kleisli m,<br>
> > > > then m (P x y) would be isomorphic to (m x,m y). This seems not<br>
> > > > to<br>
> > > > 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<br>
> > > > projections<br>
> > > > from (x,y) would be fst' = return.fst and snd' = return.snd.<br>
> > > > Now<br>
> > > > think<br>
> > > > of two Kleisli maps f :: Bool -> Maybe x, g :: Bool -> Maybe y.<br>
> > > > Assume<br>
> > > > that f True = Just x for some x and g True = Nothing. In order<br>
> > > > to<br>
> > > > satisfy g True = (snd' <=< (f&&&g))True, the unique pair arrow<br>
> > > > (f&&&g)<br>
> > > > would need to map True to Nothing, but then f True = (fst' <=<<br>
> > > > (f&&&g))<br>
> > > > True can not hold. We conclude that (Kleisli Maybe) does not<br>
> > > > even<br>
> > > > have<br>
> > > > categorical products, so asking for Cartesian closure does not<br>
> > > > make<br>
> > > > sense.<br>
> > > > <br>
> > > > You might ask for a weaker property: For every type x, ((,) x)<br>
> > > > is a<br>
> > > > functor on (Kleisli Maybe). Indeed, the following works because<br>
> > > > ((,) 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<br>
> > > > the<br>
> > > > Kleisli category of Maybe. This would be a type constructor g<br>
> > > > with<br>
> > > > 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<br>
> > > > going<br>
> > > > back and forth that have the right type, but they do not<br>
> > > > establish<br>
> > > > an<br>
> > > > isomorphism. I doubt there is such a right adjoint g, but can<br>
> > > > not<br>
> > > > prove<br>
> > > > it at the moment. The idea is that a function (x,a) -> Maybe b<br>
> > > > may<br>
> > > > decide for Nothing depending on both x and a, and therefore the<br>
> > > > image<br>
> > > > function under the isomorphism must map every a to Just (g b)<br>
> > > > and<br>
> > > > delay<br>
> > > > the Nothing-decision to the g b. But for the reverse<br>
> > > > isomorphism<br>
> > > > you<br>
> > > > can have functions that do not always return Just (g b) and<br>
> > > > there<br>
> > > > 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<br>
> > > > post.<br>
<br>
</blockquote></div></div></div>