[Haskell-cafe] no sparks?
Daniel Fischer
daniel.is.fischer at web.de
Sun Dec 20 18:39:06 EST 2009
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
More information about the Haskell-Cafe
mailing list