[Haskell-cafe] Re: Parsers are monadic?
Jonathan Cast
jcast at ou.edu
Mon Jul 2 11:01:23 EDT 2007
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
More information about the Haskell-Cafe
mailing list