| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.ListInf
Description
Infinite lists (streams).
Wrapper for Data.List.Infinite from the infinite-list package
that generalizes some type signatures, using Integral for indexing,
and adds some missing functions.
Import this module as follows:
import Agda.Utils.ListInf (ListInf, pattern (:<)) import Agda.Utils.ListInf qualified as ListInf
Motivation: lists constructed by repeat, iterate, cycle etc.
are infinite, so the nil case can never arise when consuming them,
e.g. in a take or zipWith.
Constructing them as properly infinite lists (ListInf) should thus
lead to slightly more efficient code, eliminating impossible cases.
Synopsis
- (!!) :: Integral n => ListInf a -> n -> a
- append :: [a] -> ListInf a -> ListInf a
- drop :: Integral n => n -> ListInf a -> ListInf a
- pad :: [a] -> a -> ListInf a
- splitAt :: Integral n => n -> ListInf a -> ([a], ListInf a)
- take :: Integral n => n -> ListInf a -> [a]
- upFrom :: Enum n => n -> ListInf n
- updateAt :: Integral n => n -> (a -> a) -> ListInf a -> ListInf a
- type ListInf = Infinite
- cycle :: NonEmpty a -> Infinite a
- head :: Infinite a -> a
- iterate :: (a -> a) -> a -> Infinite a
- prependList :: [a] -> Infinite a -> Infinite a
- repeat :: a -> Infinite a
- tail :: Infinite a -> Infinite a
- zip :: Infinite a -> Infinite b -> Infinite (a, b)
- zipWith :: (a -> b -> c) -> Infinite a -> Infinite b -> Infinite c
- pattern (:<) :: a -> Infinite a -> Infinite a
Documentation
append :: [a] -> ListInf a -> ListInf a Source #
There is only one meaningful way to concatenate a finite and an infinite list,
justifying the name append = prependList.
splitAt :: Integral n => n -> ListInf a -> ([a], ListInf a) Source #
splitAt n as == (take n as, drop n as)
updateAt :: Integral n => n -> (a -> a) -> ListInf a -> ListInf a Source #
Update the nth element of an infinite list.
Θ(n).
Precondition: the index n is >= 0.
prependList :: [a] -> Infinite a -> Infinite a #