Implementing miniKanren-style logic programming and constraint solving using cloneable continuations.
Turmeric v2 will support multi-shot (cloneable) continuations, enabling backtracking computation. This guide covers the design, use cases, and integration with Turmeric's ownership model.
Backtracking enables a declarative programming style where the system automatically explores alternatives:
| Use Case | Example | Benefit |
|---|---|---|
| Parsing | Parser combinators with choice | Clean, composable grammar definitions |
| Logic Programming | miniKanren-style queries | Bidirectional computation |
| Constraint Solving | Sudoku, SAT solvers | Automatic search with pruning |
| Probabilistic Programming | Bayesian inference | Explore multiple execution paths |
| Game AI | Move exploration | Try strategies, backtrack on failure |
Phase 18 (v1): Continuations are one-shot. Calling continue k v consumes k, matching Turmeric's ownership model but preventing backtracking.
Phase 20+ (v2): Cloneable continuations enable multi-shot by requiring all captured values to implement a Clone trait.
A cloneable continuation can be resumed multiple times:
;; Surface syntax (sugar)
(cloneable-reset
(fn []
body))
(cloneable-shift [k]
body)
Every type captured by a cloneable continuation must implement Clone:
;; Clone primitives (copy semantics)
(instance Clone int64 (clone [x] x))
(instance Clone bool (clone [x] x))
;; Clone derived types (deep copy)
(instance Clone (Pair a b) [Clone a, Clone b]
(clone [x] (Pair (clone x.first) (clone x.second))))
(instance Clone (Vector a) [Clone a]
(clone [x] (map clone x)))
Key invariant: Before a cloneable continuation is resumed, all values in its environment must be cloned. This means:
ref<T> values should be immutable or used carefully.Multi-shot continuations are modeled as the backtracking monad:
;; A computation that yields zero or more results
(defalias Backtrack<a> (-> ((list (-> a)))))
;; Monadic operations
(defn mzero [] : (Backtrack a)
[])
(defn mplus [fs gs : (Backtrack a)] : (Backtrack a)
(fn [] (append (fs) (gs))))
(defn bind [f : (-> a (Backtrack b)) xs : (Backtrack a)] : (Backtrack b)
(fn []
(flat-map (fn [k] ((f (k)) ())) (xs ()))))
(defn return [x : a] : (Backtrack a)
(fn [] [(fn [] x)]))
A backtracking parser tries multiple production rules:
;; Token parser
(defn parse-token [t input]
(if (= (car input) t)
(return (cdr input))
mzero))
;; Choice: try parseA, then parseB if parseA fails
(defn <|> [parseA parseB input]
(mplus (parseA input) (parseB input)))
;; Sequence: parseA then parseB
(defn >> [parseA parseB input]
(bind (fn [rest] (parseB rest))
(parseA input)))
;; Grammar:
;; expr := term ('+' term)*
(defn parse-expr [input]
(<|>
(do-backtrack
(def rest (parse-term input))
(def rest (parse-many (parse-plus rest)))
(return rest))
(parse-term input)))
Relational queries that work in multiple directions:
;; Unification: make two values equal
(defn unify [x y subst]
(cond
[(== x y) (return subst)]
[(lvar? x) (ext-s x y subst)]
[(lvar? y) (ext-s y x subst)]
[(and (pair? x) (pair? y))
(bind (fn [s] (unify (cdr x) (cdr y) s))
(unify (car x) (car y) subst))]
[:else mzero]))
;; Relation: append(x, y, z) :- z = x ++ y
(defn appendo [x y z]
(<|>
;; Base case: x = [], z = y
(bind (fn [s] (unify y z s)) (unify x [] {}))
;; Recursive: x = [h|t], z = [h|r], append(t, y, r)
(bind (fn [s]
(let [h (lvar 'h)
t (lvar 't)
r (lvar 'r)]
(appendo t y r)))
(unify x (cons (lvar 'h) (lvar 't)) {}))))
;; Query: (appendo [1 2] [3 4] X) => X = [1 2 3 4]
(run 1 [x]
(appendo [1 2] [3 4] x))
(defn sudoku [grid]
;; grid is a 9x9 array with some cells filled (1-9), others unbound (lvar)
;; For each cell, either it's already bound or we bind it to 1-9
(defn choose-domain [cell]
(if (lvar? cell)
(choice-point [1 2 3 4 5 6 7 8 9])
(return cell)))
(defn all-different [xs]
;; Constraint: all values in xs must be distinct
(bind (fn [vs]
(if (distinct? vs)
(return vs)
mzero))
(map-backtrack choose-domain xs)))
;; Run constraints: rows, columns, 3x3 boxes all distinct
(do-backtrack
(def filled (map choose-domain grid))
(map all-different (rows filled))
(map all-different (cols filled))
(map all-different (boxes filled))
(return filled)))
;; Solve and get first 10 solutions
(run 10 [solution]
(sudoku initial-grid))
Turmeric's ref<T> assumes linear consumption (move semantics). Cloneable continuations re-execute the captured code, trying to consume the same ref<T> multiple times:
;; ERROR: re-executing code will consume the ref twice
(cloneable-reset
(fn []
(let [r (ref 42)]
(choice-point [1 2])))) ; captures r; next backtrack tries to use r again
Solution: Capture immutable data or use rc<T> for shared ownership:
;; OK: captured value is immutable
(cloneable-reset
(fn []
(let [x 42] ; immutable
(choice-point [1 2]))))
;; OK: shared ownership doesn't consume on re-entry
(cloneable-reset
(fn []
(let [r (rc 42)]
(choice-point [1 2]))))
When a cloneable continuation captures state across a defer boundary, each clone must re-run the deferred cleanup on entry:
;; When backtracking re-enters this block,
;; the file is re-opened in the cloned continuation
(cloneable-reset
(fn []
(defer-with-close (open-file "data.txt")
(fn [f]
(let [data (read f)]
(choice-point (parse data)))))))
This is safe but can be expensive. Prefer immutable snapshots where possible.
;; Delimit a cloneable computation
(cloneable-reset body)
;; Capture continuation for backtracking
(cloneable-shift [k] body)
;; Choice point: try multiple values
(choice-point [v1 v2 ...])
;; Run a backtracking computation, collect N solutions
(run n [vars] body)
;; Run all solutions
(run* [vars] body)
;; Constraint: succeed if predicate holds
(constraint pred)
(return x) ; succeed with one value
(mzero) ; fail (zero solutions)
(mplus fs gs) ; choice between fs and gs
(bind f xs) ; flatMap: sequence computations
;; Syntactic sugar
(do-backtrack
(def x (goal1))
(def y (goal2 x))
(return (list x y)))
Cloning captured environments is expensive for large states. Strategies:
! operator to commit to first solution, preventing unnecessary backtracking.Unlike Prolog's stack-based choice points, Turmeric's cloneable continuations allocate on the heap. This is acceptable for bounded search spaces but may not scale to million-node search trees.