| Safe Haskell | Safe-Inferred |
|---|---|
| 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
- ascendFrom' :: forall a m n. Nat m -> Nat n -> a -> (Fin (m + n) -> a -> a) -> a
- ascendFrom'# :: forall a m n. Nat# m -> Nat# n -> a -> (Fin# (m + 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. 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 ()
- ascendM_# :: forall m a n. Monad 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
- with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a
- with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a
- construct# :: (i < n) -> Nat# i -> Fin# n
- lift :: Fin# n -> Fin n
- unlift :: Fin n -> Fin# n
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)))
Arguments
| :: forall a n. 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)))
Arguments
| :: forall a m n. Nat m | Index to start at |
| -> Nat n | Number of steps to take |
| -> a | Initial accumulator |
| -> (Fin (m + n) -> a -> a) | Update accumulator |
| -> a |
Generalization of ascend' that lets the caller pick the starting index:
ascend' === ascendFrom' 0
Arguments
| :: forall a m n. Nat# m | Index to start at |
| -> Nat# n | Number of steps to take |
| -> a | Initial accumulator |
| -> (Fin# (m + n) -> a -> a) | Update accumulator |
| -> a |
Variant of ascendFrom' with unboxed arguments.
Arguments
| :: forall m a n. 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
| :: forall m a n. Monad m | |
| => Nat# n | Upper bound |
| -> a | Initial accumulator |
| -> (Fin# n -> a -> m a) | Update accumulator |
| -> m a |
Variant of ascendM that takes an unboxed Nat and provides
an unboxed Fin to the callback.
Arguments
| :: forall m a n. 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
Variant of ascendM_ that takes an unboxed Nat and provides
an unboxed Fin to the callback.
Arguments
| :: forall a n. 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)))
Arguments
| :: forall a n. 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 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
| :: forall m a n. 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]
Absurdities
Demote
demote :: Fin n -> Int Source #
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.
Deconstruct
with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a Source #
Consume the natural number and the proof in the Fin.
with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a Source #
Variant of with for unboxed argument and result types.