Under Curry-Howard isomorphism, these rules, used frequently in logic, map into programming concepts. If we denote $A, B, C \vdash D$ a program (corresponding to a natural deduction proof) that computes a value of type $D$ from inputs of types $A$, $B$ and $C$, we get:
Contraction: $\Gamma, A, A\vdash B$ can be transformed into $\Gamma, A\vdash B$.
That is, a single input can be used twice.
Weakening: $\Gamma\vdash B$ can be transformed into $\Gamma, A\vdash B$.
That is, it's possible to add arbitrary, unused inputs.
Exchange: $\Gamma_1, A, B, \Gamma_2 \vdash C$ can be transformed into $\Gamma_1, B, A, \Gamma_2 \vdash C$.
That is, the order of inputs doesn't matter.
It also seems to me that weakening isn't an admissible rule for quantum computing, at least in the above form, as we can't forget a value with a unitary matrix. But we could have a weaker rule such as $\Gamma\vdash B$ can be transformed into $\Gamma, A\vdash A\otimes B$, and the $A$ in the output can be dropped when extracting the results of such a computation.
The exchange rule is clearly permissible in quantum computing.
Are there any other examples, in particular a language that doesn't allow exchange, or where weakening isn't allowed even in such a weaker form?