I'm totally obsessed at the moment by the fact that (on rings, say) + is linear as a function of type R & R → R, and * is linear as a function of type R ⊗ R → R. In other words, addition is on additive pairs, and multiplication is on multiplicative pairs.
Conversation
This Tweet was deleted by the Tweet author. Learn more
That blog post a few weeks back about tensor networks hinted me on to it. The notion of linearity in type theory matches up syntactically to the notion of linearity in linear algebra (given only addition and multiplication – no exponentials).
2
3
Expand them into iterated multiplication 😛. It's quite possible that linear logic's exponentials fit, particularly if graded. x² requires 2 copies of x, so maybe -^y : !_y R → R makes sense (even for non-natural number y).