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

[Ignat Insarov]

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

When I said _«theoretically»_, I meant that a map `Map.singleton 1 (mempty ::
Map)` is the same as `mempty :: Map` because there is no such tuple of keys that
you would be able to extract any value. In other words, _{1} × { } ⇸ α_ is the
same as _{ } ⇸ α_, so both are of type `Void → α` and there is only one such
map. Insofar as I only care about values, I may never observe a difference.

By the way, finite maps are also problematic in the sense that there is any
number of identity maps of the same type, one for each finite subset of that
type. This makes it impossible to define a category of finite maps formally
within the Haskell type system. So maybe I should speak instead of a
semigroupoid and a semigroup of finite maps, removing both these corner cases
from consideration. The reality is that empty maps are my enemy anyway — I even
have a special function:

    dropEmpty :: (Filterable g, Foldable f) => g (f a) -> g (f a)
    dropEmpty = Witherable.filter (not . null)

— To contain their proliferation.

Of course, there are many ways an empty map may appear, such as via intersection
of maps with disjoint source sets. So some usual operations would need to
acquire more complicated types.

> 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 :-)?

I am not sure I follow you here. I see how we may model relations as sets of
tuples, but finite maps definitely need to be an abstract type of its own to
ensure that they are actually _functional_relations.

The category **Haskell** of Haskell types and total functions is not a suitable
category for these entities, because you cannot represent subsets in it, and
subsets are kinda the whole point of the exercise. So I look at it as though
**Haskell** is a subcategory of **Set** and **Finite Set** — the category of
finite sets and finite maps — is another, although not entirely disjoint
subcategory.