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

Sun Jan 10 11:53:31 UTC 2021

You found it! See specifically the documentation for Data.Can.

On Sun, Jan 10, 2021, 2:54 AM <jack at jackkelly.name> wrote:

> You may be thinking of https://hackage.haskell.org/package/smash and
> related packages.
>
> -- Jack
>
> January 10, 2021 5:19 PM, "David Feuer" <david.feuer at gmail.com> wrote:
>
> > 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/fb05232b/attachment.html>