Richard seems to be the only one with a strong opinion on this. I'm
happy to implement Richard's recommendations (both in the proposal and
in the code), unless there are dissenting voices?
I am still struggling to understand the choice that you are putting before us. I laid out my understanding last week:
- I think that the issue you are debating only arises when you, the programmer, want to explicitly annotate a let/where binding with a multiplicity. Right?
- I think that you are saying that all bindings with a non-Many multiplicity must be strict.
- I think the choices you are identifying are:
- If the explicit annotation is Many, does the binding still need to be strict?
- If the binding needs to be strict, do we insist on an explicit ! or, if -XStrict is on can we omit that bang?
Can I ask if my understanding is correct?
It is, with two caveats:
- the question of whether a pattern is strict also shows up when we infer the multiplicity of an unannotated let-binding. In this case, if the non-variable pattern isn't strict, then we emit a multiplicity-must-be-Many constraint. And the same choice (should we consider some patterns as strict when they aren't annotated with `!`) arises.
- beside the -XStrict question, there is the question of whether `(!p)` (with parentheses) is considered strict.
Here's the full logic I've considered so far (where `checkManyPattern` means: must be Many, and `return WpHole` means: no constraint on the multiplicity):
manyIfLazy dflags lpat
| xopt LangExt.Strict dflags = xstrict lpat
| otherwise = not_xstrict lpat
where
xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty
xstrict (L _ (ParPat _ _ p _)) = xstrict p
xstrict _ = return WpHole
not_xstrict (L _ (BangPat _ _)) = return WpHole
not_xstrict (L _ (VarPat _ _)) = return WpHole
not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p
not_xstrict _ = checkManyPattern pat_ty
Assuming so, to me the most straightforward and conservative thing is:
- All multiplicity-annotated pattern bindings must have an explicit bang, thus let %p !pat = rhs
This rule is simple, direct, and explicable. No one is going to write a multiplicity-annotated pattern binding let %Many pat = rhs, so it's not worth optimising for that case.
It's certainly the more conservative option. But Richard was arguing that it's too conservative. As for explicability: which of “the pattern must be strict” or “the pattern must be annotated with a !” is easier to explain? I'm not sure, but here's some food for thought: if we settle on “annotated with a !”, then how do we explain that patterns in case branches don't need to be annotated with a “!"?