Let's begin with the familiar type of CPS suspended computations, (a -> r) -> r, spelled as Cont r a in mtl-speak. We know that it is isomorphic to a as long as it is kept polymorphic in r. If we nest this type, we get this rank-3 type:
forall r. ((forall s. (a -> s) -> s) -> r) -> r
(For the sake of convenience, I might have defined type Susp a = forall r. (a -> r) -> r and then began talking about Susp (Susp a), but I fear that would lead to distracting technicalities.)
We can get a similar type by universally quantifying the result type only after nesting, as it would be if we had forall r. Cont r (Cont r a):
forall r. (((a -> r) -> r) -> r) -> r
Is there any meaningful difference between these two types? I say meaningful because some things that can apparently be only done with the first, "SuspSusp" type...
GHCi> foo = (\kk -> kk (\k -> k True)) :: forall s. ((forall r. (Bool -> r) -> r) -> s) -> s
GHCi> bar = (\kk -> kk (\k -> k True)) :: forall r. (((Bool -> r) -> r) -> r) -> r
GHCi> foo (\m -> show (m not))
"False"
GHCi> bar (\m -> show (m not))
<interactive>:76:12: error:
* Couldn't match type `[Char]' with `Bool'
Expected type: Bool
Actual type: String
* In the expression: show (m not)
In the first argument of `bar', namely `(\ m -> show (m not))'
In the expression: bar (\ m -> show (m not))
... can also be achieved with the second, "ContCont" one by taking advantage of the free theorem for (a -> r) -> r, f (m g) = m (f . g) for any m :: (a -> r) -> r.
GHCi> foo (\m -> m (show . not))
"False"
GHCi> bar (\m -> m (show . not))
"False"
I'm not entirely confident about the following take on the matter (it kinda feels too good to be true), but it is the best I have to offer up to now, so let's put it on the table.
chi's answer tackles the problem by proposing an isomorphism candidate between a and forall r. (((a -> r) -> r) -> r) -> r:
-- If you want to play with these in actual code, make YD a newtype.
type YD a = forall r. (((a -> r) -> r) -> r) -> r
ydosi :: a -> YD a
ydosi x = \kk -> kk (\k -> k x)
ydiso :: YD a -> a
ydiso mm = mm (\m -> m id)
chi then proves ydiso . ydosi = id, which leaves the ydosi . ydiso direction to be dealt with.
Now, if we have some f and its left inverse g (g . f = id), it readily follows that f . g . f = f. If f is surjective, we can "cancel" it on the right, leading us to f . g = id (i.e. the other direction of the isomorphism). That being so, given that we have ydiso . ydosi = id, establishing that ydosi is surjective will be enough to prove the isomorphism. One way of looking into that is reasoning about the inhabitants of YD a.
(Though I won't attempt to do that here, I presume the following passages can be made precise by expressing them in terms of the System F typing rules -- cf. this Math.SE question.)
An YD A value is a function that takes a continuation:
mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> _y
-- kk :: forall r. ((A -> r) -> r) -> r
-- _y :: r
The only way to get a result of type r here is by applying kk to something:
mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk _m
-- kk :: forall r. ((A -> r) -> r) -> r
-- _m :: forall r. (A -> r) -> r
As the type of kk is polymorphic in r, so must be the type of _m. That means we also know what _m must be like, thanks to the familiar A/forall r. (A -> r) -> r isomorphism:
mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk (\k -> k _x)
-- kk :: forall r. ((A -> r) -> r) -> r
-- k :: forall r. (A -> r) -> r
-- _x :: A
The right-hand side above, however, is precisely ydosi:
mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = ydosi _x
-- _x :: A
We have just found out that any forall r. (((A -> r) -> r) -> r) -> r value is ydosi x for some x :: A. It immediately follows that ydosi is surjective, which is enough to prove the isomorphism.
Since a is isomorphic to forall r. ((forall s. (a -> s) -> s) -> r) -> r (cf. Twan van Laarhoven's comment) and to forall r. (((a -> r) -> r) -> r) -> r, transitivity means both nested suspension types are isomorphic.
What do the witnesses of the nested suspension isomorphism look like? If we define...
-- The familiar isomorphism.
type Susp a = forall r. (a -> r) -> r
suosi :: a -> Susp a
suosi x = \k -> k x
suiso :: Susp a -> a
suiso m = m id
... we can write...
ydosi . suiso . suiso :: Susp (Susp a) -> YD a
suosi . suosi . ydiso :: YD a -> Susp (Susp a)
... which boils down to:
-- A few type annotations would be necessary to persuade GHC about the types here.
\mm -> \kk -> kk (\k -> k (mm id id)) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)
We can apply the Susp a free theorem on mm in the first witness...
f (mm g) = mm (f . g) -- Free theorem
f (mm id) = mm f
mm id id
($ id) (mm id)
mm ($ id)
mm (\m -> m id)
... and so:
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)
Fascinatingly, the witnesses are "the same" except for their types. I wonder if there some argument starting from this observation would allow us to proceed backwards and prove the isomorphism in a more direct way.