A quick question about distribution of finite maps.

[Ignat Insarov]

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

[Tom Smeding-3]

Hi Ignat,

A ghci session:


Prelude> import Test.QuickCheck
Prelude Test.QuickCheck> import qualified Data.Map.Strict as Map
Prelude Test.QuickCheck Map> import Data.Map.Strict (Map)
Prelude Test.QuickCheck Map Data.Map.Strict> let distribute = Map.unionsWith Map.union . Map.mapWithKey (fmap . Map.singleton)
Prelude Test.QuickCheck Map Data.Map.Strict> quickCheck $ \m -> distribute (distribute m) == (m :: Map Int (Map Int Int))
*** Failed! Falsified (after 2 tests and 2 shrinks):
fromList [(0,fromList [])]
Prelude Test.QuickCheck Map Data.Map.Strict> distribute (Map.singleton 1 mempty)
fromList []


It seems your property fails with the map `fromList [(0, fromList [])]`. I'm not sure if you need it to work for that case; I'm not a category theorist.

Cheers,
Tom


‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Saturday, January 9, 2021 9:38 AM, Ignat Insarov <[hidden email]> 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 suchcategories 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
>
> 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.

[Ignat Insarov]

Thanks Tom!

This is not a complete disaster theoretically, because a `mempty` map
corresponds to a function with `Void` domain which may not be invoked
anyway. But truly it makes the definition problematic, in the way
similar to how `Set` is not quite a functor — usually it works but
sometimes _map g ∘ map f_ may lose more elements than _map (g ∘ f)_.

I am not sure how much of sad I should be about it. The function still
works most of the time.
_______________________________________________
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 - Haskell-Cafe mailing list]

On Sat, Jan 09 2021 16:30, Ignat Insarov wrote:
> This is not a complete disaster theoretically, because a `mempty` map
> corresponds to a function with `Void` domain which may not be invoked
> anyway. 

A law failing just because the object one is looking at happens to be
inital sounds like a pretty severe theoretical disaster to me.

> Finite maps from `"containers" Data.Map` look like they may form a
> Cartesian closed category.

What category are you using as a base here?  I suppose it's not just
Set, as one could easily model finite maps as a finite set of tuples
there (and finite sets are definitely cartesian closed); is it some
idealised version of Hask (so that it actually exists :-)?
_______________________________________________
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.

[Ignat Insarov]

> > This is not a complete disaster theoretically, because a `mempty` map
> > corresponds to a function with `Void` domain which may not be invoked
> > anyway.
>
> A law failing just because the object one is looking at happens to be inital
> sounds like a pretty severe theoretical disaster to me.

When I said _«theoretically»_, I meant that a map `Map.singleton 1 (mempty ::
Map)` is the same as `mempty :: Map` because there is no such tuple of keys that
you would be able to extract any value. In other words, _{1} × { } ⇸ α_ is the
same as _{ } ⇸ α_, so both are of type `Void → α` and there is only one such
map. Insofar as I only care about values, I may never observe a difference.

By the way, finite maps are also problematic in the sense that there is any
number of identity maps of the same type, one for each finite subset of that
type. This makes it impossible to define a category of finite maps formally
within the Haskell type system. So maybe I should speak instead of a
semigroupoid and a semigroup of finite maps, removing both these corner cases
from consideration. The reality is that empty maps are my enemy anyway — I even
have a special function:

    dropEmpty :: (Filterable g, Foldable f) => g (f a) -> g (f a)
    dropEmpty = Witherable.filter (not . null)

— To contain their proliferation.

Of course, there are many ways an empty map may appear, such as via intersection
of maps with disjoint source sets. So some usual operations would need to
acquire more complicated types.

> What category are you using as a base here? I suppose it's not just Set, as
> one could easily model finite maps as a finite set of tuples there (and finite
> sets are definitely cartesian closed); is it some idealised version of Hask
> (so that it actually exists :-)?

I am not sure I follow you here. I see how we may model relations as sets of
tuples, but finite maps definitely need to be an abstract type of its own to
ensure that they are actually _functional_relations.

The category **Haskell** of Haskell types and total functions is not a suitable
category for these entities, because you cannot represent subsets in it, and
subsets are kinda the whole point of the exercise. So I look at it as though
**Haskell** is a subcategory of **Set** and **Finite Set** — the category of
finite sets and finite maps — is another, although not entirely disjoint
subcategory.
_______________________________________________
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.

[宮里 洸司]

Hi Ignat, would you slow down a bit and tell us the idea behind your
question?

You seem to expect Map forms a Cartesian closed category, and
want to know if the specific property of CCC holds ("functors of shape (a ⇸ -)
are distributive".)

Could you explain that expectation step-by-step? For the first step, let us know
the category made from Maps more clearly. I mean, (1) what are the objects
of that category? (2) what are the morphisms? (3) how the identity morphisms
and the composition of morphisms are defined?

The next step would be the "Cartesian" part. This category should have
direct product of any finite number of objects. What exactly are these,
and how do you define the projection morphisms (equivalents of `fst` and
`snd` in your category) and the product of morphisms (equivalent of `&&&`.)

It's too rushed to think about CCC until these aren't clear.

--
/* Koji Miyazato <[hidden email]> */
_______________________________________________
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.

[Olaf Klinke]

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

[David Feuer]

I don't know any of this category theory stuff, but you write "I can not imagine a type constructor P where

Maybe (P x y) ~ (Maybe x,Maybe y)". Unless there's some important condition missing from your statement, there indeed is such a constructor:

data These a b = This a | That b | These a b

Nothing -> (Nothing, Nothing)

Just (This a) -> (Just a, Nothing)

Just (That b) -> (Nothing, Just b)

Just (These a b) -> (Just a, Just b)

On Sat, Jan 9, 2021, 4:01 PM Olaf Klinke <[hidden email]> 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.

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

[migmit-2]

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 <[hidden email]> 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.

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

[David Feuer]

Where do you get

() -> Maybe (X^Y) ~

OneOrBoth () Y -> Maybe X

On Sat, Jan 9, 2021, 4:26 PM MigMit <[hidden email]> 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 <[hidden email]> 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.

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

[migmit-2]

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 <[hidden email]> wrote:
>
> Where do you get
>
> () -> Maybe (X^Y) ~
> OneOrBoth () Y -> Maybe X
>
> On Sat, Jan 9, 2021, 4:26 PM MigMit <[hidden email]> 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 <[hidden email]> 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.
>
> _______________________________________________
> 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.

[David Feuer]

Ah, I see.

On Sat, Jan 9, 2021, 4:41 PM MigMit <[hidden email]> wrote:

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 <[hidden email]> wrote:
>
> Where do you get
>
> () -> Maybe (X^Y) ~
> OneOrBoth () Y -> Maybe X
>
> On Sat, Jan 9, 2021, 4:26 PM MigMit <[hidden email]> 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 <[hidden email]> 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.
>
> _______________________________________________
> 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.

[Olaf Klinke]

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 <[hidden email]> 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.

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

[migmit-2]

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 <[hidden email]> 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 <[hidden email]> 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.
>

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

[David Feuer]

`These` is not my own invention. It's in the `these` package.

On Sat, Jan 9, 2021, 5:41 PM Olaf Klinke <[hidden email]> 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 <[hidden email]> 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.

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

[Olaf Klinke]

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 <[hidden email]>
> 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 <[hidden email]>
> > > > 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.

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

[David Feuer]

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 <[hidden email]> 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 <[hidden email]>
> 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 <[hidden email]>
> > > > 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.

_______________________________________________
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 - Haskell-Cafe mailing list]

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

-- Jack

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

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

[David Feuer]

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

On Sun, Jan 10, 2021, 2:54 AM <[hidden email]> wrote:

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

-- Jack

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

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

[Ignat Insarov]

Wow, this blew up overnight. Thank you Olaf and allies for attending to this
topic. But I think there is a hidden mismatch of premises. So let me take a step
back and look at things again, in order, from the ground up.

> Hi Ignat, would you slow down a bit and tell us the idea behind your
> question?
>
> You seem to expect Map forms a Cartesian closed category, and
> want to know if the specific property of CCC holds ("functors of shape (a ⇸ -)
> are distributive".)
>
> Could you explain that expectation step-by-step? For the first step, let us know
> the category made from Maps more clearly. I mean, (1) what are the objects
> of that category? (2) what are the morphisms? (3) how the identity morphisms
> and the composition of morphisms are defined?
>
> The next step would be the "Cartesian" part. This category should have
> direct product of any finite number of objects. What exactly are these,
> and how do you define the projection morphisms (equivalents of `fst` and
> `snd` in your category) and the product of morphisms (equivalent of `&&&`.)
>
> It's too rushed to think about CCC until these aren't clear.

This is most fair. Being a software engineer and not a mathematician, I was
hoping to avoid the scrutiny into what I was taking to be an accepted base
line. It did not play out as I hoped, so let us rewind.

As I offered previously:

> The category **Haskell** of Haskell types and total functions is not a
> suitable category for these entities, because you cannot represent subsets in
> it, and subsets are kinda the whole point of the exercise. So I look at it as
> though **Haskell** is a subcategory of **Set** and **Finite Set** — the
> category of finite sets and finite maps — is another, although not entirely
> disjoint subcategory.

I take **Finite Set** to be Cartesian closed with the same product and exponent
objects as its supercategory **Set**. Objections?

None, excellent. Now to the mentioned mismatch. There are two philosophies:

1. Let us model perfect Mathematics in an imperfect programming language as best
   we can.
2. Let us have only as much Mathematics as we can so our programming language
   remains perfect.

I employ the approach №1 here. Also, I already have a good idea of what I want
to do, and I already have code that works. This makes proofs of non-existence
somewhat less effective, in the sense that they cannot discourage me from
exploring the matter. If the idea cannot work, I need to know in what cases it
_does_ work. Actually, I find the idea that finite sets and functions may be
represented in Haskell very attractive in general, so I think it is worth the
effort to realize it in Haskell possibly better, even if perfect realization is
unattainable _(and it is)_.

That is not to say that I am going to ignore all objections. But I do want to
recover as much as can be recovered. If not a category, maybe a semigroupoid? If
not a monoid, maybe a semigroup? If we cannot model it in types, can we still
use it with imaginary proofs? Maybe we can use a clever normalization to exclude
pathologies? And so on.

Particularly, I do not invoke the `Maybe` stuff — instead I say that an
evaluation of a finite map on a value outside the set of its keys is an error
and it is the responsibility of the programmer to prove that no such evaluations
occur, even though they may pass the type checker. Yes, I give up type safety.

## Now to the technical details.

We do not have subtypes in Haskell, but we do have subsets and finite maps — it
is only that the type system does not know which subsets and finite maps are
compatible. So, we depart from the category **Haskell** of types and total
functions, and we allow instead that some values may be objects in our category
**X** — notably the values of type `Set α`.

* Now a function may be restricted to a finite set via `fromSet ∷ (k → a) → Set
  k → Map k a`, so there are arrows in **X** for every pair of an arrow of
  **Haskell** and a finite subset of an object of **Haskell** that has a total
  ordering _(or even mere decidable equality if we may sacrifice performance)_.

* An identity arrow for a given finite set is then a restriction of `id` to that
  set.

* Finite maps compose when the domain of one subsumes the range of the other via
  `fmap (g !) f`.

* Terminal object is the unique singleton of type `Set ( )` or any uniquely
  isomorphic singleton of a type with a single nullary constructor.

* The product of two finite sets is given by `cartesianProduct`, and projections
  are the appropriate restrictions of the usual `fst` and `snd`.

* The exponential object is a finite set of all maps with the same domain and
  range. I went on and invented the definitions witnessing the requisite
  isomorphose:

      curry = mapKeysWith union fst ∘ mapWithKey (singleton ∘ snd)
      uncurry = unions ∘ mapWithKey (mapKeys ∘ (, ))

  They pass any example except the one Tom gave earlier, with an empty map.

This establishes a Cartesian closed category of somewhat idealized entities. Can
the realization of this category in Haskell be perfected to exclude pathologies
by construction? Perhaps it is enough to normalize maps with `dropEmpty` before
comparison? Seems worth some research.
_______________________________________________
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.