License	BSD-style
Maintainer	Vincent Hanquez <vincent@snarc.org>
Stability	experimental
Portability	portable
Safe Haskell	None
Language	Haskell2010

Basement.Sized.List

Contents

Applicative And Monadic

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 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 :: 1 <= n => ListN n a -> (a, ListN (n - 1) a)
cons :: a -> ListN n a -> ListN (n + 1) a
unsnoc :: 1 <= n => ListN n a -> ( ListN (n - 1) a, a)
snoc :: ListN n a -> a -> ListN (n + 1) a
index :: ListN n ty -> Offset ty -> ty
indexStatic :: forall i n a. ( KnownNat i, CmpNat i n ~ ' LT , Offsetable a i) => ListN n a -> a
updateAt :: forall n a. Offset a -> (a -> a) -> ListN n a -> ListN n a
map :: (a -> b) -> ListN n a -> ListN n b
mapi :: ( Natural -> a -> b) -> ListN n a -> ListN n b
elem :: Eq a => a -> ListN n a -> Bool
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl' :: (b -> a -> b) -> b -> ListN n a -> b
foldl1' :: 1 <= n => (a -> a -> a) -> ListN n a -> a
scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n + 1) b
scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr1 :: 1 <= n => (a -> a -> a) -> ListN n a -> a
reverse :: ListN n a -> ListN n a
append :: ListN n a -> ListN m a -> ListN (n + m) a
minimum :: ( Ord a, 1 <= n) => ListN n a -> a
maximum :: ( Ord a, 1 <= n) => ListN n a -> a
head :: 1 <= n => ListN n a -> a
tail :: 1 <= n => ListN n a -> ListN (n - 1) a
init :: 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 (m :: Nat ) (n :: Nat ). ( KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
splitAt :: forall a d (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 :: ListN n a -> ListN n b -> ListN n (a, b)
zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c)
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a, b, c, d)
zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a, b, c, d, e)
unzip :: ListN n (a, b) -> ( ListN n a, ListN n b)
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith3 :: (a -> b -> c -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n x
zipWith4 :: (a -> b -> c -> d -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n x
zipWith5 :: (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 :: Monad m => ListN n (m a) -> m ( ListN n a)
sequence_ :: Monad m => ListN n (m a) -> m ()
mapM :: Monad m => (a -> m b) -> ListN n a -> m ( ListN n b)
mapM_ :: 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

Instances details

Eq a => Eq ( ListN n a) Source #
Instance details Defined in Basement.Sized.List Methods (==) :: ListN n a -> ListN n a -> Bool Source # (/=) :: ListN n a -> ListN n a -> Bool Source #
Ord a => Ord ( ListN n a) Source #
Instance details Defined in Basement.Sized.List Methods compare :: ListN n a -> ListN n a -> Ordering Source # (<) :: ListN n a -> ListN n a -> Bool Source # (<=) :: ListN n a -> ListN n a -> Bool Source # (>) :: ListN n a -> ListN n a -> Bool Source # (>=) :: ListN n a -> ListN n a -> Bool Source # max :: ListN n a -> ListN n a -> ListN n a Source # min :: ListN n a -> ListN n a -> ListN n a Source #
Show a => Show ( ListN n a) Source #
Instance details Defined in Basement.Sized.List Methods showsPrec :: Int -> ListN n a -> ShowS Source # show :: ListN n a -> String Source # showList :: [ ListN n a] -> ShowS Source #
Generic ( ListN n a) Source #
Instance details Defined in Basement.Sized.List Associated Types type Rep ( ListN n a) :: Type -> Type Source # Methods from :: ListN n a -> Rep ( ListN n a) x Source # to :: Rep ( ListN n a) x -> ListN n a Source #
NormalForm a => NormalForm ( ListN n a) Source #
Instance details Defined in Basement.Sized.List Methods toNormalForm :: ListN n a -> () Source #
type Rep ( ListN n a) Source #
Instance details Defined in Basement.Sized.List type Rep ( ListN n a) = D1 (' MetaData "ListN" "Basement.Sized.List" "basement-0.0.15-6RkaeFQt65GF50at0tox6w" ' True ) ( C1 (' MetaCons "ListN" ' PrefixI ' True ) ( S1 (' MetaSel (' Just "unListN") ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 [a])))

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

unListN :: ListN n a -> [a] Source #

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

empty :: ListN 0 a Source #

Create an empty list of a

singleton :: a -> ListN 1 a Source #

create a list of 1 element

uncons :: 1 <= n => ListN n a -> (a, ListN (n - 1) a) Source #

Decompose a list into its head and tail.

cons :: a -> ListN n a -> ListN (n + 1) a Source #

prepend an element to the list

unsnoc :: 1 <= n => ListN n a -> ( ListN (n - 1) a, a) Source #

Decompose a list into its first elements and the last.

snoc :: ListN n a -> a -> ListN (n + 1) a Source #

append an element to the list

index :: ListN n ty -> Offset ty -> ty Source #

Get the i'the element

indexStatic :: forall i n 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 a. Offset a -> (a -> a) -> ListN n a -> ListN n a Source #

Update the value in a list at a specific location

map :: (a -> b) -> ListN n a -> ListN n b Source #

Map all elements in a list

mapi :: ( Natural -> a -> b) -> ListN n a -> ListN n b Source #

Map all elements in a list with an additional index

elem :: Eq a => a -> ListN n a -> Bool Source #

Check if a list contains the element a

foldl :: (b -> a -> b) -> b -> ListN n a -> b Source #

Fold all elements from left

foldl' :: (b -> a -> b) -> b -> ListN n a -> b Source #

Fold all elements from left strictly

foldl1' :: 1 <= n => (a -> a -> a) -> ListN n a -> a Source #

Fold all elements from left strictly with a first element as the accumulator

scanl' :: (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' :: (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 :: (a -> b -> b) -> b -> ListN n a -> b Source #

Fold all elements from right

foldr1 :: 1 <= n => (a -> a -> a) -> ListN n a -> a Source #

Fold all elements from right assuming at least one element is in the list.

reverse :: ListN n a -> ListN n a Source #

Reverse a list

append :: ListN n a -> ListN m a -> ListN (n + m) a Source #

Append 2 list together returning the new list

minimum :: ( Ord a, 1 <= n) => ListN n a -> a Source #

Get the minimum element of a list

maximum :: ( Ord a, 1 <= n) => ListN n a -> a Source #

Get the maximum element of a list

head :: 1 <= n => ListN n a -> a Source #

Get the head element of a list

tail :: 1 <= n => ListN n a -> ListN (n - 1) a Source #

Get the tail of a list

init :: 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 (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 (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 :: 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 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a, b, c) Source #

Zip 3 lists of the same size

zip4 :: 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 :: 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 :: ListN n (a, b) -> ( ListN n a, ListN n b) Source #

Unzip a list of tuple, to 2 List of the deconstructed tuples

zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x Source #

Zip 2 lists using a function

zipWith3 :: (a -> b -> c -> x) -> ListN n a -> ListN n b -> ListN n c -> ListN n x Source #

Zip 3 lists using a function

zipWith4 :: (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 :: (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 :: Monad m => ListN n (m a) -> m ( ListN n a) Source #

Evaluate each monadic action in the list sequentially, and collect the results.

sequence_ :: Monad m => ListN n (m a) -> m () Source #

Evaluate each monadic action in the list sequentially, and ignore the results.

mapM :: Monad m => (a -> m b) -> ListN n a -> m ( ListN n b) Source #

Map each element of a List to a monadic action, evaluate these actions sequentially and collect the results

mapM_ :: Monad m => (a -> m b) -> ListN n a -> m () Source #

Map each element of a List to a monadic action, evaluate these actions sequentially and ignore the results