std::control::nondet

The nondet module provides nondeterminism through the nondet algebraic effect.

use std::control::nondet::*

The effect

pub act nondet:
    pub branch: () -> bool
    pub reject: () -> never

branch makes a binary choice; reject prunes the current branch. Higher-level helpers below are built on top of these.

each

(each [1, 2, 3]).list   // [1, 2, 3]
(each 1..).once         // opt::just 1

each xs returns one element of xs, signalling its choice through the nondet effect. xs can be any value implementing Fold (lists, ranges, …).

guard

{
    guard: true
    "kept"
}.once

{
    guard (1 == 1)
    "kept"
}.once

When the condition is false, guard calls reject and prunes the current branch.

Collectors

Collectors are written as method calls on a nondeterministic expression:

Method	Result type	Description
.list	list 'a	All results, in branch order
.logic	list 'a	All results with breadth-first scheduling (suitable for infinite branches)
.once	opt 'a	First result if any, otherwise nil

Each collector handles branch and reject, removing the nondet effect from the type.

Example: Pythagorean triples

{
    my a = each 1..
    my b = each a<..
    my c = each b<..

    guard: a * a + b * b == c * c

    (a, b, c)
} .once

The result is just (3, 4, 5).

The same search can use three independent each 1.. choices and guard: a <= b / guard: b <= c, but the bounded form above is friendlier to the current VM and to browser Wasm stacks.

Junctions

The companion module std::control::junction exposes all xs and any xs. They are not part of nondet, but they share the same theme — they wrap a collection so a single comparison covers every element via the junction effect:

if all [1, 2, 3] < any [2, 3, 4]:
    1
else:
    0

all/any are reachable through the prelude.