Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.ListT

Contents

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

Documentation

newtype ListT m a

Lazy monadic computation of a list of results.

Constructors

ListT 

Fields

runListT :: m (Maybe (a, 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.