A nondeterminism monad. #
We represent nondeterministic values in a type α
as a single field structure containing an
MLList m (σ × α)
, i.e. as a monadic lazy list of possible values,
each equipped with the backtrackable state
required to run further computations in the ambient monad.
We provide an Alternative
Monad
instance, as well as functions bind
, mapM
, and filterMapM
,
and functions singletonM
, ofListM
, ofOptionM
, and firstM
for entering and leaving the nondeterministic world.
Operations on the nondeterministic value via bind
, mapM
, and filterMapM
run with the appropriate backtrackable state, and are responsible for updating the state themselves
(typically this doesn't need to be done explicitly,
but just happens as a side effect in the monad m
).
Nondet m α
is variation on MLList m α
suitable for use with backtrackable monads m
.
We think of Nondet m α
as a nondeterministic value in α
,
with the possible alternatives stored in a monadic lazy list.
Along with each a : α
we store the backtrackable state, and ensure that monadic operations
on alternatives run with the appropriate state.
Operations on the nondeterministic value via bind
, mapM
, and filterMapM
run with the appropriate backtrackable state, and are responsible for updating the state themselves
(typically this doesn't need to be done explicitly,
but just happens as a side effect in the monad m
).
Convert a non-deterministic value into a lazy list, keeping the backtrackable state. Be careful that monadic operations on the
MLList
will not respect this state!
Instances For
The empty nondeterministic value.
Equations
Instances For
Equations
Bind a nondeterministic function over a nondeterministic value, ensuring the function is run with the relevant backtrackable state at each value.
Convert any value in the monad to the singleton nondeterministic value.
Equations
Instances For
Convert a value to the singleton nondeterministic value.
Equations
Instances For
Nondet m
is a monad.
Equations
Nondet m
is an alternative monad.
Equations
Equations
Lift a list of monadic values to a nondeterministic value. We ensure that each monadic value is evaluated with the same backtrackable state.
Equations
Instances For
Lift a list of values to a nondeterministic value. (The backtrackable state in each will be identical: whatever the state was when we first read from the result.)
Equations
Instances For
Convert a monadic optional value to a nondeterministic value.
Equations
Instances For
Convert an optional value to a nondeterministic value.
Equations
Instances For
All iterations of a non-deterministic function on an initial value.
(That is, depth first search.)
Find the first alternative in a nondeterministic value, as a monadic value.
Equations
Instances For
Find the value of a monadic function on the first alternative in a nondeterministic value where the function succeeds.
Equations
Instances For
Convert a non-deterministic value into a lazy list, by discarding the backtrackable state.
Equations
Instances For
Convert a non-deterministic value into a list in the monad, by discarding the backtrackable state.