Skip to content
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

Closed
vicuna opened this issue Oct 4, 2014 · 6 comments
Closed

lack of syntax for pattern-matching with no branches #6598

vicuna opened this issue Oct 4, 2014 · 6 comments
Assignees
Labels
feature-wish typing-GADTS GADT typing and exhaustiveness bugs
Milestone

Comments

@vicuna
Copy link

vicuna commented Oct 4, 2014

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.

@vicuna
Copy link
Author

vicuna commented Oct 4, 2014

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
let f : (float, (int, eq)) sum -> float =
function
| Left x -> x
| Right absurd

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 "()").

@vicuna
Copy link
Author

vicuna commented Oct 4, 2014

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".

@vicuna
Copy link
Author

vicuna commented Oct 5, 2014

Comment author: @garrigue

This would be a reasonable addition.
However, there is a problem: currently, the exhaustiveness checker does only check cases if at least one constructor is given, and has no way to get the typing information otherwise.
So we would have to solve that problem first.

@vicuna
Copy link
Author

vicuna commented Oct 11, 2014

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 =

  function
  | Left x -> x
  | Right (: (int,bool) eq);;

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.

@vicuna
Copy link
Author

vicuna commented Apr 23, 2015

Comment author: @lpw25

Maybe eg. ?! could be used instead of "absurd".

How about " * "?

@vicuna
Copy link
Author

vicuna commented Oct 23, 2015

Comment author: @garrigue

Since the merge of gadt-warnings at revision 16532, you can now write:

let f : (int,bool) eq -> 'a = function _ -> .

@vicuna vicuna closed this as completed Feb 16, 2017
@vicuna vicuna added this to the 4.03.0 milestone Mar 14, 2019
@Octachron Octachron added the typing-GADTS GADT typing and exhaustiveness bugs label May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature-wish typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants