← Back to context

Comment by burakemir

3 days ago

The paper "Linearity and Uniqueness: an entente cordiale" by Marshall,Vollmer,Orchard offers a good discussion and explanation of the "opposite convention" you describe.

There is a dual nature of linearity and uniqueness, and it only arises when there are expressions that are not linear/not unique. At the same time, they have a lot in common, so we do not have a situation that warrants separate names. It is even possible to combine both in the same type system, as the authors demonstrate.

Taken from the paper:

"Linearity and uniqueness behave dually with respect to composition, but identically with respect to structural rules, i.e., their internal plumbing."