| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Arithmetic.Fin
Synopsis
- incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
- incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)
- weakenL :: forall n m. Fin n -> Fin (m + n)
- weakenR :: forall n m. Fin n -> Fin (n + m)
- ascend :: forall a n. Nat n -> a -> (Fin n -> a -> a) -> a
- ascendM :: forall m a n. Monad m => Nat n -> a -> (Fin n -> a -> m a) -> m a
- ascendM_ :: forall m a n. Applicative m => Nat n -> (Fin n -> m a) -> m ()
- ascending :: forall n. Nat n -> [Fin n]
- descending :: forall n. Nat n -> [Fin n]
- ascendingSlice :: forall n off len. Nat off -> Nat len -> ((off + len) < n) -> [Fin n]
- absurd :: Fin 0 -> void
- demote :: Fin n -> Int
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.
weakenL :: forall n m. Fin n -> Fin (m + n) Source #
Weaken the bound by one. This does not change the index.
Traverse
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)))
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
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] Source #
Generate all values of a finite set in ascending order.
>>>ascending (Nat.constant @3)[0, 1, 2]
descending :: forall n. Nat n -> [Fin n] Source #
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] Source #
Generate len values starting from off.
>>>slice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)[2, 3, 4]