[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

[Olaf Klinke]

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.html
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.