Thanks Tom! This is not a complete disaster theoretically, because a `mempty` map corresponds to a function with `Void` domain which may not be invoked anyway. But truly it makes the definition problematic, in the way similar to how `Set` is not quite a functor — usually it works but sometimes _map g ∘ map f_ may lose more elements than _map (g ∘ f)_. I am not sure how much of sad I should be about it. The function still works most of the time.

...

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.

Wow, this blew up overnight. Thank you Olaf and allies for attending to this topic. But I think there is a hidden mismatch of premises. So let me take a step back and look at things again, in order, from the ground up.

Hi Ignat, would you slow down a bit and tell us the idea behind your question?

You seem to expect Map forms a Cartesian closed category, and want to know if the specific property of CCC holds ("functors of shape (a ⇸ -) are distributive".)

Could you explain that expectation step-by-step? For the first step, let us know the category made from Maps more clearly. I mean, (1) what are the objects of that category? (2) what are the morphisms? (3) how the identity morphisms and the composition of morphisms are defined?

The next step would be the "Cartesian" part. This category should have direct product of any finite number of objects. What exactly are these, and how do you define the projection morphisms (equivalents of `fst` and `snd` in your category) and the product of morphisms (equivalent of `&&&`.)

It's too rushed to think about CCC until these aren't clear.

This is most fair. Being a software engineer and not a mathematician, I was hoping to avoid the scrutiny into what I was taking to be an accepted base line. It did not play out as I hoped, so let us rewind. As I offered previously:

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.

I take **Finite Set** to be Cartesian closed with the same product and exponent objects as its supercategory **Set**. Objections? None, excellent. Now to the mentioned mismatch. There are two philosophies: 1. Let us model perfect Mathematics in an imperfect programming language as best we can. 2. Let us have only as much Mathematics as we can so our programming language remains perfect. I employ the approach №1 here. Also, I already have a good idea of what I want to do, and I already have code that works. This makes proofs of non-existence somewhat less effective, in the sense that they cannot discourage me from exploring the matter. If the idea cannot work, I need to know in what cases it _does_ work. Actually, I find the idea that finite sets and functions may be represented in Haskell very attractive in general, so I think it is worth the effort to realize it in Haskell possibly better, even if perfect realization is unattainable _(and it is)_. That is not to say that I am going to ignore all objections. But I do want to recover as much as can be recovered. If not a category, maybe a semigroupoid? If not a monoid, maybe a semigroup? If we cannot model it in types, can we still use it with imaginary proofs? Maybe we can use a clever normalization to exclude pathologies? And so on. 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. ## Now to the technical details. We do not have subtypes in Haskell, but we do have subsets and finite maps — it is only that the type system does not know which subsets and finite maps are compatible. So, we depart from the category **Haskell** of types and total functions, and we allow instead that some values may be objects in our category **X** — notably the values of type `Set α`. * Now a function may be restricted to a finite set via `fromSet ∷ (k → a) → Set k → Map k a`, so there are arrows in **X** for every pair of an arrow of **Haskell** and a finite subset of an object of **Haskell** that has a total ordering _(or even mere decidable equality if we may sacrifice performance)_. * An identity arrow for a given finite set is then a restriction of `id` to that set. * Finite maps compose when the domain of one subsumes the range of the other via `fmap (g !) f`. * Terminal object is the unique singleton of type `Set ( )` or any uniquely isomorphic singleton of a type with a single nullary constructor. * The product of two finite sets is given by `cartesianProduct`, and projections are the appropriate restrictions of the usual `fst` and `snd`. * The exponential object is a finite set of all maps with the same domain and range. I went on and invented the definitions witnessing the requisite isomorphose: curry = mapKeysWith union fst ∘ mapWithKey (singleton ∘ snd) uncurry = unions ∘ mapWithKey (mapKeys ∘ (, )) They pass any example except the one Tom gave earlier, with an empty map. This establishes a Cartesian closed category of somewhat idealized entities. Can the realization of this category in Haskell be perfected to exclude pathologies by construction? Perhaps it is enough to normalize maps with `dropEmpty` before comparison? Seems worth some research.