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.