[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
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.
More information about the Haskell-Cafe
mailing list