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