Linear type systems often enforce that requirement by saying both branches need to use exactly the same linear values (or consume the same resources). So your example would be rejected by the type system. For example, the following function would not type check in a linearly-typed language because then branch is using x while else branch is not using x.
-- Using Haskell-like syntax, '-o' is linear arrow, i.e. lollipop
foo : Int -o Int -o Int
foo x y = if y < 0 then x else 0That wouldn't work, because the value must be used in all possible control paths. In this case, both the 'then' and 'else' branch would have to use the value.
Just curious, what is considered as 'using' the value?
Passing it as a parameter to a function or returning it
So can you work around that requirement by just going:
Technically it is used exactly once, but really it will never be used..