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)
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.