Safe Haskell | None |
---|---|
Language | Haskell2010 |
Finite categories are categories with a finite number of arrows. In our case, this corresponds to functions with finite domains (and hence, ranges). These functions have a number of possible representations. Which is best will depend on the given function. One common property is that these functions support decidable equality.
- data SparseFunction a b
- proveSparseFunction :: (ValidCategory SparseFunction a, ValidCategory SparseFunction b, Order a ~ Order b) => (a -> b) -> SparseFunction a b
- list2sparseFunction :: (ValidCategory SparseFunction a, ValidCategory SparseFunction b, Order a ~ Order b) => [Z (Order a)] -> SparseFunction a b
- data SparseFunctionMonoid a b
- data DenseFunction a b
- proveDenseFunction :: forall a b. (ValidCategory DenseFunction a, ValidCategory DenseFunction b) => (a -> b) -> DenseFunction a b
- class KnownNat (Order a) => FiniteType a where
- data ZIndex a
Function representations
Sparse permutations
data SparseFunction a b Source
Represents finite functions as a map associating input/output pairs.
Category * SparseFunction Source | |
type ValidCategory * SparseFunction a = FiniteType a Source |
proveSparseFunction :: (ValidCategory SparseFunction a, ValidCategory SparseFunction b, Order a ~ Order b) => (a -> b) -> SparseFunction a b Source
list2sparseFunction :: (ValidCategory SparseFunction a, ValidCategory SparseFunction b, Order a ~ Order b) => [Z (Order a)] -> SparseFunction a b Source
Generate sparse functions on some subset of the domain.
Sparse monoids
data SparseFunctionMonoid a b Source
Category * SparseFunctionMonoid Source | |
type ValidCategory * SparseFunctionMonoid a = (FiniteType a, Monoid a) Source |
Dense functions
data DenseFunction a b Source
Represents finite functions as a hash table associating input/output value pairs.
Category * DenseFunction Source | |
type ValidCategory * DenseFunction a = FiniteType a Source |
proveDenseFunction :: forall a b. (ValidCategory DenseFunction a, ValidCategory DenseFunction b) => (a -> b) -> DenseFunction a b Source
Generates a dense representation of a Hask
function.
This proof will always succeed; however, if the Order
of the finite types
are very large, it may take a long time.
In that case, a SparseFunction
is probably the better representation.
Finite types
class KnownNat (Order a) => FiniteType a where Source
A type is finite if there is a bijection between it and the natural numbers. The 'index'/'deZIndex' functions implement this bijection.
KnownNat n => FiniteType (Z n) Source |
The ZIndex
class is a newtype wrapper around the natural numbers Z
.
FIXME: remove this layer; I don't think it helps