Thank you for all of the responses! The amb package is something like what I want; though, as aforementioned, the right and left rules won&#39;t return the same proof and so we can&#39;t really use it here. <br><br>I&#39;ve been thinking about this problem generally, not just in the Haskell setting. It makes sense (in the very least, with theorem proving)<br>
to allow <br> <br>a p|| b <br><br>to return the value of a or b, whichever returns first, wrapped in a constructor which would allow you to case analyze which result returned<br><br>case (a p|| b) of <br> (1, Xa) = ...<br>
 (2, Xb) = ...<br><br><br><div class="gmail_quote">On Sun, Dec 20, 2009 at 8:52 PM, Benedikt Huber <span dir="ltr">&lt;<a href="mailto:benjovi@gmx.net">benjovi@gmx.net</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Daniel Fischer schrieb:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="im">
Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern:<br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hello;<br>
<br><div class="im">
Also, I was wondering if something akin to a &quot;parallel or&quot; exists. By this,<br>
I mean I am looking for a function which, given x : a , y : a, returns<br>
either, whichever computation returns first.<br>
</div></blockquote><div class="im">
<br>
This wouldn&#39;t be easy to reconcile with referential transparency.<br>
You can do that in IO, roughly<br>
<br>
m &lt;- newEmptyMVar<br>
t1 &lt;- forkIO $ method1 &gt;&gt;= putMVar m<br>
t2 &lt;- forkIO $ method2 &gt;&gt;= putMVar m<br>
rs &lt;- takeMVar m<br>
killThread t1<br>
killThread t2<br>
return rs<br>
</div></blockquote>
<br>
And in this case (returning (Maybe Proof)), you are not happy with any of the results, but with one of the proofs. So you would need something like<br>
<br>
solve :: Ctx -&gt; Prop -&gt; Int -&gt; IO (Maybe Proof)<br>
solve ctx goal n = amb leftRight rightLeft<br>
  where<br>
    leftRight = m1 `mplus` m2<br>
    rightLeft = m2 `mplus` m1<div class="im"><br>
    m1 = (tryRight ctx goal n)<br>
    m2 = (tryLeft ctx goal n)<br>
<br></div>
I think the idea of directly supporting this kind of thing is quite interesting.<br><font color="#888888">
<br>
benedikt<br>
</font></blockquote></div><br>