Data.NList

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.

NList type

data NList (n :: Nat) a

A list whose length is statically known.

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

Instances

Functor (NList n)

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)

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)

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)

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)

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)

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)

Defined in Data.NList

Methods

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

show :: NList n a -> String

showList :: [NList n a] -> ShowS

ToTuple (NList 2 a)

Defined in Data.NList

Associated Types

type Tuple (NList 2 a) :: Type

Methods

toTuple :: NList 2 a -> Tuple (NList 2 a)

ToTuple (NList 3 a)

Defined in Data.NList

Associated Types

type Tuple (NList 3 a) :: Type

Methods

toTuple :: NList 3 a -> Tuple (NList 3 a)

ToTuple (NList 4 a)

Defined in Data.NList

Associated Types

type Tuple (NList 4 a) :: Type

Methods

toTuple :: NList 4 a -> Tuple (NList 4 a)

ToTuple (NList 5 a)

Defined in Data.NList

Associated Types

type Tuple (NList 5 a) :: Type

Methods

toTuple :: NList 5 a -> Tuple (NList 5 a)

ToTuple (NList 6 a)

Defined in Data.NList

Associated Types

type Tuple (NList 6 a) :: Type

Methods

toTuple :: NList 6 a -> Tuple (NList 6 a)

ToTuple (NList 7 a)

Defined in Data.NList

Associated Types

type Tuple (NList 7 a) :: Type

Methods

toTuple :: NList 7 a -> Tuple (NList 7 a)

ToTuple (NList 8 a)

Defined in Data.NList

Associated Types

type Tuple (NList 8 a) :: Type

Methods

toTuple :: NList 8 a -> Tuple (NList 8 a)

ToTuple (NList 9 a)

Defined in Data.NList

Associated Types

type Tuple (NList 9 a) :: Type

Methods

toTuple :: NList 9 a -> Tuple (NList 9 a)

ToTuple (NList 10 a)

Defined in Data.NList

Associated Types

type Tuple (NList 10 a) :: Type

Methods

toTuple :: NList 10 a -> Tuple (NList 10 a)

type Tuple (NList 2 a)

Defined in Data.NList

type Tuple (NList 2 a) = (a, a)

type Tuple (NList 3 a)

Defined in Data.NList

type Tuple (NList 3 a) = (a, a, a)

type Tuple (NList 4 a)

Defined in Data.NList

type Tuple (NList 4 a) = (a, a, a, a)

type Tuple (NList 5 a)

Defined in Data.NList

type Tuple (NList 5 a) = (a, a, a, a, a)

type Tuple (NList 6 a)

Defined in Data.NList

type Tuple (NList 6 a) = (a, a, a, a, a, a)

type Tuple (NList 7 a)

Defined in Data.NList

type Tuple (NList 7 a) = (a, a, a, a, a, a, a)

type Tuple (NList 8 a)

Defined in Data.NList

type Tuple (NList 8 a) = (a, a, a, a, a, a, a, a)

type Tuple (NList 9 a)

Defined in Data.NList

type Tuple (NList 9 a) = (a, a, a, a, a, a, a, a, a)

type Tuple (NList 10 a)

Defined in Data.NList

type Tuple (NList 10 a) = (a, a, a, a, a, a, a, a, a, a)

Basic functions

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

Prepend an element to a list.

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

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

Append two lists.

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

length :: NList n a -> Int

Length of a list.

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

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

Head of a non-empty list.

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

headMay :: NList n a -> Maybe a

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

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

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)

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

The last element of a non-empty list.

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

lastMay :: NList n a -> Maybe a

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

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

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)

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

uncons :: 1 <= n => NList n a -> (a, NList (n - 1) a)

Decompose a list into head and tail.

uncons (singleton 'a') === ('a', empty)
uncons (mk3 'a' 'b' 'c') === ('a', mk2 'b' 'c')

toList :: NList n a -> [a]

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

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

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)

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

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

Reverse a list.

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

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

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)

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

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

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

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

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)

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

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)

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

Return a list containing n copies of the given element.

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

