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.
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:
... (read more)