= 27d567bc2d48d9f40e9ccc20ea370b15)
lmm 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)
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.