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?

[zeit_raffer]

Wadler says yes. His free theorems guarantee...

[sassa_nf]

Does this mean Hask type system is boolean then?

[zeit_raffer]

no. it means that expression of cps with a quantifier is a good approximation for Yoneda.

[sassa_nf]

да, я забыл, это же fast and loose reasoning, а не полная правда.

А как Йонеда в Set выглядит? Вот у нас есть Hom(A,-), тогда Hom(A,⊥) - пустое множество для непустых A. Не наврал? И вот множество стрелок из пустого множества (естественные преобразования) изоморфно множеству, отображающему A?..