On nested CPS suspension types

Question

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"

Since `Susp a` is isomorphic to `a`, it follows that `Susp (Susp a)` is also isomorphic to `a`. So your question then boils down to whether `forall r. Cont r (Cont r a)` is isomorphic to `a`. — Twan van Laarhoven, Apr 26 '18 at 15:56
I don't understand your statement of the free theorem. Can you clarify which variables are supposed to be quantified? — dfeuer, Apr 26 '18 at 16:47
@TwanvanLaarhoven Yup, that's another way of looking at it. (Originally, I was wondering about `Cont r (Cont r a)` versus `Susp a`; I then switched to the formulation in this post hoping that it might bring some extra clarity.) — duplode, Apr 26 '18 at 19:57
@dfeuer `r` is quantified; with `g :: a -> r` and `f :: r -> s`. (I probably should have written `(A -> r) -> r`, for the sake of clarity.) — duplode, Apr 26 '18 at 19:59

score 1 · Answer 1 · answered Apr 26 '18 at 21:25

(partial answer)

I wouldn't be surprised if a turned up to be isomorphic to your proposed type

forall r. (((a -> r) -> r) -> r) -> r

So far, I was only able to prove that the former embeds into the latter. The embedding could as well be an isomorphism, but if that holds, to prove that we will likely need to exploit parametricity on the scary type above.

Here's the embedding:

type YD a = forall r. (((a -> r) -> r) -> r) -> r

ydosi :: a -> YD a
ydosi x = \f -> f (\g -> g x)

ydiso :: YD a -> a
ydiso x = x (\a -> a id)

Proving that this is an embedding is easy, and only requires beta steps:

ydiso (ydosi x)
= ydiso (\f -> f (\g -> g x))
= (\f -> f (\g -> g x)) (\a -> a id)
= (\a -> a id) (\g -> g x)
= (\g -> g x) id
= id x
= x

The opposite direction is much harder, and (if possible) should rely on the parametricity of x :: YD a. Completing this would prove the wanted isomorphism.

ydosi (ydiso x)
= ydosi (x (\a -> a id))
= \f -> f (\g -> g (x (\a -> a id)))
= ????
= x

Yup -- the harder direction feels so close, yet so far... I wonder if showing either that `ydiso` is injective or that `ydosi` is surjective (which, I believe, should be enough to get the other direction given the one we already have), though it probably requires parametricity in a similar way. — duplode, Apr 27 '18 at 11:49
After quite a while, I have grown confident enough in my attempt to wiggle out of this bind to post it as [a complementary answer](https://stackoverflow.com/a/50885488/2751851). I'd love to hear your take on it. — duplode, Jun 16 '18 at 06:25

duplode · Accepted Answer · 2018-06-16T06:26:36.663

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.

On nested CPS suspension types

2 Answers2