[Haskell-cafe] A quick question about distribution of finite maps.
Olaf Klinke
olf at aatal-apotheke.de
Tue Jan 26 06:16:18 UTC 2021
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.
More information about the Haskell-Cafe
mailing list