@hackage / refined-containers

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

Latest0.1.2.0

About

Metadata

  • Last updated , by mniip
  • License MIT
  • Maintained by: mniip@typeable.io

  • Lottery factor: 1

Links

Installation

Tested Compilers

  1. 9.12.1
  2. 9.10.1
  3. 9.8.2
  4. 9.6.6
  5. 9.4.8
  6. 9.2.8
  7. 9.0.2
  8. 8.10.7
  9. 8.6.5

Readme

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.