Making sense of Yoneda
Nov. 17th, 2024 11:04 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sassa_nfFurther to the earlier conversation about (x→p)→q as a monad.
Let's make sense of the application of Yoneda lemma here:
https://chaource.dreamwidth.org/235262.html?thread=1023998#cmt1023998
This part of the original proof:
is basically telling us that all we can do, is compose (y → p) with (p → p).
See what changed? A bind that receives (y → p) and (x → (y → p) → q) is the same as a bind that receives just (x → (p → p) → q). This means that all that the original bind can do, is pass a modified yp: (y → p) to (x → (y → p) → q), and that the only way the bind can modify yp is by composing it with a pp: (p → p).
In other words,
bind : ∀ x. ∀ y. ((x → p) → q) → (x → (y → p) → q) → (y → p) → q
can be obtained from
bind-p : ∀ x. ((x → p) → q) → (x → (p → p) → q) → q
Like so:
bind xpq xypq yp = bind-p xpq (\x pp -> xypq x (pp . yp))
It works the other way around, too (remember how Yoneda works? Set y=p, and pass id):
Hey! That's one part of the isomorphism done!
Ditto for bind:
I don't know how to get to isomorphism without an extra assumption, which I think we can make due to Parametricity: bind xpq xypq = bind xpq . (\yp x -> xypq x yp) - basically, that bind necessarily passes yp to xypq. There seems to be a spirit of Y combinator here.
Perhaps, less formally:
This is the case, if yp1=yp and pp=id - which is the case only if bind passes its third argument to the second. So, we infer some aspect of bind's implementation. It would be great to figure out that that's the only way.
I hope I didn't make a mess of it, so I will continue in the same vein for the second part of the proof.
So we have a new function, bind-r : ((((p → p) → q) → p) → q) → q, which can be used to obtain bind-p:
bind-p xpq xppq = bind-r (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp)))
We can get bind-r from bind-p, too - just pass id to bind-p:
Let's see how it works the other way:
I am not sure how to proceed to a full proof that this is bind-p xpq xppq, except assume that it has to pass xppq to xpq, because it has to work for any type x, and that there is a function pp: p → p and qp : q → p, because that's the only way to pass xppq to xpq: xpq can't pass a value of that type, so only bind-p can do it; and xpq can't accept a function that returns q, we need qp to make it of the right type.
Perhaps, less formally:
This is the case if bind-p constructs ppqp like so: ppqp = qp . ($ pp) . xppq. Then on the last line we get ppqp1=qp . ($ pp) . xppq, and on the line above that ppqp=qp .($ pp) . id, but it becomes the same expression after composing with xppq.
Now let's consider what possible bind-r are there:
bind-r ppqpq = qq $ ppqpq (\ppq -> qp $ ppq pp)
Basically, smallest possible bind-r can be constructed from three values:
bind-r-cons : (p → p) → (q → p) → (q → q) → ((((p → p) → q) → p) → q) → q
bind-r-cons pp qp qq = \ppqpq -> qq $ ppqpq (\ppq -> qp $ ppq pp)
Hmmm... I was hoping to get rid of these loose ends in one go, but maybe later.
Let's make sense of the application of Yoneda lemma here:
https://chaource.dreamwidth.org/235262.html?thread=1023998#cmt1023998
This part of the original proof:
bind : ∀ x. ∀ y. ((x → p) → q) → (x → (y → p) → q) → (y → p) → q ≅ ∀ x. ∀ y. (y → p) → ((x → p) → q) → (x → (y → p) → q) → q -- Flipped the curried arguments. ≅ ∀ x. ∀ y. (y → p) → H y -- Defined H y = ((x → p) → q) → (x → (y → p) → q) → q. Use Yoneda: ≅ ∀ x. H p = ∀ x. ((x → p) → q) → (x → (p → p) → q) → q
is basically telling us that all we can do, is compose (y → p) with (p → p).
See what changed? A bind that receives (y → p) and (x → (y → p) → q) is the same as a bind that receives just (x → (p → p) → q). This means that all that the original bind can do, is pass a modified yp: (y → p) to (x → (y → p) → q), and that the only way the bind can modify yp is by composing it with a pp: (p → p).
In other words,
bind : ∀ x. ∀ y. ((x → p) → q) → (x → (y → p) → q) → (y → p) → q
can be obtained from
bind-p : ∀ x. ((x → p) → q) → (x → (p → p) → q) → q
Like so:
bind xpq xypq yp = bind-p xpq (\x pp -> xypq x (pp . yp))
It works the other way around, too (remember how Yoneda works? Set y=p, and pass id):
bind-p xpq xpp = bind xpq xpp id
= bind-p xpq (\x pp -> xpp x (pp . id))
= bind-p xpq (\x pp -> xpp x pp)
= bind-p xpq xpp
Hey! That's one part of the isomorphism done!
Ditto for bind:
bind xpq xypq yp = bind-p xpq (\x pp -> xypq x (pp . yp))
= bind xpq (\x pp -> xypq x (pp . yp)) id
= -- substitute itself to unwrap one level
= bind xpq (\x1 pp1 -> (\x pp -> xypq x (pp . yp)) x1 (pp1 . id)) id
= bind xpq (\x1 pp1 -> (\x pp -> xypq x (pp . yp)) x1 pp1) id
= bind xpq (\x pp -> xypq x (pp . yp)) id
-- we reached a fixed point of the type
I don't know how to get to isomorphism without an extra assumption, which I think we can make due to Parametricity: bind xpq xypq = bind xpq . (\yp x -> xypq x yp) - basically, that bind necessarily passes yp to xypq. There seems to be a spirit of Y combinator here.
Perhaps, less formally:
bind xpq xypq yp = bind xpq (\x pp -> xypq x (pp . yp)) id
= bind xpq (\x yp1 -> xypq x yp1) ypThis is the case, if yp1=yp and pp=id - which is the case only if bind passes its third argument to the second. So, we infer some aspect of bind's implementation. It would be great to figure out that that's the only way.
I hope I didn't make a mess of it, so I will continue in the same vein for the second part of the proof.
... = ∀ x. ((x → p) → q) → (x → (p → p) → q) → q ≅ ∀ x. ((x → p) → q) → (x → r) → q -- Defined r = (p → p) → q ≅ ∀ x. (x → r) → ((x → p) → q) → q -- Flipped the curried arguments. ≅ ∀ x. (x → r) → H x -- Defined H x = ((x → p) → q) → q. Use Yoneda: ≅ H r = ((r → p) → q) → q = ((((p → p) → q) → p) → q) → q
So we have a new function, bind-r : ((((p → p) → q) → p) → q) → q, which can be used to obtain bind-p:
bind-p xpq xppq = bind-r (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp)))
We can get bind-r from bind-p, too - just pass id to bind-p:
bind-r rpq = bind-p rpq id
= bind-r (\ppqp -> rpq (\ppq -> ppqp (\pp -> id ppq pp)))
= bind-r (\ppqp -> rpq (\ppq -> ppqp (\pp -> ppq pp)))
= bind-r (\ppqp -> rpq (\ppq -> ppqp ppq))
= bind-r (\ppqp -> rpq ppqp)
= bind-r rpqLet's see how it works the other way:
bind-p xpq xppq = bind-r (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp)))
= bind-p (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) id
= -- apply itself to itself to unwrap one level
= bind-p (\ppqp1 -> (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) (\x1 -> ppqp1 (\pp1 -> id x1 pp1))) id
= bind-p (\ppqp1 -> (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) (\x1 -> ppqp1 (\pp1 -> x1 pp1))) id
= bind-p (\ppqp1 -> (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) (\x1 -> ppqp1 x1)) id
= bind-p (\ppqp1 -> (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) ppqp1) id
= bind-p (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) id
-- we reached a fixed point of the typeI am not sure how to proceed to a full proof that this is bind-p xpq xppq, except assume that it has to pass xppq to xpq, because it has to work for any type x, and that there is a function pp: p → p and qp : q → p, because that's the only way to pass xppq to xpq: xpq can't pass a value of that type, so only bind-p can do it; and xpq can't accept a function that returns q, we need qp to make it of the right type.
Perhaps, less formally:
bind-p xpq xppq = bind-p (\ppqp -> xpq (\x -> ppqp (\pp -> xppq x pp))) id
= bind-p (\ppqp -> xpq (\x -> ppqp (xppq x)) id
= bind-p (\ppqp -> xpq (ppqp . xppq)) id
= bind-p (\ppqp1 -> xpq ppqp1) xppqThis is the case if bind-p constructs ppqp like so: ppqp = qp . ($ pp) . xppq. Then on the last line we get ppqp1=qp . ($ pp) . xppq, and on the line above that ppqp=qp .($ pp) . id, but it becomes the same expression after composing with xppq.
Now let's consider what possible bind-r are there:
bind-r ppqpq = qq $ ppqpq (\ppq -> qp $ ppq pp)
Basically, smallest possible bind-r can be constructed from three values:
bind-r-cons : (p → p) → (q → p) → (q → q) → ((((p → p) → q) → p) → q) → q
bind-r-cons pp qp qq = \ppqpq -> qq $ ppqpq (\ppq -> qp $ ppq pp)
Hmmm... I was hoping to get rid of these loose ends in one go, but maybe later.
