Yoneda is CPS

[sassa_nf]

https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/

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

Is it forall a or not? Yoneda says yes. Does this mean type system is boolean?

Comments

[ex_juan_gan]

The notation is kind of misleading.

It's about natural transformations from (a->_) to id, in Sets, and they are in one-to-one correspondence with the set a.

Hask is not Sets. Again, Hask is not Sets. I don't know where Bartosz takes all this, to me he seems over-creative.

So - never mind. He's just fantasizing.

[sassa_nf]

ok, that's better.

The question actually comes from the allegation that CPS is isomorphic to "direct" expression. I cannot recall where I saw this allegation, so was looking for a confirmation.

Then if they are not isomorphic, it means one of the ways is "more expressive"?

[ex_juan_gan]

Most probably, yes.

[sassa_nf]

meaning, one of them is more expressive?

[ex_juan_gan]

That's what I would expect.

I think continuation is like a closure, double adjunction. Generalized points.

[sassa_nf]

Actially, it is just me getting confused.

Here we are not talking about an isomorphism ((A→⊥)→⊥)→A (from which booleanness would follow). Here we are talking about a _family_ of functions. That is, the type is also an input:

CPS transform is an isomorphism: ((X : Type)→(A→X)→X)→A

(Note it isn't a value of type X as the first argument, but the type X)