Map operation class

[JamesGallicchio]

Functor only applies to type constructors (Type u -> Type v). So, is insufficient for a general purpose map : (A -> B) -> CA -> CB where perhaps CA and CB cannot contain arbitrary element types.

Example: Functor ByteArray does not typecheck, even though we can give map : (Byte -> Byte) -> ByteArray -> ByteArray

Suggested implementation:

class Map (C : Type w) (τ : Type x) (C' : Type y) (τ' : Type z) where
  map : (f : τ → τ') → C → C'

This conflicts with the current Map class (which is the bag of associations abstraction commonly called a Map in other languages).

We could

1. Name the new class MapOp? Since we will export MapOp (map) it will still be visible, but with the current naming scheme, theorems about map will end up in the MapOp.theorems_about_map namespace.
2. Rename current Map to MapBag or similar. I don't .. hate this solution? because it emphasizes the class's relationship to Bag, but this goes against other languages with interfaces named Map.

[JamesGallicchio]

I haven't yet checked what Haskell libraries do. Could be a useful source.

[sullyj3]

What about Dict or Dictionary?

[JamesGallicchio]

Gonna wait until the 4.8 release to add a Map class, so the deprecation notice sticks around for at least a little while.