As usual, Edward Kmett has the answer for anything categorical in Haskell. The type CPS a = forall r. (a -> r) -> r is isomorphic to Yoneda Identity a = forall r. (a -> r) -> Identity r and the latter is the Yoneda embedding [1] of the Identity functor. The Yoneda Lemma [2,3] states that for any functor f, the Yoneda embedding of f is isomorphic to f. We conclude that CPS a is isomorphic to a, and the relationship you found with Void is akin to the fact that in any Heyting algebra, any element is smaller than its double negation. Olaf [1] https://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Yoneda.... See also the blog post linked at the top of that page. [*] [2] https://en.wikipedia.org/wiki/Yoneda_lemma [3] https://ncatlab.org/nlab/show/Yoneda+embedding [*] Fun fact: If you install a Haskell package and watch which dependencies are build, surprisingly often kan-extensions is among them. You'd think: What the hell does category theory have to do with my program? But hey, this is a Haskell program you're writing, so you really should not be surprised.