Description

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.

Synopsis

# Function representations

## Sparse permutations

data SparseFunction a b Source

Represents finite functions as a map associating input/output pairs.

Instances

 Source Source

proveSparseFunction :: (ValidCategory SparseFunction a, ValidCategory SparseFunction b, Order a ~ Order b) => (a -> b) -> SparseFunction a b Source

Generates a sparse representation of a `Hask` function. This proof will always succeed, although it may be computationally expensive if the `Order` of a and b is large.

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

Instances

 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.

Instances

 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.

Associated Types

type Order a :: Nat Source

Methods

index :: a -> ZIndex a Source

deZIndex :: ZIndex a -> a Source

enumerate :: [a] Source

getOrder :: a -> Integer Source

Instances

 KnownNat n => FiniteType (Z n) Source

data ZIndex a Source

The `ZIndex` class is a newtype wrapper around the natural numbers `Z`.

FIXME: remove this layer; I don't think it helps

Instances

 Eq (Z (Order a0)) => Eq (ZIndex a) Source (Ord (Z (Order a0)), Eq (Z (Order a0))) => Ord (ZIndex a) Source Read (Z (Order a0)) => Read (ZIndex a) Source Show (Z (Order a0)) => Show (ZIndex a) Source Arbitrary (Z (Order a0)) => Arbitrary (ZIndex a) Source NFData (Z (Order a0)) => NFData (ZIndex a) Source IsMutable a0 => IsMutable (ZIndex a) Source Eq_ (Z (Order a0)) => Eq_ (ZIndex a) Source data Mutable m (ZIndex a0) = Mutable_ZIndex (Mutable m (Z (Order a))) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Elem (ZIndex a0) = Elem (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Scalar (ZIndex a0) = Scalar (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Actor (ZIndex a0) = Actor (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source type Logic (ZIndex a0) = Logic (Z (Order a0)) Source