| 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)
- weaken :: forall n m. (n <= m) -> Fin n -> Fin 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
- 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 ()
- descend :: forall a n. Nat n -> a -> (Fin n -> a -> a) -> a
- descend' :: forall a n. Nat n -> a -> (Fin n -> a -> a) -> a
- descendM :: forall m a n. Monad m => Nat n -> a -> (Fin n -> a -> m a) -> m a
- descendM_ :: 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]
- descendingSlice :: 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.
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)))
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
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)))
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]