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

[Tom Smeding]

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 <kindaro at gmail.com> 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.