Thanks a lot! But your soundness condition isn’t one of the assumptions of the theorem, and it’s still too strong for my taste. Maybe I should clarify more.
I want the implementation of loeb to actually be a proof, by Curry-Howard. That means the implementation needs to be translatable into a total language, because non-totality turns the type system into an unsound logic where you can prove anything. An extreme case is this silly implementation of loeb, which will happily typecheck in Haskell:
loeb = loeb
Sadly, your version of loeb can’t be made total. To see why, consider the identity wrapper type:
data Id a = Id a
You immediately see that loeb specialized for Id is just the Y combinator with type (a → a) → a, which shouldn’t be implementable in a total language, because (a → a) → a isn’t true in any logic. To avoid that, the typeclass must have some methods that aren’t implementable for Id. But all methods in your typeclass are easily implementable for Id, therefore your loeb can’t be made total.
The same argument also rules out some other implementations I’ve tried. Maybe the root problem is the use of types like Fix, because they don’t have quite the same properties as the diagonal lemma which is used in the original proof. But I don’t really understand what’s going on yet, it’s a learning exercise for me.
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’m guessing that we get soundness :: a → p a for free in your notation?
I think you wanted loeb :: Prov p ⇒ (p a → a) → p a.
Scala implementation, I think:
Thanks a lot! But your soundness condition isn’t one of the assumptions of the theorem, and it’s still too strong for my taste. Maybe I should clarify more.
I want the implementation of loeb to actually be a proof, by Curry-Howard. That means the implementation needs to be translatable into a total language, because non-totality turns the type system into an unsound logic where you can prove anything. An extreme case is this silly implementation of loeb, which will happily typecheck in Haskell:
Sadly, your version of loeb can’t be made total. To see why, consider the identity wrapper type:
You immediately see that loeb specialized for Id is just the Y combinator with type (a → a) → a, which shouldn’t be implementable in a total language, because (a → a) → a isn’t true in any logic. To avoid that, the typeclass must have some methods that aren’t implementable for Id. But all methods in your typeclass are easily implementable for Id, therefore your loeb can’t be made total.
The same argument also rules out some other implementations I’ve tried. Maybe the root problem is the use of types like Fix, because they don’t have quite the same properties as the diagonal lemma which is used in the original proof. But I don’t really understand what’s going on yet, it’s a learning exercise for me.
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.