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