[Top] [All Lists]

## RE: [Haskell-cafe] Re: no sparks?

 Subject: RE: [Haskell-cafe] Re: no sparks? "Sittampalam, Ganesh" Mon, 21 Dec 2009 17:07:20 -0000
 \a b -> Left a `amb` Right b From: [email protected] [mailto:[email protected]] On Behalf Of Jamie MorgensternSent: 21 December 2009 16:50To: Benedikt HuberCc: [email protected]Subject: [Haskell-cafe] Re: no sparks? 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. I've been thinking about this problem generally, not just in the Haskell setting. It makes sense (in the very least, with theorem proving)to allow  a p|| b to return the value of a or b, whichever returns first, wrapped in a constructor which would allow you to case analyze which result returnedcase (a p|| b) of  (1, Xa) = ... (2, Xb) = ... On Sun, Dec 20, 2009 at 8:52 PM, Benedikt Huber wrote: Daniel Fischer schrieb: Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern: Hello; 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, returnseither, whichever computation returns first. This wouldn't be easy to reconcile with referential transparency.You can do that in IO, roughlym <- newEmptyMVart1 <- forkIO \$ method1 >>= putMVar mt2 <- forkIO \$ method2 >>= putMVar mrs <- takeMVar mkillThread t1killThread t2return rsAnd 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 likesolve :: Ctx -> Prop -> Int -> IO (Maybe Proof)solve ctx goal n = amb leftRight rightLeft where   leftRight = m1 `mplus` m2   rightLeft = m2 `mplus` m1    m1 = (tryRight ctx goal n)   m2 = (tryLeft ctx goal n)I think the idea of directly supporting this kind of thing is quite interesting.benedikt ==============================================================================Please access the attached hyperlink for an important electronic communications disclaimer:http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html============================================================================== ```_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe ```