refined-containers

Type-checked proof that a key exists in a container and can be safely indexed.

Stackage Nightly 2025-04-03:	0.1.2.0
Latest on Hackage:	0.1.2.0

See all snapshots refined-containers appears in

MIT licensed and maintained by

This version can be pinned in stack with:refined-containers-0.1.2.0@sha256:d62e84122ef8ffe55c5074562b73f6a27b09a44be52bdcde278e6f0366d0c646,3057

Module documentation for 0.1.2.0

Data
- Data.HashMap
  - Data.HashMap.Refined
  - Data.HashMap.Strict
    - Data.HashMap.Strict.Refined
- Data.HashSet
  - Data.HashSet.Refined
- Data.IntMap
  - Data.IntMap.Refined
  - Data.IntMap.Strict
    - Data.IntMap.Strict.Refined
- Data.IntSet
  - Data.IntSet.Refined
- Data.Map
  - Data.Map.Refined
  - Data.Map.Strict
    - Data.Map.Strict.Refined
- Data.Set
  - Data.Set.Refined

Depends on 12 packages(full list with versions):

adjunctions, base, constraints, containers, deepseq, distributive, hashable, indexed-traversable, mtl, refined, reflection, unordered-containers

This package defines ways to prove that a key exists in an associative container such as a Map, IntMap, or HashMap; so that the key can be used to index into the map without a Maybe or manually handling the "impossible" case with error or other partial functions.

To do this, the containers are tagged with a type parameter that identifies their set of keys, so that if you have another container with the same parameter, you know it has the same keys.

There is also a type of keys that have been proven to exist in such containers -- a refinement type. They are also tagged with a type parameter. If the type parameter of the key matches that of the container, indexing is guaranteed to proceed without failure.