empty :: NList 0 a

The empty list.

length empty === 0

singleton :: a -> NList 1 a

A singleton list.

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

mk1 :: a -> NList 1 a

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

mk2 :: a -> a -> NList 2 a

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

mk3 :: a -> a -> a -> NList 3 a

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

mk4 :: a -> a -> a -> a -> NList 4 a

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

mk5 :: a -> a -> a -> a -> a -> NList 5 a

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

mk6 :: a -> a -> a -> a -> a -> a -> NList 6 a

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

mk7 :: a -> a -> a -> a -> a -> a -> a -> NList 7 a

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

mk8 :: a -> a -> a -> a -> a -> a -> a -> a -> NList 8 a

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

mk9 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> NList 9 a

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

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

To and from tuples

class FromTuple a where

Typeclass for converting tuples to NLists.

Associated Types

type List a

Methods

fromTuple :: a -> List a

Instances

FromTuple (a, a)

Defined in Data.NList

Associated Types

type List (a, a) :: Type

Methods

fromTuple :: (a, a) -> List (a, a)

FromTuple (a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a) :: Type

Methods

fromTuple :: (a, a, a) -> List (a, a, a)

FromTuple (a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a) -> List (a, a, a, a)

FromTuple (a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a) -> List (a, a, a, a, a)

FromTuple (a, a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a, a) -> List (a, a, a, a, a, a)

FromTuple (a, a, a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a, a, a) -> List (a, a, a, a, a, a, a)

FromTuple (a, a, a, a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a, a, a, a) -> List (a, a, a, a, a, a, a, a)

FromTuple (a, a, a, a, a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a, a, a, a, a) -> List (a, a, a, a, a, a, a, a, a)

FromTuple (a, a, a, a, a, a, a, a, a, a)

Defined in Data.NList

Associated Types

type List (a, a, a, a, a, a, a, a, a, a) :: Type

Methods

fromTuple :: (a, a, a, a, a, a, a, a, a, a) -> List (a, a, a, a, a, a, a, a, a, a)

class ToTuple a where

Typeclass for converting NLists to tuples.

Associated Types

type Tuple a

Methods

toTuple :: a -> Tuple a

Instances

ToTuple (NList 2 a)

Defined in Data.NList

Associated Types

type Tuple (NList 2 a) :: Type

Methods

toTuple :: NList 2 a -> Tuple (NList 2 a)

ToTuple (NList 3 a)

Defined in Data.NList

Associated Types

type Tuple (NList 3 a) :: Type

Methods

toTuple :: NList 3 a -> Tuple (NList 3 a)

ToTuple (NList 4 a)

Defined in Data.NList

Associated Types

type Tuple (NList 4 a) :: Type

Methods

toTuple :: NList 4 a -> Tuple (NList 4 a)

ToTuple (NList 5 a)

Defined in Data.NList

Associated Types

type Tuple (NList 5 a) :: Type

Methods

toTuple :: NList 5 a -> Tuple (NList 5 a)

ToTuple (NList 6 a)

Defined in Data.NList

Associated Types

type Tuple (NList 6 a) :: Type

Methods

toTuple :: NList 6 a -> Tuple (NList 6 a)

ToTuple (NList 7 a)

Defined in Data.NList

Associated Types

type Tuple (NList 7 a) :: Type

Methods

toTuple :: NList 7 a -> Tuple (NList 7 a)

ToTuple (NList 8 a)

Defined in Data.NList

Associated Types

type Tuple (NList 8 a) :: Type

Methods

toTuple :: NList 8 a -> Tuple (NList 8 a)

ToTuple (NList 9 a)

Defined in Data.NList

Associated Types

type Tuple (NList 9 a) :: Type

Methods

toTuple :: NList 9 a -> Tuple (NList 9 a)

ToTuple (NList 10 a)

Defined in Data.NList

Associated Types

type Tuple (NList 10 a) :: Type

Methods

toTuple :: NList 10 a -> Tuple (NList 10 a)

Predecessor of a Nat

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

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