Portability | non-portable |
---|---|

Stability | experimental |

Maintainer | wren@community.haskell.org |

Safe Haskell | Trustworthy |

A newtype of `Integer`

for finite subsets of the natural numbers.

- data Fin n
- showFinType :: Nat n => Fin n -> String
- showsFinType :: Nat n => Fin n -> ShowS
- minBoundOf :: Nat n => Fin n -> Integer
- maxBoundOf :: Nat n => Fin n -> Integer
- toFin :: Nat n => Integer -> Maybe (Fin n)
- toFinProxy :: Nat n => proxy n -> Integer -> Maybe (Fin n)
- toFinCPS :: Integer -> (forall n. Reifies n Integer => Fin n -> r) -> Integer -> Maybe r
- fromFin :: Nat n => Fin n -> Integer
- weaken :: Succ m n => Fin m -> Fin n
- weakenLE :: NatLE m n => Fin m -> Fin n
- weakenPlus :: Add m n o => Fin m -> Fin o
- maxView :: Succ m n => Fin n -> Maybe (Fin m)
- maxViewLE :: NatLE m n => Fin n -> Maybe (Fin m)
- widen :: Succ m n => Fin m -> Fin n
- widenLE :: NatLE m n => Fin m -> Fin n
- widenPlus :: Add m n o => Fin n -> Fin o
- predView :: Succ m n => Fin n -> Maybe (Fin m)
- plus :: Add m n o => Either (Fin m) (Fin n) -> Fin o
- unplus :: Add m n o => Fin o -> Either (Fin m) (Fin n)
- fplus :: (Add m n o, Add m' n' o') => (Fin m -> Fin m') -> (Fin n -> Fin n') -> Fin o -> Fin o'
- thin :: Succ m n => Fin n -> Fin m -> Fin n
- thick :: Succ m n => Fin m -> Fin n -> Fin m

`Fin`

, finite sets of natural numbers

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.

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 -> StringSource

Like `show`

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

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

Like `shows`

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

## Convenience functions

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

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 -> IntegerSource

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)Source

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)Source

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 rSource

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 -> IntegerSource

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

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

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 oSource

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

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)Source

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

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

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.

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

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 oSource

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.

:: (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 nSource

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 mSource

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