Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:
Hello;
I am writing a parallel theorem prover using Haskell, and I am trying to do several things. As a first cut, I want to try using the par construct to attempt right and left rules simultaneously, and to evaluate both branches of an and clause in parallel. My code (attached) does not seem to generate sparks, however. When I run
./proposition +RTS -N2 -sstderr
I get that no sparks are created. What am I doing wrong?
findProof ctx goal n = maybe where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) m = m1 `par` m2 maybe = (m1 `mplus` m2) You never use m, so no threads are sparked. Put the par where it will actually be used: findProof ctx goal n = m2 `par` (m1 `mplus` m2) where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) and you get sparks (5 (4 converted, 0 pruned)). You know that you get a pattern match error due to incomplete patterns in tryLeftHelper, though, do you?
Also, I was wondering if something akin to a "parallel or" exists. By this, I mean I am looking for a function which, given x : a , y : a, returns either, whichever computation returns first.
This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs But in pure code, I think not.
Can I use strategies to code up something like this? I suppose this doesn't play nicely with the idea of determinism, but thought it might be worth asking anyway.
Thanks, -Jamie