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.