Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type? For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be interpreted as abelian monoids. For the sum type $A + B$, you can define the monoid operation as:
$$inj_L(a_0) \cdot inj_L(a_1) = inj_L(a_0 \cdot a_1)$$
$$inj_L(a) \cdot inj_R(b) = inj_R(b)$$
$$inj_R(b) \cdot inj_L(a) = inj_R(b)$$
$$inj_R(b_0) \cdot inj_R(b_1) = inj_R(b_0 \cdot b_1)$$
(Although this does mean that the interpretations of $A+B$ and $B+A$ are different).

So far though this scheme only lets me represent finite monoids where $\forall x: G, x \cdot x = x$. I'd like a way to extend it to infinite and more interesting monoids. That will at least require a way to interpret W-types but I can't see what that interpretation could be. Does such an interpretation exist? Or is there a simple proof that what I'm trying to do is impossible?
Fortunately you gave us some context in the comments (always a good idea to include it in your question). Rather than doing what you're trying to do, I believe quantitative type theory is what you're looking for.