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

David Feuer david.feuer at gmail.com
Sun Jan 10 07:19:29 UTC 2021 

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.

On Sun, Jan 10, 2021, 2:16 AM Olaf Klinke <olf at aatal-apotheke.de> wrote:

> On Sat, 2021-01-09 at 18:04 -0500, David Feuer wrote:
> > `These` is not my own invention. It's in the `these` package.
>
> Then please interpret my "due to David Feuer" as "brought into this
> discussion by David Feuer". I wonder whether These has ever been linked
> to categorical products in Kleisli Maybe before. There are
> Data.These.Combinators.justHere and justThere which are the same as my
> fstMaybe and sndMaybe. But combinators resulting in pairKleisli and
> iso1 seem to be missing from the these package.
>
> Olaf
>
> >
> > On Sat, Jan 9, 2021, 5:41 PM Olaf Klinke <olf at aatal-apotheke.de>
> > wrote:
> >
> > > 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.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210110/38f88a99/attachment.html>

More information about the Haskell-Cafe mailing list