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

[juan-gandhi.livejournal.com]

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.livejournal.com]

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"?

[juan-gandhi.livejournal.com]

Most probably, yes.

[sassa-nf.livejournal.com]

meaning, one of them is more expressive?

[juan-gandhi.livejournal.com]

That's what I would expect.

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

[sassa-nf.livejournal.com]

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)

[zeit-raffer.livejournal.com]

Wadler says yes. His free theorems guarantee...

[sassa-nf.livejournal.com]

Does this mean Hask type system is boolean then?

[zeit-raffer.livejournal.com]

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

[sassa-nf.livejournal.com]

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

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

[sassa-nf.livejournal.com]

а, тьфу, это же стрелка из пустого множества - одно из значений множества естественных преобразований.

[zeit-raffer.livejournal.com]

also we cannot prove the isomorphism in the underlying type system.