Data.List.Indexed.Counted

This module implements homogeneous counted lists, which are type-indexed by length.

Documentation

data CountedList n a where

Counted lists are indexed by length in the type.

Constructors

(:::) :: a -> CountedList n a -> CountedList (Succ n) a infixr 5

CountedNil :: CountedList Zero a

Instances

Functor (CountedList n)

ReifyNatural n => Applicative (CountedList n)

Show x => Show (CountedList n x)

count :: CountedList n a -> Natural n

The count of a list is the natural number corresponding to its length.

unCount :: CountedList n a -> [a]

Convert a counted list to a regular Haskell list.

replicate :: Natural n -> x -> CountedList n x

Replicate some element a certain number of times.

append :: CountedList n a -> CountedList m a -> CountedList (m + n) a

Appending two counted lists yields one of length equal to the sum of the lengths of the two initial lists.

nth :: n < m => Natural n -> CountedList m a -> a

Take the nth element of a list. We statically prevent taking the nth element of a list of length less than n.

padTo :: m <= n => Natural n -> x -> CountedList m x -> CountedList ((n - m) + m) x

Pad the length of a list to a given length. If the number specified is less than the length of the list given, it won't pass the type-checker.

zip :: CountedList n a -> CountedList n b -> CountedList n (a, b)

Zip two equal-length lists together.