Data.Number.Fin.Integer

A newtype of Integer for finite subsets of the natural numbers.

Fin, finite sets of natural numbers

data Fin n

A finite set of integers Fin n = { i :: Integer | 0 <= i < n } with the usual ordering. This is typed as if using the standard GADT presentation of Fin n, however it is actually implemented by a plain Integer.

If you care more about performance than mathematical accuracy, see Data.Number.Fin.Int32 for an alternative implementation as a newtype of Int32. Note, however, that doing so makes it harder to reason about code since it introduces many corner cases.

Instances

Typeable1 Fin

Nat n => Bounded (Fin n)

Nat n => Enum (Fin n)

Nat n => Eq (Fin n)

Nat n => Ord (Fin n)

Nat n => Read (Fin n)

Nat n => Show (Fin n)

Nat n => Ix (Fin n)

Nat n => Arbitrary (Fin n)

Nat n => CoArbitrary (Fin n)

Nat n => Serial (Fin n)

Nat n => UpwardEnum (Fin n)

Nat n => DownwardEnum (Fin n)

Nat n => Enum (Fin n)

Nat n => Serial (Fin n)

Showing types

showFinType :: Nat n => Fin n -> String

Like show, except it shows the type itself instead of the value.

showsFinType :: Nat n => Fin n -> ShowS

Like shows, except it shows the type itself instead of the value.

Convenience functions

minBoundOf :: Nat n => Fin n -> Integer

Return the minBound of Fin n as a plain integer. This is always zero, but is provided for symmetry with maxBoundOf.

maxBoundOf :: Nat n => Fin n -> Integer

Return the maxBound of Fin n as a plain integer. This is always n-1, but it's helpful because you may not know what n is at the time.

Introduction and elimination

toFin :: Nat n => Integer -> Maybe (Fin n)

Safely embed a number into Fin n. Use of this function will generally require an explicit type signature in order to know which n to use.

toFinProxy :: Nat n => proxy n -> Integer -> Maybe (Fin n)

Safely embed a number into Fin n. This variant of toFin uses a proxy to avoid the need for type signatures.

toFinCPS :: Integer -> (forall n. Reifies n Integer => Fin n -> r) -> Integer -> Maybe r

Safely embed integers into Fin n, where n is the first argument. We use rank-2 polymorphism to render the type-level n existentially quantified, thereby hiding the dependent type from the compiler. However, n will in fact be a skolem, so we can't provide the continuation with proof that Nat n --- unfortunately, rendering this function of little use.

 toFinCPS n k i
     | 0 <= i && i < n  = Just (k i)  -- morally speaking...
     | otherwise        = Nothing

fromFin :: Nat n => Fin n -> Integer

Extract the value of a Fin n.

N.B., if somehow the Fin n value was constructed invalidly, then this function will throw an exception. However, this should never happen. If it does, contact the maintainer since this indicates a bug/insecurity in this library.

Views and coersions

Weakening and maximum views

weaken :: Succ m n => Fin m -> Fin n

Embed a finite domain into the next larger one, keeping the same position relative to minBound. That is,

 fromFin (weaken x) == fromFin x

The opposite of this function is maxView.

 maxView . weaken                == Just
 maybe maxBound weaken . maxView == id

weakenLE :: NatLE m n => Fin m -> Fin n

A variant of weaken which allows weakening the type by multiple steps. Use of this function will generally require an explicit type signature in order to know which n to use.

The opposite of this function is maxViewLE. When the choice of m and n is held constant, we have that:

 maxViewLE . weakenLE      == Just
 fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)

weakenPlus :: Add m n o => Fin m -> Fin o

A type-signature variant of weakenLE because we cannot automatically deduce that Add m n o ==> NatLE m o. This is the left half of plus.

maxView :: Succ m n => Fin n -> Maybe (Fin m)

The maximum-element view. This strengthens the type by removing the maximum element:

 maxView maxBound = Nothing
 maxView x        = Just x  -- morally speaking...

The opposite of this function is weaken.

 maxView . weaken                == Just
 maybe maxBound weaken . maxView == id

maxViewLE :: NatLE m n => Fin n -> Maybe (Fin m)

A variant of maxView which allows strengthening the type by multiple steps. Use of this function will generally require an explicit type signature in order to know which m to use.

The opposite of this function is weakenLE. When the choice of m and n is held constant, we have that:

 maxViewLE . weakenLE      == Just
 fmap weakenLE . maxViewLE == (\i -> if i < m then Just i else Nothing)

Widening and the predecessor view

widen :: Succ m n => Fin m -> Fin n

Embed a finite domain into the next larger one, keeping the same position relative to maxBound. That is, we shift everything up by one:

 fromFin (widen x) == 1 + fromFin x

The opposite of this function is predView.

 predView . widen         == Just
 maybe 0 widen . predView == id

widenLE :: NatLE m n => Fin m -> Fin n

Embed a finite domain into any larger one, keeping the same position relative to maxBound. That is,

 maxBoundOf y - fromFin y == maxBoundOf x - fromFin x
     where y = widenLE x

Use of this function will generally require an explicit type signature in order to know which n to use.

widenPlus :: Add m n o => Fin n -> Fin o

A type-signature variant of widenLE because we cannot automatically deduce that Add m n o ==> NatLE n o. This is the right half of plus.

predView :: Succ m n => Fin n -> Maybe (Fin m)

The predecessor view. This strengthens the type by shifting everything down by one:

 predView 0 = Nothing
 predView x = Just (x-1)  -- morally speaking...

The opposite of this function is widen.

 predView . widen         == Just
 maybe 0 widen . predView == id

The ordinal-sum functor

plus :: Add m n o => Either (Fin m) (Fin n) -> Fin o

The ordinal-sum functor, on objects. This internalizes the disjoint union, mapping Fin m + Fin n into Fin(m+n) by placing the image of the summands next to one another in the codomain, thereby preserving the structure of both summands.

unplus :: Add m n o => Fin o -> Either (Fin m) (Fin n)

The inverse of plus.

fplus

Arguments

:: (Add m n o, Add m' n' o')

=> (Fin m -> Fin m')

The left morphism

-> (Fin n -> Fin n')

The right morphism

-> Fin o -> Fin o'

The ordinal-sum functor, on morphisms. If we view the maps as bipartite graphs, then the new map is the result of placing the left and right maps next to one another. This is similar to (+++) from Control.Arrow.

Face- and degeneracy-maps

thin :: Succ m n => Fin n -> Fin m -> Fin n

The "face maps" for Fin viewed as the standard simplices (aka: the thinning view). Traditionally spelled with delta or epsilon. For each i, it is the unique injective monotonic map that skips i. That is,

 thin i = (\j -> if j < i then j else succ j)  -- morally speaking...

Which has the important universal property that:

 thin i j /= i

thick :: Succ m n => Fin m -> Fin n -> Fin m

The "degeneracy maps" for Fin viewed as the standard simplices. Traditionally spelled with sigma or eta. For each i, it is the unique surjective monotonic map that covers i twice. That is,

 thick i = (\j -> if j <= i then j else pred j)  -- morally speaking...

Which has the important universal property that:

 thick i (i+1) == i