> We say that a function f is linear when f u is consumed exactly once implies that u is consumed exactly once (defined as follows).

- Consuming a value of a data type exactly once means evaluating it to head normal form exactly once, discriminating on its tag any number of times, then consuming its fields exactly once

- Consuming a function exactly once means applying it and consuming its result exactly once

https://github.com/ghc-proposals/ghc-proposals/blob/master/p...