data-fin-0.1.1.3: Finite totally ordered sets

Portabilitynon-portable
Stabilityexperimental
Maintainerwren@community.haskell.org
Safe HaskellTrustworthy

Data.Number.Fin.Integer

Contents

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, Monad m) => Serial m (Fin n) 
(Nat n, Monad m) => CoSerial m (Fin n) 
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) 

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.

fplusSource

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