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

Data.List.Indexed.Counted

Description

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

Synopsis

# Documentation

data CountedList n a where Source

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 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.