When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange?
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.
An example for language lacking contraction would be quantum computing. There the allowed operations can be described with unitary matrices, and duplicating a value can't be expressed as such.
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?