Data.List.Tagged
- data TaggedList n α where
- E :: TaggedList Zero α
- :. :: α -> TaggedList n α -> TaggedList (SuccessorTo n) α
- data UntaggedList α = forall n . UntaggedList (TaggedList n α)
- newtype TL α n = TL {
- unwrapTL :: TaggedList n α
- newtype ATL t α n = ATL {
- unwrapATL :: t (TaggedList n α)
- append :: TaggedList m α -> TaggedList n α -> TaggedList (Plus m n) α
- eqLists :: Eq α => TaggedList m α -> TaggedList n α -> Bool
- extractRightsOrLefts :: TaggedList n (Either α β) -> Either [α] (TaggedList n β)
- fromList :: Induction n => [α] -> TaggedList n α
- fromListAsUntagged :: [α] -> UntaggedList α
- head :: TaggedList (SuccessorTo n) α -> α
- join :: TaggedList m α -> TaggedList n α -> (TaggedList (Plus m n) α, TaggedList (Plus m n) β -> (TaggedList m β, TaggedList n β))
- length :: NaturalNumber n => TaggedList n α -> N n
- map :: (α -> β) -> TaggedList n α -> TaggedList n β
- mapM_ :: Monad m => (α -> m β) -> TaggedList n α -> m ()
- replace :: [α] -> TaggedList n β -> TaggedList n α
- tail :: TaggedList (SuccessorTo n) α -> TaggedList n α
- toList :: TaggedList n α -> [α]
- withTL :: (TL α n -> TL β n) -> TaggedList n α -> TaggedList n β
- zipf :: TaggedList n (α -> β) -> TaggedList n α -> TaggedList n β
- type family TupleOf n α
- class TupleConvertable n where
- fromTuple :: TupleOf n α -> TaggedList n α
- toTuple :: TaggedList n α -> TupleOf n α
Tagged lists
data TaggedList n α whereSource
TaggedList is a data structure that represents a linked-list tagged with a phantom type-level natural number representing the length of the list.
Constructors
| E :: TaggedList Zero α | |
| :. :: α -> TaggedList n α -> TaggedList (SuccessorTo n) α |
Instances
| Typeable2 TaggedList | |
| Induction n => Functor (TaggedList n) | |
| Induction n => Foldable (TaggedList n) | |
| Induction n => Traversable (TaggedList n) | |
| (Induction n, Eq α) => Eq (TaggedList n α) | |
| (Induction n, Binary α) => Binary (TaggedList n α) |
data UntaggedList α Source
UntaggedList is a wrapper around TaggedList that lets you hide the length tag; the purpose of this is to allow for situations in which you have a tagged list with an unknown length.
Constructors
| forall n . UntaggedList (TaggedList n α) |
Instances
| Typeable1 UntaggedList | |
| Binary α => Binary (UntaggedList α) |
TL is a newtype wrapper around a TaggedList which flips the two type arguments; this type was introduced to make it easier to define inductive operations on TaggedLists.
Constructors
| TL | |
Fields
| |
ATL is a newtype wrapper around some functor of TaggedList which flips the two type arguments; this type was introduced to make it easier to define inductive operations on functors of TaggedLists.
Constructors
| ATL | |
Fields
| |
Utility functions
append :: TaggedList m α -> TaggedList n α -> TaggedList (Plus m n) αSource
Appends two tagged lists.
(Note: The order of the arguments to Plus is important since append is defined recursively over its *first* argument.)
eqLists :: Eq α => TaggedList m α -> TaggedList n α -> BoolSource
Compares two lists, which may be of different sizes; False is returned if the lists do not have the same size.
extractRightsOrLefts :: TaggedList n (Either α β) -> Either [α] (TaggedList n β)Source
fromList :: Induction n => [α] -> TaggedList n αSource
Converts a list to a TaggedList, returning _|_ if the length of the list does not match the length tag of the return type.
fromListAsUntagged :: [α] -> UntaggedList αSource
Converts an arbitrary list to an UntaggedList.
head :: TaggedList (SuccessorTo n) α -> αSource
Returns the head of a tagged list.
Note that unlike its List counterpart, this function never returns _|_ since the existence of at least one element is guaranteed by the type system.
join :: TaggedList m α -> TaggedList n α -> (TaggedList (Plus m n) α, TaggedList (Plus m n) β -> (TaggedList m β, TaggedList n β))Source
Appends two lists together, and returns both the result and a splitter function that allows you to take another list of the same size as the result (though possible of a different type) and split it back into two lists of the sizes of the arguments to this function.
length :: NaturalNumber n => TaggedList n α -> N nSource
Returns the length of the list as a value-level natural number.
map :: (α -> β) -> TaggedList n α -> TaggedList n βSource
Applies a function to every element of the list.
mapM_ :: Monad m => (α -> m β) -> TaggedList n α -> m ()Source
Performs an action for every element in the list and returns ().
replace :: [α] -> TaggedList n β -> TaggedList n αSource
Replaces all of the elements in a given tagged list with the members of an ordinary list, returning _|_ if the length of the list does not match the length tag.
tail :: TaggedList (SuccessorTo n) α -> TaggedList n αSource
Returns the tail of a tagged list.
Note that unlike its List counterpart, this function never returns _|_ since the existence of at least one element is guaranteed by the type system.
toList :: TaggedList n α -> [α]Source
Converts a tagged list to an ordinary list.
withTL :: (TL α n -> TL β n) -> TaggedList n α -> TaggedList n βSource
This is a convenience function for lifting a function on TL to a function on TaggedList.
(Note: TL is just a newtype wrapper around TaggedList that swaps the two type arguments to make it easier to perform inductive operations.)
zipf :: TaggedList n (α -> β) -> TaggedList n α -> TaggedList n βSource
Applies a list of functions to a list of inputs.
Tuple conversion
type family TupleOf n α Source
TupleOf is a type family that maps type-level natural numbers (from N0 to N15) to tuples with the corresponding number of entries.
class TupleConvertable n whereSource
The class TupleConvertable provides methods for converting tagged lists to and from tuples.
Methods
fromTuple :: TupleOf n α -> TaggedList n αSource
toTuple :: TaggedList n α -> TupleOf n αSource
Instances