Apologies if this is is not very well-defined or exposes my ignorance; I know comparatively little about abstract algebra.
The structure of certain programming languages can be described with the algebraic structure $(S,\cdot,\verb|^|)$ where
$\cdot:S\times S\rightarrow S$ is associative and unital, and
$\verb|^| : S \rightarrow S$
i.e., a monoid with an extra unary operation. Unfortunately, nothing much can be said about $\verb|^|$ except that:
$\verb|^|$ distributes over $\cdot$, i.e., $\verb|^|(a\cdot b) = \verb|^|a\cdot \verb|^|b$.
$\verb|^|$ is cancellative: $\verb|^|a = \verb|^|$b implies $a = b$.
In particular, $\verb|^|$ is not an inverse operation, nor idempotent; in general, $\verb|^|(\verb|^|a) \neq a$, and in particular, $\verb|^|1\neq1$.
My question is:
Has this structure been studied, or at least been given a name, in abstract algebra?
I'm not optimistic, because adding $\verb|^|$ doesn't appear to make the structure much more interesting than a monoid. But if anyone can even point me towards similar structures, I'd be grateful. (Although clearly groups are not a good fit because of the lack of invertibility.)
(Edited to include the cancellative property of $\verb|^|$ and to explicitly mention its non-idempotency.)