Monadic lazy lists. #
Lazy lists with "laziness" controlled by an arbitrary monad.
In an initial section we describe the specification of MLList
,
and provide a private unsafe implementation,
and then a public opaque
wrapper of this implementation, satisfying the specification.
Equations
Constructs an MLList
recursively, with state in α
, recording terms from β
.
If f
returns none
the list will terminate.
Variant of MLList.fix?
that allows returning values of a different type.
Repeatedly apply a function f : α → m (α × List β)
to an initial a : α
,
accumulating the elements of the resulting List β
as a single monadic lazy list.
(This variant allows starting with a specified List β
of elements, as well. )
Performs a case distinction on a MLList
when the motive is a MLList
as well.
(We need to be in a monadic context to distinguish a nil from a cons.)
Equations
Instances For
Gives the monadic lazy list consisting all of folds of a function on a given initial element.
Thus [a₀, a₁, ...].foldsM f b
will give [b, ← f b a₀, ← f (← f b a₀) a₁, ...]
.
Gives the monadic lazy list consisting all of folds of a function on a given initial element.
Thus [a₀, a₁, ...].foldsM f b
will give [b, f b a₀, f (f b a₀) a₁, ...]
.
Equations
Instances For
Implementation of MLList.fin
.
Implementation of MLList.ofArray
.
Lift the monad of a lazy list.
Run a lazy list in a StateRefT'
monad on some initial state.
Return the head of a monadic lazy list, as a value in the monad. Fails if the list is empty.
Equations
Instances For
Apply a function returning values inside the monad to a monadic lazy list, returning only the first successful result.
Equations
Instances For
Return the first value on which a predicate returns true.