Excellent Question. The notion of linearity were starting with for type system design corresponds with runtime linear usage, which Means linear computations that are pure can be lifted into types because they don't have any runtime usage.
One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like &
Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake
One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like &
Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake