[Haskell-cafe] Re: no sparks?

[Sittampalam, Ganesh]

\a b -> Left a `amb` Right b

________________________________

From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Jamie Morgenstern
Sent: 21 December 2009 16:50
To: Benedikt Huber
Cc: haskell-cafe at haskell.org
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 returned

case (a p|| b) of 
 (1, Xa) = ...
 (2, Xb) = ...



On Sun, Dec 20, 2009 at 8:52 PM, Benedikt Huber <benjovi at gmx.net> 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, 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
		


	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
	
	solve :: 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 
 =============================================================================== 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091221/793d01b3/attachment.html