| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.ListT
Description
ListT done right,
see https://www.haskell.org/haskellwiki/ListT_done_right_alternative
There is also the list-t package on hackage (Nikita Volkov)
but it again depends on other packages we do not use yet,
so we rather implement the few bits we need afresh.
Synopsis
- newtype ListT m a = ListT {}
- mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b
- unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
- nilListT :: Monad m => ListT m a
- consListT :: Monad m => a -> ListT m a -> ListT m a
- sgListT :: Monad m => a -> ListT m a
- caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
- foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b
- anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
- allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
- sequenceListT :: Monad m => ListT m a -> m [a]
- concatListT :: Monad m => ListT m (ListT m a) -> ListT m a
- runMListT :: Monad m => m (ListT m a) -> ListT m a
- consMListT :: Monad m => m a -> ListT m a -> ListT m a
- sgMListT :: Monad m => m a -> ListT m a
- mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b
- mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
- liftListT :: (Monad m, Monad m') => (forall a. m a -> m' a) -> ListT m a -> ListT m' a
Documentation
Lazy monadic computation of a list of results.
Instances
mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b Source #
Boilerplate function to lift MonadReader through the ListT transformer.
unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)) Source #
Inverse to mapListT.
List operations
caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b Source #
Case distinction over lazy list.
foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b Source #
Folding a lazy list, effects left-to-right.
anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool Source #
Lazy monadic disjunction of lazy monadic list, effects left-to-right
allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool Source #
Lazy monadic conjunction of lazy monadic list, effects left-to-right
sequenceListT :: Monad m => ListT m a -> m [a] Source #
Force all values in the lazy list, effects left-to-right
concatListT :: Monad m => ListT m (ListT m a) -> ListT m a Source #
The join operation of the ListT m monad.
Monadic list operations.
runMListT :: Monad m => m (ListT m a) -> ListT m a Source #
We can `run' a computation of a ListT as it is monadic itself.
mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b Source #
Extending a monadic function to ListT.