Fail-back monad

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Fail-back monad

Alberto G. Corona
Hi Haskellers.

In my package MFlow [1] I program an entire web  navigation in a
single procedure. That happened  in the good-old WASH web application
framework.
The problem is the back button in the Browser.
To go back in the code to the previous interactions when the data
input does not match the expected because the user pressed the back
button one or more times, i came across this Monad specimen,: that
solves the problem.


data FailBack a = BackPoint a   -- will go back to this point
                             | NoBack a       . -- Normal outcome
                             | GoBack            -- "exception":: must
go to the last backPoint

newtype BackT m a = BackT { runBackT :: m (FailBack a ) }

-- this monad nas a loop

instance Monad m => Monad (BackT  m) where
    fail   _ = BackT $ return GoBack
    return x = BackT . return $ NoBack x
    x >>= f  = BackT $ loop
     where
     loop = do
        v <- runBackT x
        case v of
            NoBack y  -> runBackT (f y)  -- business as usual
            BackPoint y  -> do
                 z <- runBackT (f y)
                 case z of
                  GoBack  -> loop          -- if x was a backpoint,
then redirects the flow to this backpoint
                  other -> return other
            GoBack -> return  GoBack --propagate the signal back


 This monad does not perform exploration of alternatives as is the
case of MonadPlus instances. It does not perform the kind of
backtracking of "nondeterministic"  three navigations in the Prolog
style. It just go back to the last point where the computation can
restart again in a  sequence of actions.

In this example:


liftBackPoint f= BackT $ f >>= \x -> return $ BackPoint x

test= runBackT $ do
       lift $ print "will not return back here"
        liftBackPoint $ print "will return here"
        n2  &lt;- lift $ getLine
        lift $ print "second input"
        n3  &lt;- lift $  getLine
        if n3 == "back"
                   then  fail ""
                   else lift $ print  $ n2++n3

Whenever the second input is "back" The procedure will go back to
where liftBackPoint is. Otherwise, it will return the concatenation of
the two inputs. If the underlying monad is an instance of MonadState,
it can transport the state that caused the failure to the backpoint.

Are there something similar? May it be functionally equivalent to
something simpler or with more grounds?
 I looked at some exception monads out there, but they did not seems
to share the same idea

[1] http://haskell-web.blogspot.com.es/2012/02/web-application-server-with-stateful.html

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Alberto G. Corona
Sorry, the text example again without HTML formatting:


test= runBackT $ do
       lift $ print "will not return back here"
        liftBackPoint $ print "will return here"
        n2  <- lift $ getLine
        lift $ print "second input"
        n3  <- lift $  getLine
        if n3 == "back"
                   then  fail ""
                   else lift $ print  $ n2++n3


I wrote a blog entry about this :

 http://haskell-web.blogspot.com.es/2012/03/failback-monad.html


2012/3/28 Alberto G. Corona <[hidden email]>:

> Hi Haskellers.
>
> In my package MFlow [1] I program an entire web  navigation in a
> single procedure. That happened  in the good-old WASH web application
> framework.
> The problem is the back button in the Browser.
> To go back in the code to the previous interactions when the data
> input does not match the expected because the user pressed the back
> button one or more times, i came across this Monad specimen,: that
> solves the problem.
>
>
> data FailBack a = BackPoint a   -- will go back to this point
>                             | NoBack a       . -- Normal outcome
>                             | GoBack            -- "exception":: must
> go to the last backPoint
>
> newtype BackT m a = BackT { runBackT :: m (FailBack a ) }
>
> -- this monad nas a loop
>
> instance Monad m => Monad (BackT  m) where
>    fail   _ = BackT $ return GoBack
>    return x = BackT . return $ NoBack x
>    x >>= f  = BackT $ loop
>     where
>     loop = do
>        v <- runBackT x
>        case v of
>            NoBack y  -> runBackT (f y)  -- business as usual
>            BackPoint y  -> do
>                 z <- runBackT (f y)
>                 case z of
>                  GoBack  -> loop          -- if x was a backpoint,
> then redirects the flow to this backpoint
>                  other -> return other
>            GoBack -> return  GoBack --propagate the signal back
>
>
>  This monad does not perform exploration of alternatives as is the
> case of MonadPlus instances. It does not perform the kind of
> backtracking of "nondeterministic"  three navigations in the Prolog
> style. It just go back to the last point where the computation can
> restart again in a  sequence of actions.
>
> In this example:
>
>
> liftBackPoint f= BackT $ f >>= \x -> return $ BackPoint x
>
> test= runBackT $ do
>       lift $ print "will not return back here"
>        liftBackPoint $ print "will return here"
>        n2  &lt;- lift $ getLine
>        lift $ print "second input"
>        n3  &lt;- lift $  getLine
>        if n3 == "back"
>                   then  fail ""
>                   else lift $ print  $ n2++n3
>
> Whenever the second input is "back" The procedure will go back to
> where liftBackPoint is. Otherwise, it will return the concatenation of
> the two inputs. If the underlying monad is an instance of MonadState,
> it can transport the state that caused the failure to the backpoint.
>
> Are there something similar? May it be functionally equivalent to
> something simpler or with more grounds?
>  I looked at some exception monads out there, but they did not seems
> to share the same idea
>
> [1] http://haskell-web.blogspot.com.es/2012/02/web-application-server-with-stateful.html

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Stephen Tetley-2
In reply to this post by Alberto G. Corona
Maybe this is a version of William Harrison's DebugT monad with
rollback, listed in his periodic table of effects?

