I think the problem is hidden beneath the fixed point operator (I’ve edited the code to be more correct). For Id, is there actually a type Psi such that Psi <~> (Id[Psi] ⇒ A)? Isn’t that where the Y combinator comes in—the only reason loeb is able to act as a Y combinator is that it gets one passed in via the fixed point lemma? Isn’t a fixed point lemma always going to be the same as a Y combinator?
(I wish we were working with a proof that didn’t invoke this external lemma)
I asked the folks on /r/haskell, we hashed out a version in Agda and then I translated it into Haskell. It’s not completely in the spirit of the original question, but at least it’s a starting point. The code is here, you can try it out on CompileOnline.
Hmm, you’re right, in a total language you can’t define such a Psi for Id. Maybe the type class should go like this:
class Prov p f where
fix :: p (f a -> a (f a))
unfix :: p (a (f a) -> f a)
dup :: p a -> p (p a)
mp :: p (a -> b) -> p a -> p b
I don’t know if that’s enough. One problem is that fix and unfix are really inconvenient to use without type lambdas, which Haskell doesn’t have. Maybe I should try Scala, which has them.
Another problem is in step 13. To do that without soundness, I probably need versions of dup and mp that work inside p, as well as outside. But that makes the type class too complicated.
I think the problem is hidden beneath the fixed point operator (I’ve edited the code to be more correct). For Id, is there actually a type Psi such that Psi <~> (Id[Psi] ⇒ A)? Isn’t that where the Y combinator comes in—the only reason loeb is able to act as a Y combinator is that it gets one passed in via the fixed point lemma? Isn’t a fixed point lemma always going to be the same as a Y combinator?
(I wish we were working with a proof that didn’t invoke this external lemma)
I asked the folks on /r/haskell, we hashed out a version in Agda and then I translated it into Haskell. It’s not completely in the spirit of the original question, but at least it’s a starting point. The code is here, you can try it out on CompileOnline.
ETA: now I also wrote a post about it.
Hmm, you’re right, in a total language you can’t define such a Psi for Id. Maybe the type class should go like this:
I don’t know if that’s enough. One problem is that fix and unfix are really inconvenient to use without type lambdas, which Haskell doesn’t have. Maybe I should try Scala, which has them.
Another problem is in step 13. To do that without soundness, I probably need versions of dup and mp that work inside p, as well as outside. But that makes the type class too complicated.
Does this Haskell code answer your question?
The two directions of isomorphism:
Not sure. Fix is a type-level Y combinator, while loeb is a value-level Y combinator.
I think that’s not possible. Löb’s theorem requires the diagonal lemma.