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].
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.