Arithmetic.Fin

Modification

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

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)

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

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)

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)

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

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

ascend'

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

ascendM

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

ascendM_

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

descend

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

descend'

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

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

descendM_

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]

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]

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]

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]

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

A finite set of no values is impossible.

Demote

demote :: Fin n -> Int

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.