Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created a minimum at function monad (aka “reader monad”, “environment monad”)
What can be said about algebras for the function/reader monad, $A \mapsto A^E$? I see Zhen Lin gives as an example a setting where for a function $p: I \to E$ and dependent $X(i)$, the product type $\prod_{i:I} X(i)$ is an algebra, where the action
$(\prod_{i:I} X(i))^E \to \prod_{i:I} X(i)$sends $f$ to $i \mapsto f(p(i))(i)$.
I guess you can think of that by factoring $\prod_{i: I} X(i)$ as $\prod_{e: E} \cdot \prod_p X(i)$?
Is there anything to be said more generally about these algebras?
It’s possible that $\prod_E: Set/E \to Set$ is monadic in general (the associated monad is this reader monad). I can check this at least in the case where $E$ is finite, using crude monadicity: $\prod_E$ preserves reflexive coequalizers since the latter are sifted colimits and these commute with finite products. It seems to be isomorphism-reflecting as well although a slick proof eludes me at the moment.
I’m not going to have any time during the remainder of today to look into the situation for more general $E$.
If I recall correctly, when $E=2$ then the algebras are precisely the rectangular bands.
Regarding #3, I don’t think $\prod_E$ reflects isos even for finite $E$. If I’m not mistaken, when $E=\{0,1\}$, then $\prod_E(X,k_0)=\prod_E(Y,k_0)=\emptyset$ for all $X$ and $Y$. Here $k_0$ is the constant $0$ function. Maybe I misunderstood #3.
Thanks, Sam. I see you’re talking about such things in Instances of computational effects:an algebraic perspective. I’d never heard of bands before. There’s then a ’rectangular bands monad’, as discussed here, which is $id \times id$ for the identity monad.
A whole new world!
Stupid me.
Thanks. It was also discussed at the cafe back in 2015 (here). Out of that came the observation that $\prod: NonEmptySet^2\to NonEmptySet$ is monadic. So perhaps, more generally, #3 can be rescued with some non-emptyness assumptions.
1 to 8 of 8