Okay, I know next to nothing about Haskell, and next to nothing about provability logic, so maybe what I’m about to ask doesn’t make any sense, but here’s something that’s making me very curious right now. How do I implement a function like this:
loeb :: Prov p => p (p a -> a) -> p a
loeb = ???
using some typeclass like this:
class Prov p where
dup :: p a -> p (p a)
mp :: p (a -> b) -> p a -> p b
???
The idea is that the implementation of loeb should follow the steps of this proof, and the methods of Prov should correspond to the assumptions of that proof. The question was inspired by this post by sigfpe, but he thought that the class should be Functor, which seems wrong to me.
Apologies for the formatting, it turns out LW collapses whitespace even in preformatted blocks.
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.
Functor is a weak typeclass; the only thing it implies about □ is that □(a→b)→□a→□b (which we already know to be true). So the idea of using Functor was just to make the minimum possible assumption.
I don’t know enough Haskell to answer your question, but if you can write it in Scala I’ll give it a go.
The problem is that Functor’s operation isn’t quite what you wrote, but rather (a→b)→□a→□b, which is way too strong. I don’t think it holds in provability logic. That’s why I want to define an even weaker typeclass Prov, but I’m not sure what methods it should have, apart from dup and mp.
If you give me some Scala code, I think I’ll be able to make sense of it :-)
You’re right, I was taking the linked thing at face value.
The signature given is almost exactly Comonad. If I’m reading this right, Loeb’s theorem gives you something vaguely interesting: it’s a function from C[A] ⇒ A to A. So it tells you that any function that “flattens” a comonad must have some kind of “zero” value—e.g. any Stream[A] ⇒ A must give rise to a distinguished value of type A—which you can extract without ever having an instance of Stream[A].
Okay, I know next to nothing about Haskell, and next to nothing about provability logic, so maybe what I’m about to ask doesn’t make any sense, but here’s something that’s making me very curious right now. How do I implement a function like this:
using some typeclass like this:
The idea is that the implementation of loeb should follow the steps of this proof, and the methods of Prov should correspond to the assumptions of that proof. The question was inspired by this post by sigfpe, but he thought that the class should be Functor, which seems wrong to me.
Apologies for the formatting, it turns out LW collapses whitespace even in preformatted blocks.
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.
Functor is a weak typeclass; the only thing it implies about □ is that □(a→b)→□a→□b (which we already know to be true). So the idea of using Functor was just to make the minimum possible assumption.
I don’t know enough Haskell to answer your question, but if you can write it in Scala I’ll give it a go.
The problem is that Functor’s operation isn’t quite what you wrote, but rather (a→b)→□a→□b, which is way too strong. I don’t think it holds in provability logic. That’s why I want to define an even weaker typeclass Prov, but I’m not sure what methods it should have, apart from dup and mp.
If you give me some Scala code, I think I’ll be able to make sense of it :-)
You’re right, I was taking the linked thing at face value.
The signature given is almost exactly Comonad. If I’m reading this right, Loeb’s theorem gives you something vaguely interesting: it’s a function from C[A] ⇒ A to A. So it tells you that any function that “flattens” a comonad must have some kind of “zero” value—e.g. any Stream[A] ⇒ A must give rise to a distinguished value of type A—which you can extract without ever having an instance of Stream[A].
I’ve replied with Scala code upthread.