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
lack of syntax for pattern-matching with no branches #6598
Comments
Comment author: @gasche I think an excellent syntax for this would be to have a special keyword "absurd", that would be a valid "absurd pattern" (absurd patterns being a new syntactic class defined just as patterns, except it also includes (absurd), possibly deep in the pattern). The syntax of pattern-matching clauses would then be extended with the case "| absurd_pattern". This would allow to write: let f : (int, eq) bool -> float = function absurd but also ( this example is taken from #6403 ): type ('a, 'b) sum = Left of 'a | Right of 'b In other words, "absurd" could serve as a hint to the type-checker about why a particular pattern is dead for typing reason, helping the exhaustiveness checker do a better job. (Inspiration comes from Agda's absurd pattern "()"). |
Comment author: @gasche Of course I'm not suggesting actually adding an "absurd" keyword, which is problematic for the usual backward-compatibility reasons, but it's still a good way to think about the syntax. An easy way out would be to use [%absurd] instead, but I dislike using extension points to add new semantic capabilities to the language. And the grammar would still need to be changed to accept absurd patterns without a right-hand-side expression. Maybe eg. ?! could be used instead of "absurd". |
Comment author: @garrigue This would be a reasonable addition. |
Comment author: jbj To get the typing information in there, how about writing "absurd" with a syntax like "(: t)", where t is a type. Then the examples above would be let f = function (: (int,bool) eq);;val f : (int,bool) eq -> 'a and let f =
val f : ('a, (int,bool) eq) sum -> 'a Note that type annotations on the "f" functions are no longer required. Hopefully the "locally abstract types" extension is powerful enough to let us write out the types in these patterns, even deep inside an expression. |
Comment author: @lpw25
How about " * "? |
Comment author: @garrigue Since the merge of gadt-warnings at revision 16532, you can now write: let f : (int,bool) eq -> 'a = function _ -> . |
Original bug ID: 6598
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:45Z)
Resolution: fixed
Priority: normal
Severity: feature
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: ~DO NOT USE (was: OCaml general)
Related to: #5998 #6403
Monitored by: jpdeplaix
Bug description
Assuming the usual declaration of GADT equality:
type (_, _) eq = Refl : ('a, 'a) eq
the function of type ((int, bool) eq -> float) with no branches cannot be written.
This is a purely syntactic limitation, as using the revised syntax makes the following program type-check:
type eq 'a 'b = [ Refl : eq 'a 'a ];
value f : eq int bool -> float = fun [ ];
It would be nice to have a way to express this in regular OCaml syntax.
The text was updated successfully, but these errors were encountered: