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."
No comments yet
Contribute on Hacker News ↗