Copyright | Copyright (c) 2014 Kenneth Foner |
---|---|

Maintainer | kenneth.foner@gmail.com |

Stability | experimental |

Portability | non-portable |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

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

- data CountedList n a where
- (:::) :: a -> CountedList n a -> CountedList (Succ n) a
- CountedNil :: CountedList Zero a

- count :: CountedList n a -> Natural n
- unCount :: CountedList n a -> [a]
- replicate :: Natural n -> x -> CountedList n x
- append :: CountedList n a -> CountedList m a -> CountedList (m + n) a
- nth :: n < m => Natural n -> CountedList m a -> a
- padTo :: m <= n => Natural n -> x -> CountedList m x -> CountedList ((n - m) + m) x
- zip :: CountedList n a -> CountedList n b -> CountedList n (a, b)

# Documentation

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 |

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.