Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

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

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

:: 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.

`>>>`

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

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

Generate all values of a finite set in descending order.

`>>>`

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

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

Generate `len`

values starting from `off`

in ascending order.

`>>>`

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

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.

`>>>`

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