Search code examples
haskellcontinuations

Anything wrong with this simpler bind for Cont?


{-# 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

Solution

  • 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.