Fin, finite sets of natural numbers

A finite set of integers Fin n = { i :: Int16 | 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 Int16.

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

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

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

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.

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.

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

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 

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.

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 

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) 

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.

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 

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) 

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 

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.

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.

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, 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.

The inverse of plus.

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.

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 

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