{-# 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 runContto 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:
and it's useful because a
C' r ais "almost isomorphic" to anavalue, except that the typeris known. This means that you can construct a monadic value of typeC' Int Charrepresenting a pureChar:but you can also construct a monadic value of the same type
C' Int Charthat short circuits the computation with anIntreturn value:In constrast, your rank-2 continuation monad:
is precisely isomorphic to type
a. One direction of the isomorphism is given bypure, and the other is given by:So, with your
C Char, you can represent a pureChar:and that's it.
Because of this isomorphism, your
arris always equal to the section($ a0)for somea0 :: a, and youraCbrris always equal to\a' -> C ($ f a')for somef :: a -> b, and this means that the original definition of>>=gives:while your modified definition of
>>=givesso the two definitions are equivalent.