indexed-containers-0.1.0.0: Simple, no-frills indexed lists.

MaintainerZiyang Liu <free@cofree.io>
Safe HaskellSafe
LanguageHaskell2010

Data.NList

Contents

Description

Lists whose types are indexed by their lengths. The implementation is a simple wrapper around a regular list.

All functions in this module are total. The time complexity of each function is the same as that of the corresponding function on regular lists.

Synopsis

NList type

data NList (n :: Nat) a Source #

A list whose length is statically known.

Type parameter n, of kind Nat, is the length of the list.

Instances
Functor (NList n) Source # 
Instance details

Defined in Data.NList

Methods

fmap :: (a -> b) -> NList n a -> NList n b #

(<$) :: a -> NList n b -> NList n a #

KnownNat n => Applicative (NList n) Source # 
Instance details

Defined in Data.NList

Methods

pure :: a -> NList n a #

(<*>) :: NList n (a -> b) -> NList n a -> NList n b #

liftA2 :: (a -> b -> c) -> NList n a -> NList n b -> NList n c #

(*>) :: NList n a -> NList n b -> NList n b #

(<*) :: NList n a -> NList n b -> NList n a #

Foldable (NList n) Source # 
Instance details

Defined in Data.NList

Methods

fold :: Monoid m => NList n m -> m #

foldMap :: Monoid m => (a -> m) -> NList n a -> m #

foldr :: (a -> b -> b) -> b -> NList n a -> b #

foldr' :: (a -> b -> b) -> b -> NList n a -> b #

foldl :: (b -> a -> b) -> b -> NList n a -> b #

foldl' :: (b -> a -> b) -> b -> NList n a -> b #

foldr1 :: (a -> a -> a) -> NList n a -> a #

foldl1 :: (a -> a -> a) -> NList n a -> a #

toList :: NList n a -> [a] #

null :: NList n a -> Bool #

length :: NList n a -> Int #

elem :: Eq a => a -> NList n a -> Bool #

maximum :: Ord a => NList n a -> a #

minimum :: Ord a => NList n a -> a #

sum :: Num a => NList n a -> a #

product :: Num a => NList n a -> a #

Traversable (NList n) Source # 
Instance details

Defined in Data.NList

Methods

traverse :: Applicative f => (a -> f b) -> NList n a -> f (NList n b) #

sequenceA :: Applicative f => NList n (f a) -> f (NList n a) #

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

sequence :: Monad m => NList n (m a) -> m (NList n a) #

Eq a => Eq (NList n a) Source # 
Instance details

Defined in Data.NList

Methods

(==) :: NList n a -> NList n a -> Bool #

(/=) :: NList n a -> NList n a -> Bool #

Ord a => Ord (NList n a) Source # 
Instance details

Defined in Data.NList

Methods

compare :: NList n a -> NList n a -> Ordering #

(<) :: NList n a -> NList n a -> Bool #

(<=) :: NList n a -> NList n a -> Bool #

(>) :: NList n a -> NList n a -> Bool #

(>=) :: NList n a -> NList n a -> Bool #

max :: NList n a -> NList n a -> NList n a #

min :: NList n a -> NList n a -> NList n a #

(KnownNat n, Show a) => Show (NList n a) Source # 
Instance details

Defined in Data.NList

Methods

showsPrec :: Int -> NList n a -> ShowS #

show :: NList n a -> String #

showList :: [NList n a] -> ShowS #

Basic functions

(<:>) :: a -> NList n a -> NList (n + 1) a infixr 5 Source #

Prepend an element to a list.

'a' <:> singleton 'b' === mk2 'a' 'b'

(<++>) :: NList n a -> NList m a -> NList (n + m) a infixr 5 Source #

Append two lists.

mk2 'a' 'b' <++> mk3 'c' 'd' 'e' === mk5 'a' 'b' 'c' 'd' 'e'

length :: NList n a -> Int Source #

Length of a list.

length (mk3 'a' 'b' 'c') === 3

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

Head of a non-empty list.

head (mk3 'a' 'b' 'c') === 'a'

headMay :: NList n a -> Maybe a Source #

Head of a list.

headMay (empty :: NList 0 Int) === Nothing
headMay (mk3 'a' 'b' 'c') === Just 'a'

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

Tail of a non-empty list.

tail (singleton 'a') === empty
tail (mk3 'a' 'b' 'c') === mk2 'b' 'c'

tail' :: NList n a -> NList (Pred n) a Source #

Tail of a list. Returns an empty list if the input is empty.

tail' (empty :: NList 0 ()) === empty
tail' (singleton 'a') === empty
tail' (mk3 'a' 'b' 'c') === mk2 'b' 'c'

tailMay :: NList n a -> Maybe (NList (Pred n) a) Source #

Tail of a list. Returns Nothing if the input is empty.

tailMay (empty :: NList 0 ()) === Nothing
tailMay (singleton 'a') === Just empty
tailMay (mk3 'a' 'b' 'c') === Just (mk2 'b' 'c')

last :: 1 <= n => NList n a -> a Source #

The last element of a non-empty list.

last (mk3 'a' 'b' 'c') === 'c'

lastMay :: NList n a -> Maybe a Source #

The last element of a list.

lastMay (empty :: NList 0 Int) === Nothing
lastMay (mk3 'a' 'b' 'c') === Just 'c'

init :: 1 <= n => NList n a -> NList (Pred n) a Source #

All elements of a non-empty list except the last one.

init (singleton 'a') === empty
init (mk3 'a' 'b' 'c') === mk2 'a' 'b'

init' :: NList n a -> NList (Pred n) a Source #

All elements of a list except the last one. Returns an empty list if the input is empty.

init' (empty :: NList 0 ()) === empty
init' (singleton 'a') === empty
init' (mk3 'a' 'b' 'c') === mk2 'a' 'b'

initMay :: NList n a -> Maybe (NList (Pred n) a) Source #

All elements of a list except the last one. Returns Nothing if the input is empty.

initMay (empty :: NList 0 ()) === Nothing
initMay (singleton 'a') === Just empty
initMay (mk3 'a' 'b' 'c') === Just (mk2 'a' 'b')

toList :: NList n a -> [a] Source #

Convert an NList into a regular list.

toList (mk3 'a' 'b' 'c') === "abc"

Extracing sublists

take :: forall k n a. (KnownNat k, k <= n) => NList n a -> NList k a Source #

Return the first k elements of a list whose length is at least k.

take @0 (mk3 'a' 'b' 'c') === empty
take @2 (mk3 'a' 'b' 'c') === mk2 'a' 'b'
take @3 (mk3 'a' 'b' 'c') === mk3 'a' 'b' 'c'

drop :: forall k n a. (KnownNat k, k <= n) => NList n a -> NList (n - k) a Source #

Drop the first k elements of a list whose length is at least k.

drop @0 (mk3 'a' 'b' 'c') === mk3 'a' 'b' 'c'
drop @2 (mk3 'a' 'b' 'c') === singleton 'c'
drop @3 (mk3 'a' 'b' 'c') === empty

splitAt :: forall k n a. (KnownNat k, k <= n) => NList n a -> (NList k a, NList (n - k) a) Source #

Return the first k elements, paired with the remaining elements, of a list whose length is at least k.

splitAt @0 (mk3 'a' 'b' 'c') === (empty, mk3 'a' 'b' 'c')
splitAt @2 (mk3 'a' 'b' 'c') === (mk2 'a' 'b', singleton 'c')
splitAt @3 (mk3 'a' 'b' 'c') === (mk3 'a' 'b' 'c', empty)

Indexing

kth :: forall k n a. (KnownNat k, k <= (n - 1)) => NList n a -> a Source #

Return the element at index k (starting from 0) in a list with at least k+1 elements.

kth @0 (mk4 'a' 'b' 'c' 'd') === 'a'
kth @3 (mk4 'a' 'b' 'c' 'd') === 'd'

Transformations

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

Reverse a list.

reverse (mk3 'a' 'b' 'c') === mk3 'c' 'b' 'a'

intersperse :: a -> NList n a -> NList (Pred (n * 2)) a Source #

Take an element and a list, and insert the element in between elements of the list.

intersperse (',') empty === empty
intersperse (',') (singleton 'a') === singleton 'a'
intersperse (',') (mk3 'a' 'b' 'c') === mk5 'a' ',' 'b' ',' 'c'

transpose :: NList n (NList m a) -> NList m (NList n a) Source #

Transpose the rows and columns of a two dimensional list.

transpose (mk2 (mk3 1 2 3) (mk3 4 5 6)) === mk3 (mk2 1 4) (mk2 2 5) (mk2 3 6)

concat :: NList n (NList m a) -> NList (n * m) a Source #

Concatenate the sublists of a two-dimensional list.

concat (mk2 (mk3 1 2 3) (mk3 4 5 6)) === mk6 1 2 3 4 5 6

Ordered lists

sort :: Ord a => NList n a -> NList n a Source #

Stably sort a list.

sort (mk6 1 4 2 8 5 7) === mk6 1 2 4 5 7 8

sortOn :: Ord b => (a -> b) -> NList n a -> NList n a Source #

Sort a list by applying a function to each element and comparing the results.

sortOn negate (mk6 1 4 2 8 5 7) === mk6 8 7 5 4 2 1

sortBy :: (a -> a -> Ordering) -> NList n a -> NList n a Source #

Non-overloaded version of sort.

sortBy (\x y -> compare (-x) (-y)) (mk6 1 4 2 8 5 7) === mk6 8 7 5 4 2 1

Zipping and unzipping

zip :: NList n a -> NList n b -> NList n (a, b) Source #

Zip two lists of the same length.

zip (mk2 1 2) (mk2 'a' 'b') === mk2 (1, 'a') (2, 'b')

zipWith :: (a -> b -> c) -> NList n a -> NList n b -> NList n c Source #

Zip with a function.

zipWith (+) (mk2 1 2) (mk2 3 4) === mk2 4 6

unzip :: NList n (a, b) -> (NList n a, NList n b) Source #

Unzip a list of pairs.

unzip (mk2 (1, 'a') (2, 'b')) === ((mk2 1 2), (mk2 'a' 'b'))

Construction

replicate :: forall n a. KnownNat n => a -> NList n a Source #

Return a list containing n copies of the given element.

replicate @3 'a' === mk3 'a' 'a' 'a'

empty :: NList 0 a Source #

The empty list.

length empty === 0

singleton :: a -> NList 1 a Source #

A singleton list.

length (singleton 'a' :: NList 1 Char) === 1

mk1 :: a -> NList 1 a Source #

toList (mk1 'a') === "a"

mk2 :: a -> a -> NList 2 a Source #

toList (mk2 'a' 'b') === "ab"

mk3 :: a -> a -> a -> NList 3 a Source #

toList (mk3 'a' 'b' 'c') === "abc"

mk4 :: a -> a -> a -> a -> NList 4 a Source #

toList (mk4 'a' 'b' 'c' 'd') === "abcd"

mk5 :: a -> a -> a -> a -> a -> NList 5 a Source #

toList (mk5 'a' 'b' 'c' 'd' 'e') === "abcde"

mk6 :: a -> a -> a -> a -> a -> a -> NList 6 a Source #

toList (mk6 'a' 'b' 'c' 'd' 'e' 'f') === "abcdef"

mk7 :: a -> a -> a -> a -> a -> a -> a -> NList 7 a Source #

toList (mk7 'a' 'b' 'c' 'd' 'e' 'f' 'g') === "abcdefg"

mk8 :: a -> a -> a -> a -> a -> a -> a -> a -> NList 8 a Source #

toList (mk8 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h') === "abcdefgh"

mk9 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> NList 9 a Source #

toList (mk9 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h' 'i') === "abcdefghi"

mk10 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> a -> NList 10 a Source #

toList (mk10 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h' 'i' 'j') === "abcdefghij"

Predecessor of a Nat

type family Pred (n :: Nat) :: Nat where ... Source #

The Pred type family is used to maintain the invariant that n is a KnownNat (i.e., n >= 0) for all List n a.

Equations

Pred 0 = 0 
Pred n = n - 1