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).

structure Nondet {σ : Type} (m : Type → Type) [Lean.MonadBacktrack σ m] (α : Type) : Type

• toMLList : MLList 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!

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).

def Nondet.nil {σ : Type} {m : Type → Type} [Lean.MonadBacktrack σ m] {α : Type} : Nondet m α

The empty nondeterministic value.

instance Nondet.instInhabitedNondet {σ : Type} {m : Type → Type} [Lean.MonadBacktrack σ m] {α : Type} : Inhabited (Nondet m α)

def Nondet.squash {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Unit → m (Nondet m α)) : Nondet m α

Squash a monadic nondeterministic value to a nondeterministic value.

partial def Nondet.bind {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (L : Nondet m α) (f : α → Nondet m β) : Nondet m β

Bind a nondeterministic function over a nondeterministic value, ensuring the function is run with the relevant backtrackable state at each value.

def Nondet.singletonM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : m α) : Nondet m α

Convert any value in the monad to the singleton nondeterministic value.

def Nondet.singleton {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : α) : Nondet m α

Convert a value to the singleton nondeterministic value.

instance Nondet.instMonadNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : Monad (Nondet m)

Nondet m is a monad.

instance Nondet.instAlternativeNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : Alternative (Nondet m)

Nondet m is an alternative monad.

instance Nondet.instMonadLiftNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : MonadLift m (Nondet m)

def Nondet.ofListM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : List (m α)) : Nondet m α

Lift a list of monadic values to a nondeterministic value. We ensure that each monadic value is evaluated with the same backtrackable state.

def Nondet.ofList {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : List α) : Nondet m α

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.)

def Nondet.mapM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → m β) (L : Nondet m α) : Nondet m β

Apply a function which returns values in the monad to every alternative of a Nondet m α.

def Nondet.map {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → β) (L : Nondet m α) : Nondet m β

Apply a function to each alternative in a Nondet m α .

def Nondet.ofOptionM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : m (Option α)) : Nondet m α

Convert a monadic optional value to a nondeterministic value.

def Nondet.ofOption {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : Option α) : Nondet m α

Convert an optional value to a nondeterministic value.

def Nondet.filterMapM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → m (Option β)) (L : Nondet m α) : Nondet m β

Filter and map a nondeterministic value using a monadic function which may return none.

def Nondet.filterMap {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → Option β) (L : Nondet m α) : Nondet m β

Filter and map a nondeterministic value.

def Nondet.filterM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (p : α → m (ULift Bool)) (L : Nondet m α) : Nondet m α

Filter a nondeterministic value using a monadic predicate.

def Nondet.filter {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (p : α → Bool) (L : Nondet m α) : Nondet m α

Filter a nondeterministic value.

partial def Nondet.iterate {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (f : α → Nondet m α) (a : α) : Nondet m α

All iterations of a non-deterministic function on an initial value.

(That is, depth first search.)

def Nondet.head {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} [Alternative m] (L : Nondet m α) : m α

Find the first alternative in a nondeterministic value, as a monadic value.

def Nondet.firstM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} [Alternative m] (L : Nondet m α) (f : α → m (Option β)) : m β

Find the value of a monadic function on the first alternative in a nondeterministic value where the function succeeds.

def Nondet.toMLList' {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : MLList m α

Convert a non-deterministic value into a lazy list, by discarding the backtrackable state.

def Nondet.toList {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : m (List (α × σ))

Convert a non-deterministic value into a list in the monad, retaining the backtrackable state.

def Nondet.toList' {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : m (List α)

Convert a non-deterministic value into a list in the monad, by discarding the backtrackable state.

instance instMonadBacktrackUnitId : Lean.MonadBacktrack Unit Id

The Id monad is trivially backtrackable, with state Unit.