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