Guards should accept linear variables
The following, for instance, will refuse to typecheck
f1 :: Bool %1 -> Int f1 x | x = 0 | otherwise = 1
However, guards are “just” another syntax for case and if expressions, where linear variable make perfect sense:
f2 :: Bool %1 -> Int f2 x = if x then 0 else 1
In principle, at least, it seems reasonable and idiomatic to allow
f1, and such functions.
The high-level proposal is easily written: make the type-checker aware of when a guard really consumes a value linearly.
But there are many things to understand
- We must make sure that such linear guards desugar to linear Core (by which I mean: the linter recognises that the code is properly linear). Maybe it is, maybe we may need to tweak it a little. See also #18806 which has similar issues.
- In pattern guards, we need to make sure that if the guard is linear, the bound variables are correspondingly linear. This is connected to #18738 .
It's very similar to
f3 :: Bool %1 -> Int f3 x | x = 0 f3 x | otherwise = 1
f1. Though it is typechecked and desugared differently. Does it matter in practice? Is this even reasonable to ask in theory? If the answer is no, though, let me note that around me there are people which consider
f3to be synonymous, and it may be surprising.
It looks a lot like
f4 :: Bool %1 -> Int f4 x | x = 0 f4 x = 1
f3too. But it is also different in subtle ways. Here again, some will consider
f4synonymous. But it's not necessarily clear that typechecking
f4as linear is reasonable in practice (I hope it would be though).
I'm probably forgetting other interesting special cases. But the point is: there is some pen-and-paper work to be done to specify what it even means to specify that a guard is linear. It may be easy, it may be hard; I don't know: I really haven't tried yet. The recent Lower your guard paper may offer a framework to think about these things.