parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2022
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.FinMap

Description

``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.

# Documentation

module Data.Parameterized.FinMap.Unsafe