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.

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

Weaken the bound by one. This does not change the index.

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

Traverse

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 differs from foldl. Roughly:

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

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

Generate all values of a finite set in ascending order.

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

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

Generate all values of a finite set in descending order.

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

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

Generate len values starting from off.

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

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.