Clarity on Implementation of Continuation Monad Instance

Question

Below is the code sample I tried for Continuation Monad

newtype Cont r a = Cont { rC :: (a -> r) -> r }

instance Functor (Cont r) where
  fmap :: (a -> b) -> Cont r a -> Cont r b
  fmap f (Cont aCont) = Cont $ \k -> aCont (\a -> k (f a))

instance Applicative (Cont r) where
  pure :: a -> Cont r a
  pure a = Cont $ \k -> k a

  (<*>) :: Cont r (a -> b) -> Cont r a -> Cont r b
  Cont fCont <*> Cont aCont = Cont $ \k -> fCont (\f -> aCont (\a -> k (f a)))

instance Monad (Cont r) where
  return = pure

  (>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
  Cont aCont >>= f = Cont $ \k -> rC (aCont (\a -> f a)) (\b -> k b)
  -- f a :: Cont r b
  -- aCont :: (a -> r) -> r
  -- t = aCont (\a -> f a) :: Cont r b
  -- t' = rc t :: (b -> r) -> r
  -- k :: b -> r
  -- t' (\b -> k b) -> r

This is Failing with below error

<interactive>:158:52: error:
    * Occurs check: cannot construct the infinite type: r ~ Cont r b
    * In the expression: f a
      In the first argument of `aCont', namely `(\ a -> f a)'
      In the first argument of `rC', namely `(aCont (\ a -> f a))'
    * Relevant bindings include
        k :: b -> r (bound at <interactive>:158:30)
        f :: a -> Cont r b (bound at <interactive>:158:18)
        aCont :: (a -> r) -> r (bound at <interactive>:158:8)
        (>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
          (bound at <interactive>:158:14)

And when I changed the bind code as below it worked. Please help me with the type error.

  (>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
  Cont aCont >>= f = Cont $ \k -> aCont (\a -> rC (f a) (\b -> k b))

Answer 1

It looks to me like you were simply getting confused - which I find very easy to do with continuations!

This definition:

newtype Cont r a = Cont { rC :: (a -> r) -> r }

defines 2 functions "for free":

Cont :: ((a -> r) -> r) -> Cont r a
rC :: Cont r a -> (a -> r) -> r

Then in your attempted definition of >>=, you had:

Cont aCont >>= f = Cont $ \k -> rC (aCont (\a -> f a)) (\b -> k b)

Here aCont (\a -> f a) is being used as the argument to rC, so must have type Cont r a. At the same time, since Cont is a constructor with the type shown above, from Cont aCont then GHC must assign to aCont the type (a -> r) -> r. This in turn means f a must have type r, while a has type a -> r.

But from the type of >>=, f must have type a -> Cont r b. So f a must simultaneously be of type r and Cont r b, and trying to make those two types the same clearly involves an infinite regress - which is exactly what GHC is telling you.

The details above aren't too important however. What seems obvious is that aCont was already "unwrapped" and you didn't need to apply the unwrapping function rC to it.

Answer 2

The r types must match in the definition of the >>=

If your type was

type Cont' a = forall r . Cont r a

Your definition would be valid

bind  :: Cont' a -> (a -> Cont' b) -> Cont'  b
bind  (Cont aCont) f = Cont $ \k -> rC (aCont (\a -> f a)) (\b -> k b)

The cool thing is without newtype wrapper this definition is simply function application.

bind
  :: (forall r . (a -> r) -> r)
  -> (forall r . a -> (b -> r) -> r)
  -> (forall r . (b -> r) -> r)
bind a b = a b

Without using existential quantification you should do explicitly pass continuations.

bind' :: ((a -> r) -> r) -> (a -> (b -> r) -> r) -> ((b -> r) -> r)
bind' a b cont = a (\a' -> b a' cont)

Finally with newtype wrapper

bind'' :: Cont r a -> (a -> Cont r b) -> Cont r b
bind'' a b = Cont $ \g -> rC  a (\a' -> rC (b a') g )