[Haskell-cafe] Re: Parsers are monadic?

[Jonathan Cast]

On Monday 02 July 2007, apfelmus wrote:
> apfelmus wrote:
> >   class DiMonad m where
> >     returnR :: a -> m e a
> >     bindR   :: m e a -> (a -> m e b)  -> m e b
> >
> >     returnL :: e -> m e a
> >     bindL   :: m e a -> (e -> m e' a) -> m e' a
> >
> >   type TwoCont e a = (e -> R) -> (a -> R) -> R
> >
> > A final question remains: does the dimonad abstraction cover the full
> > power of TwoCont? I mean, it still seems like there's an operation
> > missing that supplies new left and right continuations at once.
>
> I think that this missing operation is
>
>   bind2 :: m e a -> (e -> m e' a') -> (a -> m e' a') -> m e' a'
>
> It executes the second or the third argument depending on whether the
> first argument is a failure or a success.
>
> First, bind2 can be defined for TwoCont
>
>  bind2 m fe fa = \e' a' -> m (\e -> (fe e) e' a') (\a -> (fa a) e' a')
>
> Apparently, bindL and bindR can be expressed with bind2
>
>   bindL m f = bind2 m f returnR
>   bindR m f = bind2 m returnL f
>
> The question is whether bind2 can be expressed by bindL and bindR or
> whether bind2 offers more than both. It turns out that bind2 can be
> formulated from bindL and bindR alone
>
>   fmapR f m = m `bindR` returnR . f
>   bind2 m fe fa =
>      ((Left `fmapR` m) `bindL` (\e -> Right `fmapR` fe e))
>     `bindR`
>      (\aa' -> case aa' of
>          Left  a  -> fa a
>          Right a' -> returnR a')

Exactly.

> The definitions is rather cumbersome

As you point out below, try makes it easier:

try a = liftM Right a `catchE` return . Left
bind2 m fe fa = try a >>= either fe fa

And, of course, it's not cheating, since try and either are both independently 
useful in their own rights.

And if you want to eliminate try, it's still a one-liner:

bind2 m fe fa = (liftM Right a `catchE` return . Left) >>= either fe fa

is still a one-line (71 characters), and

bind2 m fe fa = join (liftM fa a `catchE` return . fe)

is even shorter.  (Proof: by a >>= f = join (liftM f a) and natural 
transformations).

> and we omit the proof that both definitions for bind2 are the same for
> TwoConts. 

  try a >>= either fe fa
= \ ke ka -> try a ke (\ x -> either fe fa x ke ka))
= \ ke ka -> (\ ke' ka' -> a (ka' . Left) (ka' . Right))
                ke  (\ x -> either fe fa x ke ka)
= \ ke ka -> a ((\ x -> either fe fa x ke ka) . Left)
               ((\ x -> either fe fa x ke ka) . Right)
= \ ke ka -> a (\ x -> fe x ke ka) (\ x -> fa x ke ka)

Not hard.

> For a general proof, 
> we'd need an axiomatic characterization of dimonads and bind2.

Harder :)  But I think the definition of bind2 above is good enough.  (Is it 
easier to define MonadError axiomatically in terms of throw/try than 
throw/catch?

catch a h = try a >>= either h return
)

<snip>

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs