[Haskell-cafe] A better, fair, and terminating backtracking monad [Was: Concurrency question]

[Dmitry Vyal]

oleg at pobox.com wrote:

> Dmitry Vyal wrote:
> 
>>Currently I'm playing with theorem-proving using resolution. So I need
>>some technique to break a computation, if takes too long.
> 
> 
> When it comes to resolution proofs, perhaps a better approach is
> to use a better monad that natively offers termination guarantees. For
> example, 
> 
> 	http://pobox.com/~oleg/ftp/Computation/monads.html#fair-bt-stream
> 
> First of all, the monad can let succeed the computations that surely
> diverge in List and similar monads. As the code at the end of that
> file shows, the monad avoids depth-first traps, and can even handle
> left-recursion at the monadic level. Furthermore, the monad has the
> inherent `timing' metric: Incomplete eliminations. Each elimination is
> bounded in time. One can specify the upper bound on the number of
> eliminations and thus force the termination if no solution was found
> thus far. It is possible to modify the run function of the monad to
> return the continuation once the counter has expired. So, one can run
> the monad for a bit more, if desired. In contrast to iterative
> deepening, running the continuation does _not_ repeat any of the
> previous work.

Thanks a lot.
I was seeking for some material about monads in order to understand them better. 
  I've just became studying your article. It promises to be very useful to me.

But it doesn't clear to me, why my first attempt failed. In "Control.Concurrent" 
it's said, that GHC implements preemptive multitasking when there are no tight 
loops without allocations, so my approach should be successful too.

Then I'll start writing some practical programs, I'm sure I'll have to deal with 
concurrency. So it would be great if someone points on my mistakes or 
misunderstandings.

Thanks in advance.