ModuleAgda-2.7.0.1Haskell2010

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.

1 type
17 values

PackageAgda-2.7.0.1
Exports18
LanguageHaskell2010
LicenceMIT
SourceListT.hs

newtypenewtype ListT (m :: Type -> Type) a

Lazy monadic computation of a list of results.

Constructors

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

Instances26MonadTrans, MonadReader, MonadState, MonadFresh, Monad, Functor, …

MonadTrans ListTDefined in Agda-2.7.0.1 · Agda.Utils.ListT
(Applicative m, MonadReader r m) => MonadReader r (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
(Applicative m, MonadState s m) => MonadState s (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
MonadFresh i m => MonadFresh i (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
(Functor m, Applicative m, Monad m) => Monad (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
Functor m => Functor (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
Monad m => MonadFail (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
(Functor m, Applicative m, Monad m) => Applicative (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
(Functor m, Applicative m, Monad m) => Alternative (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
(Functor m, Applicative m, Monad m) => MonadPlus (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
(Applicative m, MonadIO m) => MonadIO (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
MonadBench m => MonadBench (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
HasOptions m => HasOptions (ListT m)Defined in Agda-2.7.0.1 · Agda.Interaction.Options.HasOptions
MonadReduce m => MonadReduce (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
MonadTCEnv m => MonadTCEnv (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
MonadTCM tcm => MonadTCM (ListT tcm)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
MonadTCState m => MonadTCState (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
ReadTCState m => ReadTCState (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
HasBuiltins m => HasBuiltins (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
MonadAddContext m => MonadAddContext (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Context
MonadDebug m => MonadDebug (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
PureTCM m => PureTCM (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Pure
HasConstInfo m => HasConstInfo (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Signature
Monad m => Semigroup (ListT m a)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
Monad m => Monoid (ListT m a)Defined in Agda-2.7.0.1 · Agda.Utils.ListT
type BenchPhase (ListT m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark

valuemapListT

:: m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
-> ListT m a
-> ListT n b

Boilerplate function to lift MonadReader through the ListT transformer.

valueunmapListT

:: ListT m a -> ListT n b
-> m (Maybe (a, ListT m a))
-> n (Maybe (b, ListT n b))

Inverse to mapListT.

List operations

9 declarations

valuenilListT :: Monad m => ListT m a

The empty lazy list.

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

Consing a value to a lazy list.

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

Singleton lazy list.

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

Case distinction over lazy list.

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

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

valueanyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool

Lazy monadic disjunction of lazy monadic list, effects left-to-right

valueallListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool

Lazy monadic conjunction of lazy monadic list, effects left-to-right

valuesequenceListT :: Monad m => ListT m a -> m [a]

Force all values in the lazy list, effects left-to-right

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

The join operation of the ListT m monad.

Monadic list operations.

6 declarations

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

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

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

Monadic cons.

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

Monadic singleton.

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

Extending a monadic function to ListT.

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

Alternative implementation using foldListT.

valueliftListT

:: (Monad m, Monad m')
=> forall a1. m a1 -> m' a1
-> ListT m a
-> ListT m' a

Change from one monad to another