Yoneda is CPS, think again

[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 - the isomorphism is between a fixed A and a dependently typed function:

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 a type X)

Comments

[juan-gandhi.livejournal.com]

Why should it even exist?

[sassa-nf.livejournal.com]

:-) I am not saying that it should, just reformulating the argument. I am only saying that I misunderstood the original argument - what was claimed to be isomorphic to what.

[sassa-nf.livejournal.com]

Having it for some types is interesting, especially if you can figure out for what sort of types the isomorphism holds. Like, it would be cool that if there is T→A, then the isomorphism holds.

If we cannot choose behaviour based on type X, then we cannot construct a value for any type X. But if we have a way to construct a value of type A, then we can costruct a value of any type X for which a A→X is provided. This is probably back to Wadler's free theorems to see that there are no other ways to obtain X in such a setting - so there are only as many functions of that type as there are values of A.

If there is no arrow T→A for some A, then maybe that's a type I am not that interested in. For example, I am not sure the non-existence of ((X : Type)→(A→X)→X) can be shown for A=⊥