<div dir="auto">You found it! See specifically the documentation for Data.Can.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jan 10, 2021, 2:54 AM  <<a href="mailto:jack@jackkelly.name">jack@jackkelly.name</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You may be thinking of <a href="https://hackage.haskell.org/package/smash" rel="noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/smash</a> and related packages.<br>
<br>
-- Jack<br>
<br>
January 10, 2021 5:19 PM, "David Feuer" <<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>> wrote:<br>
<br>
> I just don't want to take credit for anyone else's work. I have a very vague recollection that<br>
> Emily Pillmore may have looked at some related categorical stuff, but I could easily be mistaken.<br>
> <br>
> On Sun, Jan 10, 2021, 2:16 AM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>> wrote:<br>
> <br>
>> On Sat, 2021-01-09 at 18:04 -0500, David Feuer wrote:<br>
>>> `These` is not my own invention. It's in the `these` package.<br>
>> <br>
>> Then please interpret my "due to David Feuer" as "brought into this<br>
>> discussion by David Feuer". I wonder whether These has ever been linked<br>
>> to categorical products in Kleisli Maybe before. There are<br>
>> Data.These.Combinators.justHere and justThere which are the same as my<br>
>> fstMaybe and sndMaybe. But combinators resulting in pairKleisli and<br>
>> iso1 seem to be missing from the these package.<br>
>> <br>
>> Olaf<br>
>> <br>
>>> <br>
>>> On Sat, Jan 9, 2021, 5:41 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>><br>
>>> wrote:<br>
>>> <br>
>>>> On Sat, 2021-01-09 at 22:26 +0100, MigMit wrote:<br>
>>>>> Actually, it's pretty easy to construct a type `P x y`, so that<br>
>>>>> Maybe<br>
>>>>> (P x y) ~ (Maybe x, Maybe y). It would be<br>
>>>>> <br>
>>>>> data OneOrBoth x y = Left' x | Right' y | Both x y<br>
>>>>> <br>
>>>>> The isomorphism is, I think, obvious<br>
>>>>> <br>
>>>>> iso1 :: Maybe (OneOrBoth x y) -> (Maybe x, Maybe y)<br>
>>>>> iso1 Nothing = (Nothing, Nothing)<br>
>>>>> iso1 (Just (Left' x)) = (Just x, Nothing)<br>
>>>>> iso1 (Just (Right' y)) = (Nothing, Just y)<br>
>>>>> iso1 (Just (Both x y)) = (Just x, Just y)<br>
>>>>> <br>
>>>>> iso2 :: (Maybe x, Maybe y) -> Maybe (OneOrBoth x y)<br>
>>>>> iso2 = -- left as an excersize for the reader<br>
>>>>> <br>
>>>>> And indeed, "OneOrBoth" would be a cartesian product functor in<br>
>>>>> the<br>
>>>>> category of finite types (and maps).<br>
>>>> <br>
>>>> I stand corrected. Below is the full code, in case anyone wants to<br>
>>>> play<br>
>>>> with it.<br>
>>>> <br>
>>>> import Control.Arrow ((&&&))<br>
>>>> <br>
>>>> -- due to David Feuer<br>
>>>> data OneOrBoth x y = Left' x | Right' y | Both x y<br>
>>>> <br>
>>>> iso2 :: (Maybe x,Maybe y) -> Maybe (OneOrBoth x y)<br>
>>>> iso2 p = case p of<br>
>>>> (Nothing,Nothing) -> Nothing<br>
>>>> (Just x,Nothing) -> (Just (Left' x))<br>
>>>> (Nothing,Just y) -> (Just (Right' y))<br>
>>>> (Just x, Just y) -> (Just (Both x y))<br>
>>>> <br>
>>>> -- (OneOrBoth x) is a functor on Kleisli Maybe<br>
>>>> fmapKleisli :: (a -> Maybe b) -><br>
>>>> OneOrBoth x a -> Maybe (OneOrBoth x b)<br>
>>>> fmapKleisli k (Left' x) = Just (Left' x)<br>
>>>> fmapKleisli k (Right' a) = fmap Right' (k a)<br>
>>>> fmapKleisli k (Both x a) = fmap (Both x) (k a)<br>
>>>> <br>
>>>> -- is OneOrBoth the cartesian product? Seems so:<br>
>>>> <br>
>>>> pairKleisli :: (a -> Maybe x) -><br>
>>>> (a -> Maybe y) -><br>
>>>> a -> Maybe (OneOrBoth x y)<br>
>>>> pairKleisli f g = iso2 . (f &&& g)<br>
>>>> <br>
>>>> fstMaybe :: OneOrBoth x y -> Maybe x<br>
>>>> fstMaybe (Left' x) = Just x<br>
>>>> fstMaybe (Both x _) = Just x<br>
>>>> fstMaybe (Right' _) = Nothing<br>
>>>> <br>
>>>> sndMaybe :: OneOrBoth x y -> Maybe y<br>
>>>> sndMaybe (Left' _) = Nothing<br>
>>>> sndMaybe (Right' y) = Just y<br>
>>>> sndMaybe (Both _ y) = Just y<br>
>>>> <br>
>>>>> But it won't be cartesian closed. If it were, then for any finite<br>
>>>>> X<br>
>>>>> and Y we should have<br>
>>>>> <br>
>>>>> Maybe (X^Y) ~<br>
>>>>> () -> Maybe (X^Y) ~<br>
>>>>> OneOrBoth () Y -> Maybe X ~<br>
>>>>> (() -> Maybe X, Y -> Maybe X, ((), Y) -> Maybe X) ~<br>
>>>>> (Maybe X, Y -> Maybe X, Y -> Maybe X)<br>
>>>>> <br>
>>>>> so<br>
>>>>> <br>
>>>>> X^Y ~ (X, Y -> Maybe X, Y -> Maybe X)<br>
>>>>> <br>
>>>>> But then<br>
>>>>> <br>
>>>>> Z -> Maybe (X^Y) ~<br>
>>>>> Z -> (Maybe X, Y -> Maybe X, Y -> Maybe X) ~<br>
>>>>> (Z -> Maybe X, (Z, Y) -> Maybe X, (Z, Y) -> Maybe X) ~<br>
>>>>> <br>
>>>>> and<br>
>>>>> <br>
>>>>> OneOrBoth Z Y -> Maybe X ~<br>
>>>>> (Z -> Maybe X, Y -> Maybe X, (Z, Y) -> Maybe X)<br>
>>>>> <br>
>>>>> We see that those aren't the same, they have a different number<br>
>>>>> of<br>
>>>>> elements, so, no luck.<br>
>>>> <br>
>>>> Doesn't this chain of isomorphisms require () to be the terminal<br>
>>>> object, or did you take () as synonym for the terminal object in<br>
>>>> the<br>
>>>> category? For example, there are several functions of the type<br>
>>>> Bool -> Maybe ().<br>
>>>> So the terminal object in Kleisli Maybe would be Void, because<br>
>>>> Maybe<br>
>>>> Void ~ (). We'd need to make fields in OneOrBoth strict to have an<br>
>>>> isomorphism OneOrBoth Void a ~ a, just as the true categorical<br>
>>>> product<br>
>>>> in (->) is the strict pair.<br>
>>>> <br>
>>>> Olaf<br>
>>>> <br>
>>>>>> On 9 Jan 2021, at 22:01, Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank" rel="noreferrer">olf@aatal-apotheke.de</a>><br>
>>>>>> wrote:<br>
>>>>>> <br>
>>>>>>> Hello!<br>
>>>>>>> <br>
>>>>>>> Finite maps from `"containers" Data.Map` look like they may<br>
>>>>>>> form<br>
>>>>>>> a<br>
>>>>>>> Cartesian closed category. So it makes sense to ask if the<br>
>>>>>>> rule<br>
>>>>>>> _α ⇸<br>
>>>>>>> (β ⇸ γ) ≡ ⟨α; β⟩ ⇸ γ ≡ ⟨β; α⟩ ⇸ γ ≡ β ⇸ (α ⇸ γ)_ that holds<br>
>>>>>>> in<br>
>>>>>>> such<br>
>>>>>>> categories does hold for finite maps. Note that, a map being<br>
>>>>>>> a<br>
>>>>>>> functor, this also may be seen as _f (g α) ≡ g (f α)_, which<br>
>>>>>>> would<br>
>>>>>>> work if maps were `Distributive` [1].<br>
>>>>>>> <br>
>>>>>>> It looks to me as though the following definition might work:<br>
>>>>>>> <br>
>>>>>>> distribute = unionsWith union . mapWithKey (fmap .<br>
>>>>>>> singleton)<br>
>>>>>>> <br>
>>>>>>> — And it works on simple examples. _(I checked the law<br>
>>>>>>> `distribute ∘<br>
>>>>>>> distribute ≡ id` — it appears to be the only law required.)_<br>
>>>>>>> <br>
>>>>>>> Is this definition correct? Is it already known and defined<br>
>>>>>>> elsewhere?<br>
>>>>>>> <br>
>>>>>>> [1]:<br>
>>>>>>> <br>
>>>> <br>
>> <a href="https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distributive.html#t:Distributive" rel="noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/distributive-0.6.2.1/docs/Data-Distributive.html#t:Distributive</a><br>
>>>>>> Hi Ignat,<br>
>>>>>> <br>
>>>>>> TL;DR: No and no.<br>
>>>>>> <br>
>>>>>> The documentation says that every distributive functor is of<br>
>>>>>> the<br>
>>>>>> form<br>
>>>>>> (->) x for some x, and (Map a) is not like this.<br>
>>>>>> <br>
>>>>>> If Maps were a category, what is the identity morphism?<br>
>>>>>> <br>
>>>>>> Let's put the Ord constraint on the keys aside, Tom Smeding has<br>
>>>>>> already<br>
>>>>>> commented on that. Next, a Map is always finite, hence let's<br>
>>>>>> pretend<br>
>>>>>> that we are working inside the category of finite types and<br>
>>>>>> functions.<br>
>>>>>> Then the problems of missing identity and missing Ord go away.<br>
>>>>>> Once<br>
>>>>>> that all types are finite, we can assume an enumerator. That<br>
>>>>>> is,<br>
>>>>>> each<br>
>>>>>> type x has an operation<br>
>>>>>> enumerate :: [x]<br>
>>>>>> which we will use to construct the inverse of<br>
>>>>>> flip Map.lookup :: Map a b -> a -> Maybe b<br>
>>>>>> thereby showing that a Map is nothing but a memoized version of<br>
>>>>>> a<br>
>>>>>> Kleisli map (a -> Maybe b). Convince yourself that Map<br>
>>>>>> concatenation<br>
>>>>>> has the same semantics as Kleisli composition (<=<). Given a<br>
>>>>>> Kleisli<br>
>>>>>> map k between finite types, we build a Map as follows.<br>
>>>>>> \k -> Map.fromList (enumerate >>= (\a -> maybe [] (pure.(,) a)<br>
>>>>>> (k<br>
>>>>>> a)))<br>
>>>>>> <br>
>>>>>> With that knowledge, we can answer your question by deciding:<br>
>>>>>> Is<br>
>>>>>> the<br>
>>>>>> Kleisli category of the Maybe monad on finite types Cartesian<br>
>>>>>> closed?<br>
>>>>>> Short answer: It is not even Cartesian.<br>
>>>>>> There is an adjunction between the categories (->) and (Kleisli<br>
>>>>>> m)<br>
>>>>>> for<br>
>>>>>> every monad m, where<br>
>>>>>> * The left adjoint functor takes<br>
>>>>>> types x to x,<br>
>>>>>> functions f to return.f<br>
>>>>>> * The right adjoint functor takes<br>
>>>>>> types x to m x,<br>
>>>>>> Kleisli maps f to (=<<) f<br>
>>>>>> Right adjoint functors preserve all existing limits, which<br>
>>>>>> includes<br>
>>>>>> products. Therefore, if (Kleisli m) has binary products, then m<br>
>>>>>> must<br>
>>>>>> preserve them. So if P x y was the product of x and y in<br>
>>>>>> Kleisli m,<br>
>>>>>> then m (P x y) would be isomorphic to (m x,m y). This seems not<br>
>>>>>> to<br>
>>>>>> hold<br>
>>>>>> for m = Maybe: I can not imagine a type constructor P where<br>
>>>>>> Maybe (P x y) ~ (Maybe x,Maybe y).<br>
>>>>>> In particular, P can not be (,). The only sensible Kleisli<br>
>>>>>> projections<br>
>>>>>> from (x,y) would be fst' = return.fst and snd' = return.snd.<br>
>>>>>> Now<br>
>>>>>> think<br>
>>>>>> of two Kleisli maps f :: Bool -> Maybe x, g :: Bool -> Maybe y.<br>
>>>>>> Assume<br>
>>>>>> that f True = Just x for some x and g True = Nothing. In order<br>
>>>>>> to<br>
>>>>>> satisfy g True = (snd' <=< (f&&&g))True, the unique pair arrow<br>
>>>>>> (f&&&g)<br>
>>>>>> would need to map True to Nothing, but then f True = (fst' <=<<br>
>>>>>> (f&&&g))<br>
>>>>>> True can not hold. We conclude that (Kleisli Maybe) does not<br>
>>>>>> even<br>
>>>>>> have<br>
>>>>>> categorical products, so asking for Cartesian closure does not<br>
>>>>>> make<br>
>>>>>> sense.<br>
>>>>>> <br>
>>>>>> You might ask for a weaker property: For every type x, ((,) x)<br>
>>>>>> is a<br>
>>>>>> functor on (Kleisli Maybe). Indeed, the following works because<br>
>>>>>> ((,) x)<br>
>>>>>> is a polynomial functor.<br>
>>>>>> fmapKleisli :: Functor m => (a -> m b) -> (x,a) -> m (x,b)<br>
>>>>>> fmapKleisli f (x,a) = fmap ((,) x) (f a)<br>
>>>>>> Thus you may ask whether this functor has a right adjoint in<br>
>>>>>> the<br>
>>>>>> Kleisli category of Maybe. This would be a type constructor g<br>
>>>>>> with<br>
>>>>>> a<br>
>>>>>> natural isomorphism<br>
>>>>>> <br>
>>>>>> (x,a) -> Maybe b ~ a -> Maybe (g b).<br>
>>>>>> <br>
>>>>>> The first thing that comes to mind is to try<br>
>>>>>> g b = x -> Maybe b and indeed djinn can provide two functions<br>
>>>>>> going<br>
>>>>>> back and forth that have the right type, but they do not<br>
>>>>>> establish<br>
>>>>>> an<br>
>>>>>> isomorphism. I doubt there is such a right adjoint g, but can<br>
>>>>>> not<br>
>>>>>> prove<br>
>>>>>> it at the moment. The idea is that a function (x,a) -> Maybe b<br>
>>>>>> may<br>
>>>>>> decide for Nothing depending on both x and a, and therefore the<br>
>>>>>> image<br>
>>>>>> function under the isomorphism must map every a to Just (g b)<br>
>>>>>> and<br>
>>>>>> delay<br>
>>>>>> the Nothing-decision to the g b. But for the reverse<br>
>>>>>> isomorphism<br>
>>>>>> you<br>
>>>>>> can have functions that do not always return Just (g b) and<br>
>>>>>> there<br>
>>>>>> is no<br>
>>>>>> preimage for these.<br>
>>>>>> <br>
>>>>>> Regards,<br>
>>>>>> Olaf<br>
>>>>>> <br>
>>>>>> <br>
>>>>>> <br>
>>>>>> _______________________________________________<br>
>>>>>> Haskell-Cafe mailing list<br>
>>>>>> To (un)subscribe, modify options or view archives go to:<br>
>>>>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
>>>>>> Only members subscribed via the mailman list are allowed to<br>
>>>>>> post.<br>
</blockquote></div>