Anything wrong with this simpler bind for Cont?

81 Views Asked by At
{-# LANGUAGE RankNTypes #-}

newtype C a = C {runCont :: forall r. (a -> r) -> r} 

instance Functor C where  
  fmap f (C arr) = C $ \br -> arr $ br . f

instance Applicative C where
  pure a = C ($ a)
  (C abrr) <*> (C arr) = C $ \brr -> abrr ( \ab -> arr ( brr . ab ) )

instance Monad C where 
  -- (C arr) >>= aCbrr = C $ \br -> arr (\a -> runCont (aCbrr a) br) -- The usual
  (C arr) >>= aCbrr = arr aCbrr -- My simpler idea with the same result in this test

main :: IO ()
main = print $ flip runCont id $ do
  x <- pure (5::Int)
  y <- pure $ 2 * x
  z <- pure $ take y $ repeat 'a'
  pure z

Upon Noughtmare's suggestion adding some law proofs. I think they make sense intuitively but the commented steps might not be formally sound:

Left identity: pure a >>= h === h a

pure a >>= h
C (\k -> k a) >>= h
(\k -> k a) h
h a

Right identity: m >>= pure === m

m >>= pure
C arr >>= pure
arr pure
arr ( \a -> C (\k -> k a) )
C ( \k -> k (arr id) ) -- because arr knows nothing about r
C arr -- because arr::(a->r)->r so k::a->r
m

Associativity: 

(m >>= f) >>= g         ===    m >>= (\x -> f x >>= g)
((C arr) >>= f) >>= g   ===    (C arr) >>= (\x -> f x >>= g)
(arr f) >>= g          
f (arr id) >>= g
(pure.h) (arr id) >>= g ===    (C arr) >>= (\x -> (pure.h) x >>= g)
C (h (arr id)) >>= g    ===    arr ( \x -> (C (h x)) >>= g )
                        ===    C (h (arr id)) >>= g
1

There are 1 best solutions below

1
K. A. Buhr On BEST ANSWER

Your modified definition works fine (except I don't know how you got flip runCont to type check -- I think you need to flip the arguments manually). However, I also think you'll find that your continuation monad isn't very useful.

The usual continuation monad is a rank-1 type:

newtype C' r a = C' { runCont' :: (a -> r) -> r }

and it's useful because a C' r a is "almost isomorphic" to an a value, except that the type r is known. This means that you can construct a monadic value of type C' Int Char representing a pure Char:

C' (\f -> f 'A')   -- same as `pure 'A'`

but you can also construct a monadic value of the same type C' Int Char that short circuits the computation with an Int return value:

C' (\f -> 42)

In constrast, your rank-2 continuation monad:

newtype C a = C { runCont :: forall r. (a -> r) -> r }

is precisely isomorphic to type a. One direction of the isomorphism is given by pure, and the other is given by:

unpure :: C a -> a
unpure (C f) = f id

So, with your C Char, you can represent a pure Char:

C (\f -> f 'A')    -- equivalent to `pure 'A'`

and that's it.

Because of this isomorphism, your arr is always equal to the section ($ a0) for some a0 :: a, and your aCbrr is always equal to \a' -> C ($ f a') for some f :: a -> b, and this means that the original definition of >>= gives:

(C arr) >>= aCbrr 
-- by original definition of `>>=`
= C $ \br -> arr (\a -> runCont (aCbrr a) br)
-- by the above equivalencies
= C $ \br -> ($ a0) (\a -> runCont ((\a' -> C ($ f a')) a) br)
-- and simplify
= C $ \br -> ($ a0) (\a -> runCont (C ($ f a)) br)
= C $ \br -> (\a -> runCont (C ($ f a)) br) a0
= C $ \br -> runCont (C ($ f a0)) br
= C $ \br -> ($ f a0) br
= C ($ f a0)

while your modified definition of >>= gives

(C arr) >>= aCbrr
-- by your definition of `>>=`
= arr aCbrr
-- by the above equivalencies
= ($ a0) (\a' -> C ($ f a'))
-- and simplify
= (\a' -> C ($ f a')) a0
= C ($ f a0)

so the two definitions are equivalent.