I thought the right type for ContT should be
newtype ContT m a = ContT {runContT :: forall r. (a -> m r) -> m r}
and other control operators
shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
reset :: Monad m => ContT m a -> ContT m a
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
Unfortunately, I can not make callCC
type check, and don't know how to do it.
I managed to make shift
and reset
type check
reset :: Monad m => ContT m a -> ContT m a
reset e = ContT $ \ k -> runContT e return >>= k
shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
shift e = ContT $ \ (k :: a -> m r) ->
runContT ((e $ \ v -> ContT $ \c -> k v >>= c) :: ContT m r) return
but still, I can't use shift
and reset
in recursive jumpings like this?
newtype H r m = H (H r m -> ContT m r)
unH (H x) = x
test = flip runContT return $ reset $ do
jump <- shift (\f -> f (H f))
lift . print $ "hello"
unH jump jump
Have anyone tried this before?
Would you like to play a game?
Today, you get to be callCC
.
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
-- you are here ^^
Everything to the left of that function arrow are the moves your opponent has made. To the right of the arrow is the end of the game. To win, you must construct something matching the right side using only the pieces your opponent has provided.
Fortunately, you still have some say in matters. See this arrow here?
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
-- this is your opponent ^^
When you receive something that itself contains an arrow, everything to the left of that represents moves you get to make, and the part to the right the end of that game branch, giving you another piece you can use as part of your (hopefully) winning strategy.
Before we go further, let's simplify a few things: The monad transformer aspect is merely a distraction, so discard that; and add explicit quantifiers for every type variable.
callCC :: forall a. ((a -> (forall b. Cont b)) -> Cont a) -> Cont a
Now, think about what a type like forall a. ...
amounts to. If you produce something with a type like that, you're saying you can provide a value for any type a
whatsoever. If you receive something with a type like that, you can pick a specific type to use. Compare that to a type like A -> ...
for a monomorphic function; producing such a function says that you know how to provide a result for any value of type A
, while receiving such a function lets you pick a specific value A
to use. This seems to be the same situation as with forall
, and in fact the parallel holds. So, we can treat forall
as indicating a move where you or your opponent gets to play a type, rather than a term. To reflect this, I'll abuse notation and write forall a. ...
as a =>
; we can then treat it just like (->)
except that it must appear to the left of any uses of the type variable being bound.
We can also note that the only thing that can be done directly with a value of type Cont a
is applying runCont
to it. So we'll do that in advance, and embed all the relevant quantifiers directly into the type for callCC
.
callCC :: a => ( (a -> (b => (r1 => (b -> r1) -> r1)))
-> (r2 => (a -> r2) -> r2)
) -> (r3 => (a -> r3) -> r3)
Because we're able to treat forall
just like other function arrows, we can reorder things and remove superfluous parentheses to tidy things up a bit. In particular, note that callCC
isn't actually the end of the game, as it turns out; we have to provide a function, which amounts to providing another game to play in which we again take the role of the rightmost arrow. So we can save a step by merging those. I'll also float type arguments to the left to get them all in one place.
callCC :: a => r3 => (a -> r3)
-> (r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2)
-> r3
So... our move.
We need something of type r3
. Our opponent has made four moves, which we've received as arguments. One move is to choose r3
, so we're at a disadvantage already. Another move is a -> r3
, meaning that if we can play an a
, our opponent will cough up an r3
and we can coast to victory. Unfortunately, our opponent has also played a
, so we're back where we started. We'll either need something of type a
, or some other way to get something of type r3
.
The final move our opponent made is more complicated, so we'll examine it alone:
r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2
Remember, this is the move they made. So the rightmost arrow here represents our opponent, and everything to the left represents the type of moves we can make. The result of this is something of type r2
, where r2
is something we get to play. So clearly we'll need to play either r3
or a
to make any progress.
Playing a
: If we play a
as r2
, then we can play id
as a -> r2
. The other move is more complicated, so we'll jump inside that.
b => r1 => a -> (b -> r1) -> r1
Back to the rightmost arrow representing us. This time we need to produce something of type r1
, where r1
is a move the opponent made. They also played a function b -> r1
, where the type b
was also a move they made. So we need something of either type b
or r1
from them. Unfortunately, all they've given us is something of type a
, leaving us in an unwinnable position. Guess playing a
earlier was a bad choice. Let's try again...
Playing r3
: If we play r3
as r2
, we also need to play a function a -> r3
; fortunately, the opponent already played such a function, so we can simply use that. Once again we jump inside the other move:
b => r1 => a -> (b -> r1) -> r1
...only to find that it's exactly the same impossible situation as before. Being at the mercy of the opponent's choice of r1
with no requirement that they provide a way to construct one leaves us trapped.
Perhaps a bit of trickery will help?
Bending the rules -- playing r1
:
We know that in regular Haskell we can rely on laziness to twist things around and let computations swallow their own tail. Without worrying too much about how, let's imagine that we can do the same here--taking the r1
that our opponent plays in the inner game, and pulling it out and back around to play it as r2
.
Once again, here's the opponent's move:
r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2
After our knot-tying shenanigans, it ends up equivalent to this:
(b => a -> (b -> r1) -> r1) -> (a -> r1) -> r1
The type arguments have disappeared thanks to our trickery, but r1
is still chosen by the opponent. So all we've accomplished here is shuffling things around; there's clearly no way we can even hope to get an a
or r3
out of this, so we've hit another dead end.
So we make one final, desperate attempt:
Bending the rules -- playing b
:
This time we take the b
played by the opponent in the innermost game and loop that around to play as r2
. Now the opponent's move looks like this:
(r1 => a -> (b -> r1) -> r1) -> (a -> b) -> b
And then back in the inner game:
r1 => a -> (b -> r1) -> r1
Continuing the trickery we can twist the b
result above around as well, to give to the function b -> r1
, receiving the r1
we need. Success!
Stepping back out, we still have one problem left. We have to play something of type a -> b
. There's no obvious way to find one, but we already have a b
lying around, so we can just use const
on that to discard the a
and--
--but wait. Where's that value of type b
coming from in the first place? Putting ourselves briefly in our opponent's shoes, the only places they can get one are from the results of the moves we make. If the only b
we have is the one they give us, we'll end up going around in circles; the game never ends.
So, in the game of callCC
, the only strategies we have lead to either a loss or a permanent stalemate.
callCC :: forall a. ((a -> (forall b . Cont b)) -> Cont a) -> Cont a
callCC = error "A strange game..."
Alas, it seems that the only winning move is not to play.
Although there is no way to win the given game, if we can twist the game a little bit we could win!
newtype ContT' m a =
ContT' { runContT' :: forall r. (Maybe a -> m (Maybe r)) -> m (Maybe r) }
As we have seen in the other answer, the problem we have is, to win we have to generate a value for an arbitrary type our opponent played, but we do not know how to do so.
By forcing all raw types (r
and a
) being decorated by Maybe
, we can bypass this problem, and are able to generate a value of any Maybe t
-- simply give Nothing
to them!
We got to show this is a Monad
.
instance Monad m => Monad (ContT' m) where
return a = ContT' $ \k -> k (Just a)
a >>= f = ContT' $ \c -> runContT' a (
maybe (return Nothing) (\v -> runContT' (f v) c))
And then We can implement callCC
:
class Monad m => MonadCont' m where
callCC' :: ((a -> forall b.m b) -> m a) -> m a
instance Monad m => MonadCont' (ContT' m) where
callCC' k = ContT' $ \c ->
runContT' (k (\a -> ContT' $ \_ -> c (Just a) >> return Nothing)) c
I am still working out how to implemen reset
and shift
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With