
9 Jan
2021
9 Jan
'21
7:12 a.m.
On Sat, Jan 09 2021 16:30, Ignat Insarov wrote:
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.
Finite maps from `"containers" Data.Map` look like they may form a Cartesian closed category.
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 :-)?