Agda.Utils.ListT

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.

Documentation

newtype ListT m a

Lazy monadic computation of a list of results.

Constructors

ListT

Fields

runListT :: m (Maybe (a, ListT m a))

Instances

MonadTrans ListT

(Applicative m, MonadState s m) => MonadState s (ListT m)

(Applicative m, MonadReader r m) => MonadReader r (ListT m)

(Functor m, Applicative m, Monad m) => Monad (ListT m)

Functor m => Functor (ListT m)

(Functor m, Applicative m, Monad m) => Applicative (ListT m)

(Functor m, Applicative m, Monad m) => Alternative (ListT m)

(Functor m, Applicative m, Monad m) => MonadPlus (ListT m)

(Applicative m, MonadIO m) => MonadIO (ListT m)

MonadTCM tcm => MonadTCM (ListT tcm)

Monad m => Monoid (ListT m a)

List operations

nilListT :: Monad m => ListT m a

The empty lazy list.

consListT :: Monad m => a -> ListT m a -> ListT m a

Consing a value to a lazy list.

sgListT :: Monad m => a -> ListT m a

Singleton lazy list.

caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b

Case distinction over lazy list.

foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b

Folding a lazy list, effects left-to-right.

concatListT :: Monad m => ListT m (ListT m a) -> ListT m a

The join operation of the ListT m monad.

Monadic list operations.

runMListT :: Monad m => m (ListT m a) -> ListT m a

We can `run' a computation of a ListT as it is monadic itself.

consMListT :: Monad m => m a -> ListT m a -> ListT m a

Monadic cons.

sgMListT :: Monad m => m a -> ListT m a

Monadic singleton.

mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b

Extending a monadic function to ListT.

mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b

Alternative implementation using foldListT.