On Mon, 2021-01-25 at 18:36 +0500, Ignat Insarov wrote:
Hello Olaf and everyone.
This is awesome code, much more crisp than what I have been drafting. It highlights that we need to roll out our own dynamic type system to track that the domains of finite maps match where they should.
I find it amusing and useful that we can have _«ragged»_ binary maps and currying still works in the absence of empty maps. Why that? There is Data.Map.empty and it represents any f `restrictedTo` Set.empty
So there is some space for future work — for instance, maybe non-trivial equality may remove this flaw. Other than that, I think the question is clarified! You could explore the design space of subtypes a bit further and let us know how it goes. For example, is FiniteFunction a b = (Set a, a -> b) feasible? Would TypeLevelNats be useful? What about (Set a, a -> b) where Set is a functor of subsets, such as in the infinite-search [*] package? For the special case where type a is a record, there is the records-sop package which has a binary IsSubTypeOf type relation.
Olaf [*] For any Eq type, the subsets that admit infinite search are finite.