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

Sat Jan 9 21:42:26 UTC 2021

Ah, I see.

On Sat, Jan 9, 2021, 4:41 PM MigMit <migmit at gmail.com> wrote:

> From the definition. To have a cartesian closed category you need some X^Y
> such that
>
> Z => X^Y ~ ZxY => X
>
> If your (=>) is defined as A => B ~ A -> Maybe B, and your AxB is
> OneOrBoth A B, then that's what you get.
>
> > On 9 Jan 2021, at 22:37, David Feuer <david.feuer at gmail.com> wrote:
> >
> > Where do you get
> >
> > () -> Maybe (X^Y) ~
> > OneOrBoth () Y -> Maybe X
> >
> > On Sat, Jan 9, 2021, 4:26 PM MigMit <migmit at gmail.com> 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).
> >
> > 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.
> >
> > > 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.
> >
> > _______________________________________________
> > 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/cd16b700/attachment-0001.html>