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

[Olaf Klinke]

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.