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

[宮里洸司]

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

No objections! I wanted to stress that it's always beneficial to start
from "obvious"
definitions. Maybe it's tedious, but too long is better than too vague
for readers.

Also, there can't be objections! You're the one to define. Of course
I could've speculated whatever definitions, but they're not necessarily related
to what you wanted to know.

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

So here was where the miscommunication happened. I think people
replying, including me,
were assuming you're thinking in terms of composing maps as concrete version of
Kleisli arrows `a -> Maybe b`.

>  ## Now to the technical details.

Thank you for details, I can get to write on the meat of the question.
Hope it helps!

Before starting, to be extra sure, let me restate we suppose `Map a b` are the
representation of *total* functions between finite subsets of `a` and `b`,
where these subsets are implicitly assumed.

The failing example can be seen as the result of the "implicitly assumed" part
not working well.

distribute :: (Ord a, Ord b) => Map a (Map b x) -> Map b (Map a x)
distribute = Map.unionsWith Map.union . Map.mapWithKey (fmap . Map.singleton)

m :: Map Int (Map Int x)
m = Map.fromList 1 [Map.fromList []]

m' = distribute m = Map.fromList []
m'' = distribute m' {- should be equal to m -}

Let me write the "implicitly assumed" subsets, using the imaginary syntax:

m :: Map {1} (Map ∅ x)
m' :: Map ∅ (Map ?? x)

The problem occurs here. Because the domain and the range of each map is
implicit, you can lose track of the "type" in the empty map. ("type"
here doesn't
mean an actual type Haskell checks for you, but virtual one asserting
which finite
sets are the domain and range of a given Map.)

The most easy (but less flexible) way to recover a nice mathematical structure
will be restricting Maps to be nonempty. There's no case you lose
"type" information
other than it.


--
/* Koji Miyazato <viercc at gmail.com> */