data-fin-0.1.0: Finite totally ordered sets

Data.Number.Fin.Integer

Description

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

Synopsis

# `Fin`, finite sets of natural numbers

data Fin n Source

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

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

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

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

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

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

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

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

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

The inverse of `plus`.

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