License | BSD-style |
---|---|
Maintainer | Vincent Hanquez <vincent@snarc.org> |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Basement.Sized.List
Contents
Description
A Nat-sized list abstraction
Using this module is limited to GHC 7.10 and above.
Synopsis
- data ListN (n :: Nat) a
- toListN :: forall (n :: Nat) a. (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
- toListN_ :: forall (n :: Nat) a. (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
- unListN :: ListN n a -> [a]
- length :: forall a (n :: Nat). (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
- create :: forall a (n :: Nat). KnownNat n => (Natural -> a) -> ListN n a
- createFrom :: forall a (n :: Nat) (start :: Nat). (KnownNat n, KnownNat start) => Proxy start -> (Natural -> a) -> ListN n a
- empty :: ListN 0 a
- singleton :: a -> ListN 1 a
- uncons :: forall (n :: Natural) a. 1 <= n => ListN n a -> (a, ListN (n - 1) a)
- cons :: forall a (n :: Nat). a -> ListN n a -> ListN (n + 1) a
- unsnoc :: forall (n :: Natural) a. 1 <= n => ListN n a -> (ListN (n - 1) a, a)
- snoc :: forall (n :: Nat) a. ListN n a -> a -> ListN (n + 1) a
- index :: forall (n :: Nat) ty. ListN n ty -> Offset ty -> ty
- indexStatic :: forall (i :: Nat) (n :: Natural) a. (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
- updateAt :: forall (n :: Nat) a. Offset a -> (a -> a) -> ListN n a -> ListN n a
- map :: forall a b (n :: Nat). (a -> b) -> ListN n a -> ListN n b
- mapi :: forall a b (n :: Nat). (Natural -> a -> b) -> ListN n a -> ListN n b
- elem :: forall a (n :: Nat). Eq a => a -> ListN n a -> Bool
- foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
- foldl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b
- foldl1' :: forall (n :: Natural) a. 1 <= n => (a -> a -> a) -> ListN n a -> a
- scanl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b
- scanl1' :: forall a (n :: Nat). (a -> a -> a) -> ListN n a -> ListN n a
- foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> ListN n a -> b
- foldr1 :: forall (n :: Natural) a. 1 <= n => (a -> a -> a) -> ListN n a -> a
- reverse :: forall (n :: Nat) a. ListN n a -> ListN n a
- append :: forall (n :: Nat) a (m :: Nat). ListN n a -> ListN m a -> ListN (n + m) a
- minimum :: forall a (n :: Natural). (Ord a, 1 <= n) => ListN n a -> a
- maximum :: forall a (n :: Natural). (Ord a, 1 <= n) => ListN n a -> a
- head :: forall (n :: Natural) a. 1 <= n => ListN n a -> a
- tail :: forall (n :: Natural) a. 1 <= n => ListN n a -> ListN (n - 1) a
- init :: forall (n :: Natural) a. 1 <= n => ListN n a -> ListN (n - 1) a
- take :: forall a (m :: Nat) (n :: Nat). (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
- drop :: forall a (d :: Nat) (m :: Nat) (n :: Nat). (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
- splitAt :: forall a (d :: Nat) (m :: Nat) (n :: Nat). (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (n - m) a)
- zip :: forall (n :: Nat) a b. ListN n a -> ListN n b -> ListN n (a, b)
- zip3 :: forall (n :: Nat) a b c. ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c)
- zip4 :: forall (n :: Nat) a b c d. ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d)
- zip5 :: forall (n :: Nat) a b c d e. ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a, b, c, d, e)
- unzip :: forall (n :: Nat) a b. ListN n (a, b) -> (ListN n a, ListN n b)
- zipWith :: forall a b x (n :: Nat). (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
- zipWith3 :: forall a b c x (n :: Nat). (a -> b -> c -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n x
- zipWith4 :: forall a b c d x (n :: Nat). (a -> b -> c -> d -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
- zipWith5 :: forall a b c d e x (n :: Nat). (a -> b -> c -> d -> e -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n x
- replicate :: forall (n :: Nat) a. (NatWithinBound Int n, KnownNat n) => a -> ListN n a
- replicateM :: forall (n :: Nat) m a. (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
- sequence :: forall m (n :: Nat) a. Monad m => ListN n (m a) -> m (ListN n a)
- sequence_ :: forall m (n :: Nat) a. Monad m => ListN n (m a) -> m ()
- mapM :: forall m a b (n :: Nat). Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
- mapM_ :: forall m a b (n :: Nat). Monad m => (a -> m b) -> ListN n a -> m ()
Documentation
data ListN (n :: Nat) a Source #
A Typed-level sized List equivalent to [a]
Instances
Generic (ListN n a) Source # | |||||
Defined in Basement.Sized.List Associated Types
| |||||
Show a => Show (ListN n a) Source # | |||||
NormalForm a => NormalForm (ListN n a) Source # | |||||
Defined in Basement.Sized.List Methods toNormalForm :: ListN n a -> () Source # | |||||
Eq a => Eq (ListN n a) Source # | |||||
Ord a => Ord (ListN n a) Source # | |||||
type Rep (ListN n a) Source # | |||||
Defined in Basement.Sized.List |
toListN :: forall (n :: Nat) a. (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a) Source #
Try to create a ListN from a List, succeeding if the length is correct
toListN_ :: forall (n :: Nat) a. (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a Source #
Create a ListN from a List, expecting a given length
If this list contains more or less than the expected length of the resulting type,
then an asynchronous error is raised. use toListN
for a more friendly functions
length :: forall a (n :: Nat). (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a Source #
Get the length of a list
create :: forall a (n :: Nat). KnownNat n => (Natural -> a) -> ListN n a Source #
Create a new list of size n, repeately calling f from 0 to n-1
createFrom :: forall a (n :: Nat) (start :: Nat). (KnownNat n, KnownNat start) => Proxy start -> (Natural -> a) -> ListN n a Source #
Same as create but apply an offset
uncons :: forall (n :: Natural) a. 1 <= n => ListN n a -> (a, ListN (n - 1) a) Source #
Decompose a list into its head and tail.
cons :: forall a (n :: Nat). a -> ListN n a -> ListN (n + 1) a Source #
prepend an element to the list
unsnoc :: forall (n :: Natural) a. 1 <= n => ListN n a -> (ListN (n - 1) a, a) Source #
Decompose a list into its first elements and the last.
snoc :: forall (n :: Nat) a. ListN n a -> a -> ListN (n + 1) a Source #
append an element to the list
indexStatic :: forall (i :: Nat) (n :: Natural) a. (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a Source #
Get the i'th elements
This only works with TypeApplication:
indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
updateAt :: forall (n :: Nat) a. Offset a -> (a -> a) -> ListN n a -> ListN n a Source #
Update the value in a list at a specific location
mapi :: forall a b (n :: Nat). (Natural -> a -> b) -> ListN n a -> ListN n b Source #
Map all elements in a list with an additional index
elem :: forall a (n :: Nat). Eq a => a -> ListN n a -> Bool Source #
Check if a list contains the element a
foldl :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b Source #
Fold all elements from left
foldl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> b Source #
Fold all elements from left strictly
foldl1' :: forall (n :: Natural) a. 1 <= n => (a -> a -> a) -> ListN n a -> a Source #
Fold all elements from left strictly with a first element as the accumulator
scanl' :: forall b a (n :: Nat). (b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b Source #
scanl
is similar to foldl
, but returns a list of successive
reduced values from the left
scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
scanl1' :: forall a (n :: Nat). (a -> a -> a) -> ListN n a -> ListN n a Source #
scanl1
is a variant of scanl
that has no starting value argument:
scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
foldr :: forall a b (n :: Nat). (a -> b -> b) -> b -> ListN n a -> b Source #
Fold all elements from right
foldr1 :: forall (n :: Natural) a. 1 <= n => (a -> a -> a) -> ListN n a -> a Source #
Fold all elements from right assuming at least one element is in the list.
append :: forall (n :: Nat) a (m :: Nat). ListN n a -> ListN m a -> ListN (n + m) a Source #
Append 2 list together returning the new list
minimum :: forall a (n :: Natural). (Ord a, 1 <= n) => ListN n a -> a Source #
Get the minimum element of a list
maximum :: forall a (n :: Natural). (Ord a, 1 <= n) => ListN n a -> a Source #
Get the maximum element of a list
tail :: forall (n :: Natural) a. 1 <= n => ListN n a -> ListN (n - 1) a Source #
Get the tail of a list
init :: forall (n :: Natural) a. 1 <= n => ListN n a -> ListN (n - 1) a Source #
Get the list with the last element missing
take :: forall a (m :: Nat) (n :: Nat). (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a Source #
Take m elements from the beggining of the list.
The number of elements need to be less or equal to the list in argument
drop :: forall a (d :: Nat) (m :: Nat) (n :: Nat). (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a Source #
Drop elements from a list keeping the m remaining elements
splitAt :: forall a (d :: Nat) (m :: Nat) (n :: Nat). (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (n - m) a) Source #
Split a list into two, returning 2 lists
zip :: forall (n :: Nat) a b. ListN n a -> ListN n b -> ListN n (a, b) Source #
Zip 2 lists of the same size, returning a new list of the tuple of each elements
zip3 :: forall (n :: Nat) a b c. ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c) Source #
Zip 3 lists of the same size
zip4 :: forall (n :: Nat) a b c d. ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d) Source #
Zip 4 lists of the same size
zip5 :: forall (n :: Nat) a b c d e. ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a, b, c, d, e) Source #
Zip 5 lists of the same size
unzip :: forall (n :: Nat) a b. ListN n (a, b) -> (ListN n a, ListN n b) Source #
Unzip a list of tuple, to 2 List of the deconstructed tuples
zipWith :: forall a b x (n :: Nat). (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x Source #
Zip 2 lists using a function
zipWith3 :: forall a b c x (n :: Nat). (a -> b -> c -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n x Source #
Zip 3 lists using a function
zipWith4 :: forall a b c d x (n :: Nat). (a -> b -> c -> d -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x Source #
Zip 4 lists using a function
zipWith5 :: forall a b c d e x (n :: Nat). (a -> b -> c -> d -> e -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n x Source #
Zip 5 lists using a function
replicate :: forall (n :: Nat) a. (NatWithinBound Int n, KnownNat n) => a -> ListN n a Source #
Create a list of n elements where each element is the element in argument
Applicative And Monadic
replicateM :: forall (n :: Nat) m a. (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a) Source #
performs a monadic action n times, gathering the results in a List of size n.
sequence :: forall m (n :: Nat) a. Monad m => ListN n (m a) -> m (ListN n a) Source #
Evaluate each monadic action in the list sequentially, and collect the results.
sequence_ :: forall m (n :: Nat) a. Monad m => ListN n (m a) -> m () Source #
Evaluate each monadic action in the list sequentially, and ignore the results.