FinMap n a conceptually (see NOTE) a map with Fin n keys, implying a maximum size of n. Here's how FinMap compares to other map-like types:

• FinMap n a is conceptually isomorphic to a Vector n (Maybe a), but can be more space-efficient especially if n is large and the vector is populated with a small number of Just values.
• FinMap is less general than Map, because it has a fixed key type (Fin n).
• FinMap n a is similar to IntMap a, but it provides a static guarantee of a maximum size, and its operations (such as size) allow the recovery of more type-level information.
• FinMap is dissimilar from Data.Parameterized.Map.MapF in that neither the key nor value type of FinMap is parameterized.

The type parameter n doesn't track the current number of key-value pairs in a FinMap n (i.e., the size of the map), but rather an upper bound. insert and delete don't alter n, whereas incMax does - despite the fact that it has no effect on the keys and values in the FinMap.

The FinMap interface has two implementations:

• The implementation in Data.Parameterized.FinMap.Unsafe is backed by an IntMap, and must have a size of at most maxBound :: Int. This module uses unsafe operations like unsafeCoerce internally for the sake of time and space efficiency.
• The implementation in Data.Parameterized.FinMap.Safe is backed by an Map (Fin n). All of its functions are implemented using safe operations.

The implementation in FinMap is property tested against that in FinMap to ensure they have the same behavior.

In this documentation, W is used in big-O notations the same way as in the Data.IntMap documentation.

NOTE: Where the word "conceptually" is used, it implies that this correspondence is not literally true, but is true modulo some details such as differences between bounded types like Int and unbounded types like Integer.

Several of the functions in both implementations are marked INLINE or INLINABLE. There are three reasons for this:

• Some of these just have very small definitions and so inlining is likely more beneficial than harmful.
• Some participate in RULES relevant to functions used in their implementations.
• They are thin wrappers (often just newtype wrappers) around functions marked INLINE, which should therefore also be inlined.