http://www.cs.missouri.edu/~harrisonwl/Presentations/UIUCFM05.ppt

I've never seen a definition of the monad itself...
http://www.haskell.org/pipermail/beginners/2010-January/003371.html

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Alberto G. Corona
Hi Stephen:

It could be:

It performs a rollback indeed.
 I guess that this monad can be used in something similar to
nonblocking (multilevel)  transactions.

if "GoBack" is changed to "Goback String", and  a trace string is
added to each NoBack step, then each NoBack step could sum the traces
of all the  previous steps. The when GoBack condition is reached, it
can transport back the entire trace of the failed execution. to the
BackPoint


2012/3/28 Stephen Tetley <[hidden email]>:
> Maybe this is a version of William Harrison's DebugT monad with
> rollback, listed in his periodic table of effects?
>
> http://www.cs.missouri.edu/~harrisonwl/Presentations/UIUCFM05.ppt
>
> I've never seen a definition of the monad itself...
> http://www.haskell.org/pipermail/beginners/2010-January/003371.html

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

oleg-30
In reply to this post by Alberto G. Corona

Alberto G. Corona wrote about a monad to set a checkpoint and be able
to repeatedly go to that checkpoint and re-execute the computations
following the checkpoint.
  http://haskell-web.blogspot.com.es/2012/03/failback-monad.html

The typical example is as follows.

> test= runBackT $ do
>        lift $ print "will not return back here"
>         liftBackPoint $ print "will return here"
>         n2  <- lift $ getLine
>         lift $ print "second input"
>         n3  <- lift $  getLine
>         if n3 == "back"
>                    then  fail ""
>                    else lift $ print  $ n2++n3

Let us first consider a slightly simplified problem, with a different
signature for liftBackPoint. Rather than writing
        do
        liftBackPoint $ print "will return here"
        other_computation

we will write

        do
        backPoint $ do
          lift $ print "will return here"
          other_computation

In that case, backPoint will be implemented with the Exception or
Error monad. For example,

> backPoint :: Monad m =>
>   ErrorT SomeException m a -> ErrorT SomeException m a
> backPoint m = catchError m handler
>  where
>  handler e | Just RestartMe <- fromException e = backPoint m
>  handler e = throwError e -- other errors propagate up

We designate one exception RestartMe as initiating the restart from
the checkpoint. Other exceptions will propagate as usual.

Obviously, if we are in IO or some MonadIO, we could use the regular
exception-handling facilities: throw/catch.

Suppose however that marking of the checkpoint should be a single
action rather that exception-like handling form. Then we need the
continuation monad:

> type BackT r m a = ContT r (ErrorT SomeException m) a
>
> backPointC :: Monad m => ContT e (ErrorT SomeException m) ()
> backPointC = ContT (\k -> backPoint (k ()))

(we have re-used the earlier backPoint). Incidentally, the
continuation monad will be faster than BackT in the original article.
Attentive reader must have noticed that backPointC is shift in disguise.

