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

10 Jan 2021


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

-- Jack

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

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

jack＠jackkelly.name