Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 12
    • Merge requests 12
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Issues
  • #21
Closed
Open
Issue created Oct 04, 2018 by Robbert Krebbers@robbertkrebbersMaintainer

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.

Edited Oct 04, 2018 by Robbert Krebbers
Assignee
Assign to
Time tracking