More generic `FMap` type class that also supports collections
Currently, collection_map
, which turns a set (e.g. a gset
) with elements of type A
into a set with elements of type B
cannot be an instance of the FMap
type class. Let's take a look at the FMap
class to see why:
Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
The problem here is that M
has type Type → Type
while gset
has type ∀ (A : Type) ``{Countable A}, Type
. For most other set implementations we would have the same problem, e.g. if we were to have some kind of binary search trees, the type would be something like ∀ (A : Type) ``{TotalOrder A}, Type
.
In fact, our generic mapping operation for FinCollection
has the following type:
Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A → B) (X : C) : D :=
of_list (f <$> elements X).
I know this is also a problem in Haskell where the fmap
operation on sets (which are implemented as trees, and thus needs to have access to the order) is not an instance of the Functor
type class, so it may be worth taking a look at what they're doing.