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

Olaf Klinke olf at aatal-apotheke.de
Sat May 16 08:41:28 UTC 2020

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


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. 

More information about the Haskell-Cafe mailing list