2 ms·
This is not correct actually. It comes from linear logic, and it's connection to ordinary linear functions we all learned in school is clear if you think about
by naasking 4y ago
This is not correct actually. It comes from linear logic, and it's connection to ordinary linear functions we all learned in school is clear if you think about it: any linear function f(x) can be written in a form where x appears only once on the right hand side, ie. f(x) = Bx + C.
That's exactly the property linear typing enforces: a new binding only appears once on the right hand side, ie. let x = v in e, where e references x only once.
- deleted 4y ago[deleted]