Maintainer	Ziyang Liu <free@cofree.io>
Safe Haskell	Safe
Language	Haskell2010

Data.NList

Contents

NList type
Basic functions
Extracing sublists
Indexing
Transformations
Ordered lists
Zipping and unzipping
Construction
Predecessor of a Nat

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

data NList (n :: Nat) a
(<:>) :: a -> NList n a -> NList (n + 1) a
(<++>) :: NList n a -> NList m a -> NList (n + m) a
length :: NList n a -> Int
head :: 1 <= n => NList n a -> a
headMay :: NList n a -> Maybe a
tail :: 1 <= n => NList n a -> NList (Pred n) a
tail' :: NList n a -> NList (Pred n) a
tailMay :: NList n a -> Maybe (NList (Pred n) a)
last :: 1 <= n => NList n a -> a
lastMay :: NList n a -> Maybe a
init :: 1 <= n => NList n a -> NList (Pred n) a
init' :: NList n a -> NList (Pred n) a
initMay :: NList n a -> Maybe (NList (Pred n) a)
toList :: NList n a -> [a]
take :: forall k n a. (KnownNat k, k <= n) => NList n a -> NList k a
drop :: forall k n a. (KnownNat k, k <= n) => NList n a -> NList (n - k) a
splitAt :: forall k n a. (KnownNat k, k <= n) => NList n a -> (NList k a, NList (n - k) a)
kth :: forall k n a. (KnownNat k, k <= (n - 1)) => NList n a -> a
reverse :: NList n a -> NList n a
intersperse :: a -> NList n a -> NList (Pred (n * 2)) a
transpose :: NList n (NList m a) -> NList m (NList n a)
concat :: NList n (NList m a) -> NList (n * m) a
sort :: Ord a => NList n a -> NList n a
sortOn :: Ord b => (a -> b) -> NList n a -> NList n a
sortBy :: (a -> a -> Ordering) -> NList n a -> NList n a
zip :: NList n a -> NList n b -> NList n (a, b)
zipWith :: (a -> b -> c) -> NList n a -> NList n b -> NList n c
unzip :: NList n (a, b) -> (NList n a, NList n b)
replicate :: forall n a. KnownNat n => a -> NList n a
empty :: NList 0 a
singleton :: a -> NList 1 a
mk1 :: a -> NList 1 a
mk2 :: a -> a -> NList 2 a
mk3 :: a -> a -> a -> NList 3 a
mk4 :: a -> a -> a -> a -> NList 4 a
mk5 :: a -> a -> a -> a -> a -> NList 5 a
mk6 :: a -> a -> a -> a -> a -> a -> NList 6 a
mk7 :: a -> a -> a -> a -> a -> a -> a -> NList 7 a
mk8 :: a -> a -> a -> a -> a -> a -> a -> a -> NList 8 a
mk9 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> NList 9 a
mk10 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> a -> NList 10 a
type family Pred (n :: Nat) :: Nat where ...

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