> 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
- 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...