Data.Number.Fin

Newtypes of built-in numeric types for finite subsets of the natural numbers. The default implementation is the newtype of Integer, since the type-level numbers are unbounded so this is the most natural. Alternative implementations are available as nearly drop-in replacements. The reason for using modules that provide the same API, rather than using type classes or type families, is that those latter approaches introduce a lot of additional complexity for very little benefit. Using multiple different representations of finite sets in the same module seems like an uncommon use case. Albeit, this impedes writing representation-agnostic functions...

When the underlying type can only represent finitely many values, this introduces many corner cases which makes reasoning about programs more difficult. However, the main use case for these finite representations is because we know we'll only be dealing with "small" sets, so we'll never actually encounter the corner cases. Thus, this library does not try to handle the corner cases, but rather rules them out with the type system.

Many of the operations on finite sets arise from the (skeleton of the) augmented simplex category. For example, the ordinal-sum functor provides the monoidal structure of that category. For more details on the mathematics, see http://ncatlab.org/nlab/show/simplex+category.

Documentation

module Data.Number.Fin.Integer