Has this algebraic structure been named or studied?

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

A concrete example of the structure is: strings of symbols with brackets, with a semantics which gives the substrings inside brackets a different meaning. Joy is one such programming language based on this framework. The underlying monoid for Joy is well-described in that paper, but the bracketing operator (Joy's [...], my ^) is much less well-described algebraically, and I'm trying to find out more about where it might fit in (or be made to fit in.)

Given that it is not necessarily true that $\verb|^|1\neq 1$, we can't even say that $\verb|^|$ is an endomorphism of the monoid (only an endomorphism of the semigroup.)

The cancellation rule for $\verb|^|$ makes this hard to study in category theory. Without the cancellation rule, this would be some sort of "universal algebra." With the cancellation rule, we have a harder problem. (We don't talk about the category of integral domains, but really only the category of rings in general. The same is true here.)

By the way, it is not at all obvious that the "quote" operator of Joy distributes as you say. It seems like the description of "quote" in that article does not make $[ab]=[a][b]$. It depends on what it means, I guess, to "push onto the stack," but as I take it, $[a][b]$ pushes two things onto the stack, while $[ab]$ pushes only one.

I don't know if this one can meet you requirement:

Let $(S,+,\centerdot)$ be a semiring, and treat your $\centerdot$ as $+$, treat your ^a as $a\centerdot c$ for a fixed $c$.

Even though it has more properties than your structure, it's the best one I can think of.