Here is the complete code.

> {-# LANGUAGE DeriveDataTypeable #-}
>
> module BackT where
>
> import Control.Monad.Trans
> import Control.Monad.Error
> import Control.Monad.Cont
> import Control.Exception
> import Data.Typeable
>
>
> data RestartMe = RestartMe deriving (Show, Typeable)
> instance Exception RestartMe
> instance Error SomeException
>
> -- Make a `restartable' exception
> -- (restartable from the beginning, that is)
> -- We redo the computation once we catch the exception RestartMe
> -- Other exceptions propagate up as usual.
>
> -- First, we use ErrorT
>
> backPoint :: Monad m =>
>   ErrorT SomeException m a -> ErrorT SomeException m a
> backPoint m = catchError m handler
>  where
>  handler e | Just RestartMe <- fromException e = backPoint m
>  handler e = throwError e               -- other errors propagate up
>
> test1 = runErrorT $ do
>   lift $ print "will not return back here"
>   backPoint $ do
>     lift $ print "will return here"
>     n2  <- lift $ getLine
>     lift $ print "second input"
>     n3  <- lift $  getLine
>     if n3 == "back"
>        then  throwError (toException RestartMe)
>        else lift $ print  $ n2++n3
>
> -- Obviously we can use error handling in the IO monad...
>
> -- Suppose we don't want backPoint that takes monad as argument.
> -- We wish backPoint that is a simple m () action.
>
> -- We will use Cont monad then: That is, we use Cont + Error Monad
> -- We reuse the old backPoint
>
> type BackT r m a = ContT r (ErrorT SomeException m) a
>
> backPointC :: Monad m => ContT e (ErrorT SomeException m) ()
> backPointC = ContT (\k -> backPoint (k ()))
>
> abort e = ContT(\k -> e)
>
> test2 :: BackT r IO ()
> test2 =  do
>   liftIO $ print "will not return back here"
>   backPointC                            -- This line differs
>   liftIO $ print "will return here"     -- (and the indentation on here)
>   n2  <- liftIO $ getLine
>   liftIO $ print "second input"
>   n3  <- liftIO $  getLine
>   if n3 == "back"
>        then  abort $ throwError (toException RestartMe)
>        else liftIO $ print  $ n2++n3
>
> test2r = runErrorT $ runContT test2 return


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Ross Paterson
In reply to this post by Alberto G. Corona
On Wed, Mar 28, 2012 at 01:34:29AM +0100, Alberto G. Corona  wrote:
> In my package MFlow [1] I program an entire web  navigation in a
> single procedure. That happened  in the good-old WASH web application
> framework.
> The problem is the back button in the Browser.
> To go back in the code to the previous interactions when the data
> input does not match the expected because the user pressed the back
> button one or more times, i came across this Monad specimen,: that
> solves the problem.

This definition does not satisfy the right identity law (m >>= return = m)
included in the monad definition:

*FailBack> BackT [BackPoint 1] >>= return
BackT [NoBack 1]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Alberto G. Corona
In reply to this post by oleg-30
Thaks Oleg for your clarification.
I thoutgh on the use or ErrorT or something similar but the fact is
that i need many bacPoints, not just one. That is, The user can go
many pages back in the navigation pressing many times te back
buttton.,. My code has a failure detection in each backPoint , so the
computation can fail-back to the previous backpoint and so on.  Doing
this with errorT result in a ugly syntax.

2012/3/29  <[hidden email]>:

>
> Alberto G. Corona wrote about a monad to set a checkpoint and be able
> to repeatedly go to that checkpoint and re-execute the computations
> following the checkpoint.
>  http://haskell-web.blogspot.com.es/2012/03/failback-monad.html
>
> The typical example is as follows.
>
>> test= runBackT $ do
>>        lift $ print "will not return back here"
>>         liftBackPoint $ print "will return here"
>>         n2  <- lift $ getLine
>>         lift $ print "second input"
>>         n3  <- lift $  getLine
>>         if n3 == "back"
>>                    then  fail ""
>>                    else lift $ print  $ n2++n3
>
> Let us first consider a slightly simplified problem, with a different
> signature for liftBackPoint. Rather than writing
>        do
>        liftBackPoint $ print "will return here"
>        other_computation
>
> we will write
>
>        do
>        backPoint $ do
>          lift $ print "will return here"
>          other_computation
>
> In that case, backPoint will be implemented with the Exception or
> Error monad. For example,
>
>> backPoint :: Monad m =>
>>   ErrorT SomeException m a -> ErrorT SomeException m a
>> backPoint m = catchError m handler
>>  where
>>  handler e | Just RestartMe <- fromException e = backPoint m
>>  handler e = throwError e             -- other errors propagate up
>
> We designate one exception RestartMe as initiating the restart from
> the checkpoint. Other exceptions will propagate as usual.
>
> Obviously, if we are in IO or some MonadIO, we could use the regular
> exception-handling facilities: throw/catch.
>
> Suppose however that marking of the checkpoint should be a single
> action rather that exception-like handling form. Then we need the
> continuation monad:
>
>> type BackT r m a = ContT r (ErrorT SomeException m) a
>>
>> backPointC :: Monad m => ContT e (ErrorT SomeException m) ()
>> backPointC = ContT (\k -> backPoint (k ()))
>
> (we have re-used the earlier backPoint). Incidentally, the
> continuation monad will be faster than BackT in the original article.
> Attentive reader must have noticed that backPointC is shift in disguise.
>
> Here is the complete code.
>
>> {-# LANGUAGE DeriveDataTypeable #-}
>>
>> module BackT where
>>
>> import Control.Monad.Trans
>> import Control.Monad.Error
>> import Control.Monad.Cont
>> import Control.Exception
>> import Data.Typeable
>>
>>
>> data RestartMe = RestartMe deriving (Show, Typeable)
>> instance Exception RestartMe
>> instance Error SomeException
>>
>> -- Make a `restartable' exception
>> -- (restartable from the beginning, that is)
>> -- We redo the computation once we catch the exception RestartMe
>> -- Other exceptions propagate up as usual.
>>
>> -- First, we use ErrorT
>>
>> backPoint :: Monad m =>
>>   ErrorT SomeException m a -> ErrorT SomeException m a
>> backPoint m = catchError m handler
>>  where
>>  handler e | Just RestartMe <- fromException e = backPoint m
>>  handler e = throwError e               -- other errors propagate up
>>
>> test1 = runErrorT $ do
>>   lift $ print "will not return back here"
>>   backPoint $ do
>>     lift $ print "will return here"
>>     n2  <- lift $ getLine
>>     lift $ print "second input"
>>     n3  <- lift $  getLine
>>     if n3 == "back"
>>        then  throwError (toException RestartMe)
>>        else lift $ print  $ n2++n3
>>
>> -- Obviously we can use error handling in the IO monad...
>>
>> -- Suppose we don't want backPoint that takes monad as argument.
>> -- We wish backPoint that is a simple m () action.
>>
>> -- We will use Cont monad then: That is, we use Cont + Error Monad
>> -- We reuse the old backPoint
>>
>> type BackT r m a = ContT r (ErrorT SomeException m) a
>>
>> backPointC :: Monad m => ContT e (ErrorT SomeException m) ()
>> backPointC = ContT (\k -> backPoint (k ()))
>>
>> abort e = ContT(\k -> e)
>>
>> test2 :: BackT r IO ()
>> test2 =  do
>>   liftIO $ print "will not return back here"
>>   backPointC                            -- This line differs
>>   liftIO $ print "will return here"     -- (and the indentation on here)
>>   n2  <- liftIO $ getLine
>>   liftIO $ print "second input"
>>   n3  <- liftIO $  getLine
>>   if n3 == "back"
>>        then  abort $ throwError (toException RestartMe)
>>        else liftIO $ print  $ n2++n3
>>
>> test2r = runErrorT $ runContT test2 return
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Alberto G. Corona
In reply to this post by Ross Paterson
But, on my side,
 BackT [BackPoint 1]
 and
 BackT [NoBack 1]

can be made indistinguishable outside the code where the monad is
defined.  Probably the effect required is not possible without
breaking the law

2012/3/31 Ross Paterson <[hidden email]>:

> On Wed, Mar 28, 2012 at 01:34:29AM +0100, Alberto G. Corona  wrote:
>> In my package MFlow [1] I program an entire web  navigation in a
>> single procedure. That happened  in the good-old WASH web application
>> framework.
>> The problem is the back button in the Browser.
>> To go back in the code to the previous interactions when the data
>> input does not match the expected because the user pressed the back
>> button one or more times, i came across this Monad specimen,: that
>> solves the problem.
>
> This definition does not satisfy the right identity law (m >>= return = m)
> included in the monad definition:
>
> *FailBack> BackT [BackPoint 1] >>= return
> BackT [NoBack 1]
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

oleg-30
In reply to this post by Alberto G. Corona

> I thoutgh on the use or ErrorT or something similar but the fact is
> that i need many bacPoints, not just one. That is, The user can go
> many pages back in the navigation pressing many times te back
> buttton.

The approach in the previous message extends to an arbitrary,
statically unknown number of checkpoints. If we run the following
simple code

> test1 = loop "" 1
>  where
>  loop acc n = inquire ("Enter string " ++ show n) >>= check acc n
>  check acc n ""  = liftIO . putStrLn $ "You have entered: " ++ acc
>  check acc n str = loop (acc ++ str) (n+1)
>
> test1r = runContT test1 return

we can do the following:

    *BackT> test1r
    Enter string 1
    s1
    Enter string 2
    s2
    Enter string 3
    s3
    Enter string 4
    s4
    Enter string 5
    back
    Enter string 4
    back
    Enter string 3
    back
    Enter string 2
    x1
    Enter string 3
    x2
    Enter string 4
    x3
    Enter string 5
    back
    Enter string 4
    y3
    Enter string 5

    You have entered: s1x1x2y3

I decided to go back after the fourth string, but you should feel free
to go forth.

The ContT approach is very flexible: we can not only go back, or go
back more. We can go all the way back. We can go back to the point
where certain condition was true, like when the value of the certain
named field was entered or certain value was computed.

Here is the complete code. For a change, it uses IO exceptions rather
than ErrorT.

> {-# LANGUAGE DeriveDataTypeable #-}
>
> module BackT where  
>
> import Control.Monad.Trans
> import Control.Monad.Cont
> import Control.Exception
> import Data.Typeable
> import Prelude hiding (catch)
>
> data RestartMe = RestartMe deriving (Show, Typeable)
> instance Exception RestartMe
>
> -- Make a `restartable' exception
> -- (restartable from the beginning, that is)
> -- We redo the computation once we catch the exception RestartMe
> -- Other exceptions propagate up as usual.
>
> type BackT r m a = ContT r m a
> abort e = ContT(\k -> e)
>
> -- Send a prompt, receive a reply. If it is "back", go to the
> -- previous checkpoint.
> type Prompt = String
> inquire :: Prompt -> BackT r IO String
> inquire prompt = ContT loop
>  where
>  loop k = exchange >>= checkpoint k
>  exchange = do
>             putStrLn prompt
>             r <- getLine
>             if r == "back" then throw RestartMe
>                else return r
>  checkpoint k r = k r `catch` (\RestartMe -> loop k)
>
> -- Go to the previous checkpoint
> goBack :: BackT r m a
> goBack = abort (throw RestartMe)
>
>
> test1 = loop "" 1
>  where
>  loop acc n = inquire ("Enter string " ++ show n) >>= check acc n
>  check acc n "" = liftIO . putStrLn $ "You have entered: " ++ acc
>  check acc n str = loop (acc ++ str) (n+1)
>
> test1r = runContT test1 return



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Fail-back monad

Stephen Tetley-2
In reply to this post by Stephen Tetley-2
There is also recent work by Aaron Turon and Olin Shivers - Modular
Rollback through Control Logging

http://www.ccs.neu.edu/home/shivers/
http://www.ccs.neu.edu/home/turon/

Note that as well as the paper on Olin Shivers's site there is a more
recent monadic presentation on Aaron Turon's site with Conor
McBride...


On 28 March 2012 18:11, Stephen Tetley <[hidden email]> wrote:
> Maybe this is a version of William Harrison's DebugT monad with
> rollback, listed in his periodic table of effects?
>
> http://www.cs.missouri.edu/~harrisonwl/Presentations/UIUCFM05.ppt
>
> I've never seen a definition of the monad itself...
> http://www.haskell.org/pipermail/beginners/2010-January/003371.html

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe