SubHask.Category.Finite

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.

Function representations

Sparse permutations

data SparseFunction a b

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

Instances

Category * SparseFunction

type ValidCategory * SparseFunction a = FiniteType a

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

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

Generate sparse functions on some subset of the domain.

Sparse monoids

data SparseFunctionMonoid a b

Instances

Category * SparseFunctionMonoid

type ValidCategory * SparseFunctionMonoid a = (FiniteType a, Monoid a)

Dense functions

data DenseFunction a b

Represents finite functions as a hash table associating input/output value pairs.

Instances

Category * DenseFunction

type ValidCategory * DenseFunction a = FiniteType a

proveDenseFunction :: forall a b. (ValidCategory DenseFunction a, ValidCategory DenseFunction b) => (a -> b) -> DenseFunction a b

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

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

Methods

index :: a -> ZIndex a

deZIndex :: ZIndex a -> a

enumerate :: [a]

getOrder :: a -> Integer

Instances

KnownNat n => FiniteType (Z n)

data ZIndex a

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)

(Ord (Z (Order a0)), Eq (Z (Order a0))) => Ord (ZIndex a)

Read (Z (Order a0)) => Read (ZIndex a)

Show (Z (Order a0)) => Show (ZIndex a)

Arbitrary (Z (Order a0)) => Arbitrary (ZIndex a)

NFData (Z (Order a0)) => NFData (ZIndex a)

IsMutable a0 => IsMutable (ZIndex a)

Eq_ (Z (Order a0)) => Eq_ (ZIndex a)

data Mutable m (ZIndex a0) = Mutable_ZIndex (Mutable m (Z (Order a)))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Elem (ZIndex a0) = Elem (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Scalar (ZIndex a0) = Scalar (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Actor (ZIndex a0) = Actor (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))

type Logic (ZIndex a0) = Logic (Z (Order a0))