IndexedList- Length- and element-indexed lists sitting somewhere between homogeneous and fully heterogeneous.

CopyrightCopyright (c) 2014 Kenneth Foner
Safe HaskellSafe-Inferred



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



data CountedList n a where Source

Counted lists are indexed by length in the type.


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

count :: CountedList n a -> Natural n Source

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

unCount :: CountedList n a -> [a] Source

Convert a counted list to a regular Haskell list.

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

Replicate some element a certain number of times.

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

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 Source

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 Source

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

Zip two equal-length lists together.