= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it comments on Open thread, September 15-21, 2014 - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (339)
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.