From the definition. To have a cartesian closed category you need some X^Y such that Z => X^Y ~ ZxY => X If your (=>) is defined as A => B ~ A -> Maybe B, and your AxB is OneOrBoth A B, then that's what you get.

On 9 Jan 2021, at 22:37, David Feuer wrote:

Where do you get

() -> Maybe (X^Y) ~ OneOrBoth () Y -> Maybe X

On Sat, Jan 9, 2021, 4:26 PM 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).

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.

...

On 9 Jan 2021, at 22:01, Olaf Klinke 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-Distribut...

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.

_______________________________________________ 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.

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 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-Distribut...

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.

On Sat, 2021-01-09 at 23:45 +0100, MigMit wrote: 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)

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.

I don't follow your argument. I still must be misinterpreting something. Maybe (X^Y) ~ () -> Maybe (X^Y) -- because () is terminal in Hask ~ OneOrBoth () Y -> Maybe X -- OneOrBoth is the product in Kleisli Maybe ~ (Maybe X, Y -> Maybe X, Y -> Maybe X) -- universal property of coproduct But how did you get to the next step: X^Y ~ (X, Y -> Maybe X, Y -> Maybe X) I think this can not hold for cardinality reasons: 1+X*((1+X)^Y)^2 /= (1+X)*((1+X)^Y)^2 Olaf

`These` is not my own invention. It's in the `these` package. On Sat, Jan 9, 2021, 5:41 PM Olaf Klinke 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 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-Distribut...

...

...

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.

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 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 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 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-Distribut...

...

...

...

...

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.

You found it! See specifically the documentation for Data.Can. On Sun, Jan 10, 2021, 2:54 AM wrote:

You may be thinking of https://hackage.haskell.org/package/smash and related packages.

-- Jack

January 10, 2021 5:19 PM, "David Feuer" 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 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 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 > 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-Distribut...

...

...

...

...

> 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.

On Sun, 2021-01-10 at 07:54 +0000, jack@jackkelly.name wrote:

You may be thinking of https://hackage.haskell.org/package/smash and related packages.

-- Jack

Excellent, thanks for the hint! I shall also keep an eye on Emily's packages in addition to Edward Kmett's when looking for category- related stuff. The documentation mentions that Can is the categorical product in Hask*. Unfortunately it does not say what the morphisms in Hask* are. The linked ncatlab page suggests the morphisms are point- preserving functions, which would fit Kleisli Maybe. The documentation of Data.Can also does not state whether canCurry and canUncurry are mutually inverse. If so, that still does not contradict MigMit because the first argument to canCurry might not preserve the point, i.e. might not be a morphism of Hask*. Likewise, if the first argument k to canUncurry has k Nothing Nothing = Just _ then canUncurry k does not preserve the point, i.e. is not an element of Hask*. Anyways, we have Maybe (OneOrBoth x y) ~ Maybe (These x y) ~ Can x y with iso1 = can (\x -> (Just x,Nothing)) (\y -> (Nothing,Just y)) (\x y -> (Just x,Just y)) but still no mention of an inverse. Or am I missing something? How to constuct iso2 and pairKleisli using the combinators in Data.Can? Olaf

January 10, 2021 5:19 PM, "David Feuer" wrote:

...

I just don't want to take credit for anyone else's work.

Neither do I, hence I mentioned you in my code.

...

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 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

...

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@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-Distribut... > 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.