Expand on bijection of linear inputs to outputs in quantum resource

[ss2165]

To finish the tket2 tangent above, concretely I propose TKET2 should have a constraint that it will only accept operations on qubits on linear types:

1. That take in as many of linear type L as they return
2. Will have the bijection semantics that when grouping by concrete type L, the nth input of type L maps to the nth output of type L

Functions like Sum(Qubit) ->i1 will need to use qfree in their definition. I think this gives us another distinction between Operation and Function?

Slack Message