Open thread, September 15-21, 2014

gjm

Open thread, September 15-21, 2014 — LessWrong

Comment Permalink

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.

lmm12y10

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[_]: P

... (read more)

1lmm12y

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.

See in context

9

Open thread, September 15-21, 2014

9

9

9

Open thread, September 15-21, 2014

9

9