<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META http-equiv=Content-Type content="text/html; charset=us-ascii">
<META content="MSHTML 6.00.2900.3603" name=GENERATOR></HEAD>
<BODY>
<DIV dir=ltr align=left><SPAN class=132540617-21122009><FONT face=Arial 
color=#800000 size=2>\a b -&gt; Left a `amb` Right b</FONT></SPAN></DIV><BR>
<DIV class=OutlookMessageHeader lang=en-us dir=ltr align=left>
<HR tabIndex=-1>
<FONT face=Tahoma size=2><B>From:</B> haskell-cafe-bounces@haskell.org 
[mailto:haskell-cafe-bounces@haskell.org] <B>On Behalf Of </B>Jamie 
Morgenstern<BR><B>Sent:</B> 21 December 2009 16:50<BR><B>To:</B> Benedikt 
Huber<BR><B>Cc:</B> haskell-cafe@haskell.org<BR><B>Subject:</B> [Haskell-cafe] 
Re: no sparks?<BR></FONT><BR></DIV>
<DIV></DIV>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't return 
the same proof and so we can't really use it here. <BR><BR>I'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>&nbsp;<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>&nbsp;(1, Xa) = ...<BR>&nbsp;(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="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">Daniel 
  Fischer schrieb:<BR>
  <BLOCKQUOTE class=gmail_quote 
  style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
    <DIV class=im>Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie 
    Morgenstern:<BR></DIV>
    <BLOCKQUOTE class=gmail_quote 
    style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">Hello;<BR><BR>
      <DIV class=im>Also, I was wondering if something akin to a "parallel or" 
      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'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>&nbsp;where<BR>&nbsp; &nbsp;leftRight = m1 `mplus` m2<BR>&nbsp; 
  &nbsp;rightLeft = m2 `mplus` m1
  <DIV class=im><BR>&nbsp; &nbsp;m1 = (tryRight ctx goal n)<BR>&nbsp; &nbsp;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></BODY></HTML>
<BR/><!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"><html><p class=MsoNormal><span lang=EN-US style='font-size:8.0pt;font-family:Courier'>==============================================================================<br>Please access the attached hyperlink for an important electronic communications disclaimer:<br><a href="http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html">http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html</a><br>==============================================================================<o:p></o:p></span></p></html><br>