A classic example of a computational effect that isn’t part of most programming languages is nondeterminism. (Prolog has something like it.)

Syntax and examples

Assume that we have lists (TAPL 11.12), including the syntax

      [] ≡ nil
    [t1] ≡ cons t1 nil
[t1, t2] ≡ cons t1 (cons t2 nil)

and so on. We write infix ++ for list concatenation.

The new syntax for nondeterminism is:

t ::= ...
      collect t
      amb t

amb takes a list of n arguments and causes evaluation to fork into n branches, one for each value in the list.

collect collects all the branches and puts their values into a list.

For example, if you have a nickel, a dime, and a quarter, and want to know all the amounts you can pay exactly, it’s

collect ((amb [0, 5]) + (amb [0, 10]) + (amb [0, 25]))
* [0, 25, 10, 35, 5, 30, 15, 40]

If this reminds you of Python’s

[n+d+q for n in [0, 5] for d in [0, 10] for q in [0, 25]]

you’re right. But amb can do some things that would be difficult with list comprehensions, like a function that takes a list of coin values and produces all possible sums:

sums ≡ fix λs. λc. if isnil c then 0 else amb [0, car c] + s (cdr c)
collect (sums [5, 10, 25]) * [0, 25, 10, 35, 5, 30, 15, 40]

Typing and evaluation

      Γ ⊢ t : T
Γ ⊢ collect t : List T

Γ ⊢ t : List T
Γ ⊢ amb t : T

F ::= [⋅]
      F t
      v F
      amb F

E ::= ...
      amb E
      collect E

                   collect v  [v]
collect F[amb [v1, v2, ...]]  collect F[v1] ++ collect F[v2] ++ ...

In pure lambda calculus

We can convert lambda calculus with collect and amb into pure lambda calculus:

𝒯⟦x⟧ = [x]
𝒯⟦nil⟧ = [nil]
𝒯⟦cons⟧ = [cons]

𝒯⟦λx. t⟧ = [λx. 𝒯⟦t⟧]
𝒯⟦t1 t2⟧ = concat (map (λf. concat (map f 𝒯⟦t2⟧)) 𝒯⟦t1⟧)
𝒯⟦amb t⟧ = concat 𝒯⟦t⟧
𝒯⟦collect t⟧ = [𝒯⟦t⟧]

where map and concat have their usual meanings, but for completeness, we can define them as:

map ≡ fix λm. λf. λx. if isnil x then nil else cons (f (car x)) (m f (cdr x))
concat ≡ fix λc. λx. if isnil x then nil else (car x) ++ (c (cdr x))