Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
Just a short note to show how the 3 evaluation orders can be written in a very symmetric manner: o...@okmij.org wrote these as: In call-by-name, we have lam f = S . return $ (unS . f . S) In call-by-value, we have lam f = S . return $ (\x - x = unS . f . S . return) In call-by-need, we have lam f = S . return $ (\x - share x = unS . f . S) These can be rewritten as call-by-name (eta-expanded and application made visible): lam f = S . return $ (\x - unS . f . S $ x) call-by-value (flip) lam f = S . return $ (\x - unS . f . S . return = x) call-by-need (flip) lam f = S . return $ (\x - unS . f . S = share x ) This pushes us to write two helper functions: execS :: (IO a - IO b) - IO a - IO b execS g x = g = share x execM :: Monad m = (m a - m b) - m a - m b execM g x = g . return = x And now, with the magic of slices, we can truly display those 3 in highly symmetric fashion: call-by-name: lam f = S . return $ ((unS . f . S) $) call-by-value (flip) lam f = S . return $ ((unS . f . S) `execM`) call-by-need (flip) lam f = S . return $ ((unS . f . S ) `execS`) (the redundant $ is left in to make the symmetry explicit) And now we see the pattern: lam f = wrap . lift $ ((unwrap . f . wrap) `apply`) where the names above are meant to be suggestive rather than 'actual' names. Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
On Thu, Oct 08, 2009 at 12:54:14AM -0700, o...@okmij.org wrote:
Actually it is possible to implement all three evaluation orders
within the same final tagless framework, using the same interpretation
of types and reusing most of the code save the semantics of lam. That
is where the three orders differ, by their own definition.
That's really nice, Oleg, thanks! I just wanted to comment that
I'd prefer to write
share :: IO a - IO (IO a)
share m = mdo r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
which unfortunately needs {-# LANGUAGE RecursiveDo #-} or
some ugliness from mfix
share :: IO a - IO (IO a)
share m = do r - mfix $ \r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
Thanks,
--
Felipe.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
On Fri, Oct 9, 2009 at 11:12 AM, Felipe Lessa felipe.le...@gmail.com wrote:
On Thu, Oct 08, 2009 at 12:54:14AM -0700, o...@okmij.org wrote:
Actually it is possible to implement all three evaluation orders
within the same final tagless framework, using the same interpretation
of types and reusing most of the code save the semantics of lam. That
is where the three orders differ, by their own definition.
That's really nice, Oleg, thanks! I just wanted to comment that
I'd prefer to write
share :: IO a - IO (IO a)
share m = mdo r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
which unfortunately needs {-# LANGUAGE RecursiveDo #-} or
some ugliness from mfix
share :: IO a - IO (IO a)
share m = do r - mfix $ \r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
Alternatively,
share m = do
r - newIORef undefined
writeIORef r $ do
x - m
writeIORef r (return x)
return x
return $ readIORef r = id
Which is basically the same as your version, but only needs one IORef.
--
Dave Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
On Fri, Oct 09, 2009 at 01:27:57PM -0400, David Menendez wrote:
On Fri, Oct 9, 2009 at 11:12 AM, Felipe Lessa felipe.le...@gmail.com wrote:
That's really nice, Oleg, thanks! I just wanted to comment that
I'd prefer to write
share :: IO a - IO (IO a)
share m = mdo r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
which unfortunately needs {-# LANGUAGE RecursiveDo #-} or
some ugliness from mfix
share :: IO a - IO (IO a)
share m = do r - mfix $ \r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
Alternatively,
share m = do
r - newIORef undefined
writeIORef r $ do
x - m
writeIORef r (return x)
return x
return $ readIORef r = id
Which is basically the same as your version, but only needs one IORef.
Hmmm, but my version also needs only one IORef, right? In fact I
first wrote the same code as yours but I've frowned upon the need
of having that 'undefined' and an extra 'writeIORef'.
Thanks,
--
Felipe.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
On Fri, Oct 9, 2009 at 1:39 PM, Felipe Lessa felipe.le...@gmail.com wrote:
On Fri, Oct 09, 2009 at 01:27:57PM -0400, David Menendez wrote:
On Fri, Oct 9, 2009 at 11:12 AM, Felipe Lessa felipe.le...@gmail.com wrote:
That's really nice, Oleg, thanks! I just wanted to comment that
I'd prefer to write
share :: IO a - IO (IO a)
share m = mdo r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
which unfortunately needs {-# LANGUAGE RecursiveDo #-} or
some ugliness from mfix
share :: IO a - IO (IO a)
share m = do r - mfix $ \r - newIORef (do x - m
writeIORef r (return x)
return x)
return (readIORef r = id)
Alternatively,
share m = do
r - newIORef undefined
writeIORef r $ do
x - m
writeIORef r (return x)
return x
return $ readIORef r = id
Which is basically the same as your version, but only needs one IORef.
Hmmm, but my version also needs only one IORef, right? In fact I
first wrote the same code as yours but I've frowned upon the need
of having that 'undefined' and an extra 'writeIORef'.
It's in the implementation of mfix for IO. From System.IO,
fixIO :: (a - IO a) - IO a
fixIO k = do
ref - newIORef (throw NonTermination)
ans - unsafeInterleaveIO (readIORef ref)
result - k ans
writeIORef ref result
return result
If we inline that into your definition, we get
share m = do
ref - newIORef (throw NonTermination)
ans - unsafeInterleaveIO (readIORef ref)
r - newIORef $ do { x - m; writeIORef ans (return x); return x }
writeIORef ref r
return (readIORef r = id)
So behind the scenes, the mfix version still creates an IORef with
undefined and has an extra writeIORef.
It also has that unsafeInterleaveIO, but I don't think there's any way
that can cause a problem.
Incidentally, none of the versions of share discussed so far are
thread-safe. Specifically, if a second thread starts to evaluate the
result of share m while the first thread is still evaluating m, we end
up with the effects of m happening twice. Here's a version that avoids
this by using a semaphore.
share m = do
r - newIORef undefined
s - newMVar False
writeIORef r $ do
b - takeMVar s
if b
then do
putMVar s True
readIORef r = id
else do
x - m
writeIORef r (return x)
putMVar s True
return x
return $ readIORef r = id
In the worst case, MVar will get read at most once per thread, so the
overhead is limited. Under normal circumstances, the MVar will be read
once and then discarded.
--
Dave Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
Felipe Lessa wrote:
which unfortunately needs {-# LANGUAGE RecursiveDo #-} or
some ugliness from mfix
But mdo/mfix is awesome! :-(
Martijn.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CBN, CBV, Lazy in the same final tagless framework
Actually it is possible to implement all three evaluation orders
within the same final tagless framework, using the same interpretation
of types and reusing most of the code save the semantics of lam. That
is where the three orders differ, by their own definition.
In call-by-name, we have
lam f = S . return $ (unS . f . S)
In call-by-value, we have
lam f = S . return $ (\x - x = unS . f . S . return)
In call-by-need, we have
lam f = S . return $ (\x - share x = unS . f . S)
In CBV, the function first evaluates its argument, whether the value
will be needed or not. In call-by-need, we arrange for the sharing of
the result should the computation be evaluated.
Here is an illustrative test
t2 :: HOAS exp = exp IntT
t2 = (lam $ \z - lam $ \x - let_ (x `add` x)
$ \y - y `add` y) `app` (int 100 `sub` int 10)
`app` (int 5 `add` int 5)
t2SN = runName t2 = print
{-
*CB t2SN
Adding
Adding
Adding
Adding
Adding
Adding
Adding
40
-}
In CBN, the result of subtraction was not needed, and so it was not performed
OTH, (int 5 `add` int 5) was computed four times.
t2SV = runValue t2 = print
{-
*CB t2SV
Subtracting
Adding
Adding
Adding
40
-}
In CBV, although the result of subtraction was not needed, it was
still performed. OTH, (int 5 `add` int 5) was computed only once.
t2SL = runLazy t2 = print
{-
*CB t2SL
Adding
Adding
Adding
40
-}
Now, Lazy is better than both CBN and CBV: subtraction was not needed,
and it was not performed. All other expressions were needed, and
evaluated once.
The complete code is at
http://okmij.org/ftp/tagless-final/CB.hs
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
