natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Arithmetic.Fin

Synopsis

Modification

incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n) Source #

Raise the index by m and weaken the bound by m, adding m to the left-hand side of n.

incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m) Source #

Raise the index by m and weaken the bound by m, adding m to the right-hand side of n.

weaken :: forall n m. (n <= m) -> Fin n -> Fin m Source #

Weaken the bound, replacing it by another number greater than or equal to itself. This does not change the index.

weakenL :: forall n m. Fin n -> Fin (m + n) Source #

Weaken the bound by m, adding it to the left-hand side of the existing bound. This does not change the index.

weakenR :: forall n m. Fin n -> Fin (n + m) Source #

Weaken the bound by m, adding it to the right-hand side of the existing bound. This does not change the index.

Traverse

These use the terms ascend and descend rather than the more popular l (left) and r (right) that pervade the Haskell ecosystem. The general rule is that ascending functions pair the initial accumulator with zero with descending functions pair the initial accumulator with the last index.

ascend :: forall a n. Nat n -> a -> (Fin n -> a -> a) -> a Source #

Fold over the numbers bounded by n in ascending order. This is lazy in the accumulator.

ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))

Arguments

 :: Nat n Upper bound -> a Initial accumulator -> (Fin n -> a -> a) Update accumulator -> a

Strict fold over the numbers bounded by n in ascending order. For convenince, this differs from foldl' in the order of the parameters.

ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))

Arguments

 :: Monad m => Nat n Upper bound -> a Initial accumulator -> (Fin n -> a -> m a) Update accumulator -> m a

Strict monadic left fold over the numbers bounded by n in ascending order. Roughly:

ascendM 4 z0 f =
f 0 z0 >>= \z1 ->
f 1 z1 >>= \z2 ->
f 2 z2 >>= \z3 ->
f 3 z3

Arguments

 :: Applicative m => Nat n Upper bound -> (Fin n -> m a) Effectful interpretion -> m ()

Monadic traversal of the numbers bounded by n in ascending order.

ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3

Arguments

 :: Nat n Upper bound -> a Initial accumulator -> (Fin n -> a -> a) Update accumulator -> a

Fold over the numbers bounded by n in descending order. This is lazy in the accumulator. For convenince, this differs from foldr in the order of the parameters.

descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))

Arguments

 :: Nat n Upper bound -> a Initial accumulator -> (Fin n -> a -> a) Update accumulator -> a

Fold over the numbers bounded by n in descending order. This is strict in the accumulator. For convenince, this differs from foldr' in the order of the parameters.

descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))

descendM :: forall m a n. Monad m => Nat n -> a -> (Fin n -> a -> m a) -> m a Source #

Strict monadic left fold over the numbers bounded by n in descending order. Roughly:

descendM 4 z f =
f 3 z0 >>= \z1 ->
f 2 z1 >>= \z2 ->
f 1 z2 >>= \z3 ->
f 0 z3

Arguments

 :: Applicative m => Nat n Upper bound -> (Fin n -> m a) Effectful interpretion -> m ()

Monadic traversal of the numbers bounded by n in descending order.

descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0

ascending :: forall n. Nat n -> [Fin n] Source #

Generate all values of a finite set in ascending order.

>>> ascending (Nat.constant @3)
[Fin 0,Fin 1,Fin 2]

descending :: forall n. Nat n -> [Fin n] Source #

Generate all values of a finite set in descending order.

>>> descending (Nat.constant @3)
[Fin 2,Fin 1,Fin 0]

ascendingSlice :: forall n off len. Nat off -> Nat len -> ((off + len) <= n) -> [Fin n] Source #

Generate len values starting from off in ascending order.

>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)
[Fin 2,Fin 3,Fin 4]

descendingSlice :: forall n off len. Nat off -> Nat len -> ((off + len) <= n) -> [Fin n] Source #

Generate len values starting from 'off + len - 1' in descending order.

>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)
[Fin 4,Fin 3,Fin 2]

Absurdities

absurd :: Fin 0 -> void Source #

A finite set of no values is impossible.

Demote

demote :: Fin n -> Int Source #

Extract the Int from a 'Fin n'. This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.