A quick question about distribution of finite maps.

26 messages
12
Open this post in threaded view
|

A quick question about distribution of finite maps.

 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

 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-cafeOnly members subscribed via the mailman list are allowed to post.
Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|

Re: A quick question about distribution of finite maps.

Open this post in threaded view
|