Wednesday, May 03, 2006

Backtracking

Well, STM's retry is so to say pessimistic - it restarts the whole transaction (up to "atomically" or "orElse") instead of backtracking a single step (one "bind").

Using (simple) backtracking can be inefficient. As an example, consider again a binary join, which succeeds if both its inputs succeed:

join [([], []), ([1], []), ([1], [2]), ([1, 3], [2, 4])] = [([1],[2]),([1],[2]),([1],[4]),([3],[2]),([3],[4])]

It can be implemented for any MonadPlus, but there is some inefficiency there:

join :: MonadPlus m => m (m a, m b) -> m (m a, m b)
join sab = do
(sa, sb) <- sab
a <- sa
b <- sb -- failure on this unneccesary retries sa, should retry sab
return (return a, return b)

What's worse, there is also a difference in semantics. Consider a shocking example, which fails to terminate:

join [(repeat 1, []), (repeat 1, [2])] = ⊥

This would produce a single answer, and THEN fail to terminate, if it retried sab after failing to read sb:

join [(repeat 1, []), (repeat 1, [2])] = [(1, 2), ⊥]


Note that I cannot fix join by simple moving b <- sb before a <- sa, as they are fully symmetric. What I need is a combinator, which unlike bind would execute actions in parallel, and fail AS SOON as any of them fails. Let's say I need a parallel and - pand. Can I code it in terms of MonadPlus? Let us see...
Aha, a quick googling got me A Monadic Semantics for Core Curry.

1 comment:

Andris Birkmanis said...

Aha, they used a kind of CPS to implement a scheduler of branches of "parallel and".
While fixing the semantical problem, this is still quite inefficient solution for "join".
Probably I need to re-read Truly concurrent constraint programming (http://citeseer.ist.psu.edu/gupta96truly.html).