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

[jack at jackkelly.name]

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.