cousin_it comments on Open thread, September 15-21, 2014 - Less Wrong

6 Post author: gjm 15 September 2014 12:24PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (339)
Tags: open_thread

Comments (339)

You are viewing a single comment's thread.

Comment author: cousin_it 15 September 2014 09:18:29PM *  2 points [-]

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.

Comment author: lmm 16 September 2014 08:29:36PM *  1 point [-]

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:

trait ProofLike[O[_]] {
def sound[A](a: A): O[A]
def dup[A](oa: O[A]): O[O[A]] //Isn't this just a special case of soundness?
def mp[A, B](oab: O[A => B]): O[A] => O[B]
}
/**
* type-level function. Implementation left as an exercise for the reader
*/
trait MFix[F[_], O[_]] {
type Psi
def ->(p: Psi): F[O[Psi]]
def <-(fop: F[O[Psi]]): Psi
}
def loeb[O[_]: ProofLike, P](l1: O[P] => P, fx: MFix[({type F[A] = (A => P)]})#F, O]) : P = {
val pl = implicitly[ProofLike[O]]
type Psi = fx.Psi
val l3: Psi => (O[Psi] => P) = fx.->
val l4: O[Psi => (O[Psi] => P)] = pl.sound(l3)
val l5: O[Psi] => O[O[Psi] => P] = pl.mp(l4)
val l6: O[O[Psi] => P] => (O[O[Psi]] => O[P]) = pl.mp[O[Psi], P]
val l7: O[Psi] => (O[O[Psi]] => O[P]) = l5 andThen l6
val l8: O[Psi] => O[O[Psi]] = pl.dup[Psi]
val l9: O[Psi] => O[P] = {x: O[Psi] => val y = l8(x); l7(x)(y)}
val l10: O[Psi] => P = l9 andThen l1
val l11: (O[Psi] => P) => Psi = fx.<-
val l12: Psi = l11(l10)
val l13: O[Psi] = pl.sound(l12)
fx.->(l12)(l13)
}
Comment author: cousin_it 16 September 2014 09:05:16PM *  3 points [-]

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.

Comment author: lmm 16 September 2014 11:16:41PM *  3 points [-]

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)

Comment author: cousin_it 18 September 2014 02:05:28PM *  2 points [-]

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.

Comment author: cousin_it 17 September 2014 10:40:40AM *  2 points [-]

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.

Comment author: lmm 15 September 2014 09:38:10PM 1 point [-]

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.

Comment author: cousin_it 15 September 2014 10:28:12PM *  2 points [-]

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 :-)

Comment author: lmm 16 September 2014 08:59:09PM *  1 point [-]

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.

Powered by Reddit Powered by Reddit