Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t understand how this influences how we use such a language.
-
2$\begingroup$ Your question is pretty vague, but contraction is effectively used almost anytime you use a variable more than once, and weakening when you use it zero times. If I write $f(x,y)=x+x$, contraction is what allows me to use $x$ twice and weakening allows me to use $y$ zero times. $\endgroup$– Derek Elkins left SEAug 1, 2019 at 3:35