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

[MigMit]

No, my arrows and isomorphisms are all in the original category, not the Kleisli one — although the "X^Y" is the exponent in the Kleisli category.

> On 9 Jan 2021, at 23:40, 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.
>