-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Name existentials : new approach #10180
Conversation
…edtree as suggested by @lpw25
Another drawback is that where one can write the annotations may be confusing: the type checker will only look on the outside of each argument. |
Note that I did not suggest to change the concrete syntax, only the representation in the Parsetree. I think it would be confusing to only accept |
C (P1, ..., Pn) Some (Ppat_tuple [P1; ...; Pn]) | ||
| Ppat_construct of | ||
Longident.t loc * (pattern * string loc list) option | ||
(* C None |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nitpick : I would find more natural to follow the same ordering as the concrete syntax, i.e. string loc list * pattern
.
Both syntaxes have advantages and inconvenients:
I have a preference for (2). (I think that the change of representation suggested by @alainfrisch is also probably a good idea.) Regarding the toplevel-only nature: what happens if we try to use the feature and we forget the toplevel-only nature, we try to annotate the existential variable in depth in the pattern? I suspect that the restrictions that @garrigue put (on the usage of the bound variables at the toplevel) will result in an error in this case (instead of an accepted program with a confusing behavior for the user which is not aware of the topleve restriction), which is good news. I suppose this is clear in some of the examples? |
For the second, this is already the case without For the first, it is accepted in both cases without Another solution is to go back to my first solution, but allow the second kind of annotation (yet without the inner parenthesis) even when there is no |
The only question is whether all the variables are bound or not. This is decided at the toplevel, and if some are unbound, or wrongly instantiated, one gets an error. Once they are bound, you can use them as much as you want in inner annotations. |
From the testsuite:
I find this error message rather confusing. What is it trying to tell me, and how should I fix my code? Naively I would expect that:
I think that lifting (2) would be even nicer with the new per-argument syntax, where it is very tempting to annotate only the arguments that contain the one existential type variable we care about. |
My point is that currently, users implicitly learn that It looks straightforward to allow writing Alternatively, or in addition to that, one could also decide to allow All that might seem ad hoc, but it's coherent with the current overloaded syntax for N-ary constructors, and it's just light syntactic processing that reduces the confusion. (But you know, YMMW, I'm also the one who advocated allowing to write |
Personally, my preference would be for going with the design from the other PR, but also allowing users to write:
for n-ary constructors when there is no list of existential constructors. |
I also prefer the original approach. This indeed means a change in the way to annotate constructors, but this seems more coherent with the fact annotations require parentheses. As for the way users have "learnt" that it is always better to write annotations inside, I would assume they would be happy to "unlearn" that, in particular the change is introduced with a new construct. |
The suggested changes are now implemented in the original PR #9584 . |
Close this one as #9584 was merged. |
#9584 proposed a new syntax to name existentials in pattern-matching:
This is a variation which follows the original syntax for type annotations, as suggested by @alainfrisch :
Note that one does not have to annotate all arguments, just enough of them to bind all the ai's.
For instance.
See name_existentials.ml for concrete examples.
A drawback of the current code is that it translates type annotations twice: once to bind the existentials, and once more to constrain the patterns (keeping the code simple).