Implement exhaustiveness check #4837

makenowjust · 2017-08-17T00:03:52Z

Implemented exhaustiveness check like Rust or Scala. It works for only union types and enums (and nil, true and false). For example:

enum FooBar
  Foo
  Bar
end

foo = FooBar::Foo
case foo
when .foo?
end

$ ./bin/crystal run foo_bar.cr
Error in foo_bar.cr:7: found non-exhaustive pattern: Bar

case foo
     ^~~

makenowjust · 2017-08-17T00:08:43Z

You can find other cases in spec.

makenowjust · 2017-08-17T00:17:25Z

src/compiler/crystal/semantic/main_visitor.cr

+
+        tuple_patterns.to_a
+                      .sort_by do |tuple_pattern|
+          tuple_pattern.map do |pattern|


This indentation looks formatter's bug, however it is another problem for this.

ysbaddaden

I think the feature is great. I also think I'll hate that feature.

makenowjust · 2017-08-17T00:44:44Z

@ysbaddaden I understand what you said. I want you to try to use this compiler to your project.

jhass

Leads to more verbose code but probably worth it

konovod · 2017-08-17T06:34:14Z

src/compiler/crystal/semantic/main_visitor.cr

+          last_last = last_last_else
+        end
+        if last_last.else.is_a?(Nop)
+          last_last.else = Call.new(nil, "raise", args: [StringLiteral.new("BUG: invalid exhaustivness check")] of ASTNode, global: true).at(node)


exhaustivness -> exhaustiveness

konovod · 2017-08-17T06:37:56Z

src/compiler/crystal/semantic/main_visitor.cr

+
+      case case_cond_type
+      when UnionType
+        # 'dup' is important to prevent to change this array value by mutable methods.


to change -> changing

konovod · 2017-08-17T06:43:37Z

src/http/client.cr

@@ -117,12 +117,12 @@ class HTTP::Client
  {% else %}
    def initialize(@host : String, port = nil, tls : Bool | OpenSSL::SSL::Context::Client = false)
      @tls = case tls
-             when true
-               OpenSSL::SSL::Context::Client.new
+             when Bool


~~So case now checks either types or enums, not both?~~
Nvm, i've checked and it works with old code too. So you just changed it for clarity?

No, it's just my mistake. Firstly I implemented exhaustiveness check without supporting true and false. It is remains of this.

RX14 · 2017-08-17T09:03:28Z

else nil for the old behaviour is hardly a lot of code to add, and this way is much more explicit. 👍

makenowjust · 2017-08-17T11:40:37Z

@asterite I'll fix it.

ysbaddaden · 2017-08-17T11:56:38Z

What I like in this PR is making the compiler smarter, so it knows that a case handles all possible cases, so I don't have to specify an else raise "unreachable" statement to avoid a nilable, for example. That's lovely.

What I don't like in this PR is trading implicit nilables and "I don't care for other values" for explicit noise with empty else statements (aka else # shut up crystal). This is pushing a burden to the developer.

I verified most of my applications and libraries, and this PR will help in... none. Quite the opposite, as it will require me to insert many empty else statements in each SDL2 samples for example.

The benefit, which is inexistant in all my projects (and it seems the compiler source too), isn't worth the burden. This is an unacceptable trade IMHO.

RX14 · 2017-08-17T12:16:14Z

@asterite I can't help but think that without global type inference what would be the point of crystal at all. Global type inference with unions is the defining feature of Crystal. To me - at least - it's what makes Crystal, Crystal. I think it'd be a huge mistake to change Crystal's type system in such a radical way this late in development, and it'd be a huge mistake to throw away something which is so beautiful and easy to use. Yes the compile times for large program suck, perhaps we'll have to introduce some "module" concept with defined types for the interface, but languages like Scala managed to succeed despite long compile times. Perhaps people using crystal will create more microservices than other languages.

I'd rather have a discussion like this on the mailinglist though.

faustinoaq · 2017-08-17T16:40:40Z

Maybe we can use some special keyword to check exhaustiveness

This code would compile ok:

enum FooBar
  Foo
  Bar
end

foo = FooBar::Foo

case foo
when .foo?
end

But this won't:

enum FooBar
  Foo
  Bar
end

foo = FooBar::Foo

@[Exhaustive]
case foo
when .foo?
end

See the @[Exhaustive] rule

$ ./bin/crystal run foo_bar.cr
Error in foo_bar.cr:7: found non-exhaustive pattern: Bar

case foo
     ^~~

makenowjust · 2017-08-17T17:07:20Z

I want the compiler to check exhaustiveness in default because exhaustiveness is important to prevent bugs, so I want you to consider about it at all times.

However many people need this, I suggest case! as keyword. (It breaks call of case! method, but I think this effects is very small.)

RX14 · 2017-08-18T08:45:06Z

If we are going to be exhaustive by default then else nil should be how we describe non-exhaustiveness not another keyword. However, @ysbaddaden provided some evidence that being exhaustive by default actually might not help catch many bugs, so I would like more data on this. If you have a library or project, please try out this pr and report back how much code you had to change and if it found any bugs.

makenowjust · 2017-08-18T14:35:51Z

I think exhaustiveness check to existed project affects us not helpful because all non-exhaustive cases in this project are intentional if this project is well tested.

RX14 · 2017-08-18T14:59:57Z

I actually prefer being exhaustive by default. It gives me peace of mind and most importantly a confidence to refactor and add {things to enums,types to unions} without worrying about every case clause it might touch.

makenowjust · 2017-08-18T15:04:36Z

We may need the attribute to drop exhaustiveness check from enum:

@[NotCheckExhaustiveness]
enum KeyCode
  A
  B
  # ...
end

key = KeyCode::A

# This `case` passes exhaustiveness check due to @[NotCheckExhaustiveness] attribute.
# Of course result type is nilable.
case key
when .w?
  go
when .a?
  turn_left
when .s?
  back
when .d?
  turn_right
end

/cc @ysbaddaden

RX14 · 2017-08-18T15:58:41Z

@makenowjust The problem is that that makes case behaviour dependant on an attribute on enum which is unlikely to be visible to the programmer at the point the enum is used.

straight-shoota · 2017-08-18T17:34:35Z

I found a failed exhaustiveness check in callstack.cr:205.

makenowjust · 2017-08-19T00:18:21Z

@straight-shoota I think it's already fixed. Your stdlib may be old.

makenowjust · 2017-08-19T00:24:43Z

@RX14 Exhaustiveness check to Char is impossible, and there are enums like Char (e.g. KeyCode I said.). I thought it is useful if we can define such enums.

makenowjust · 2017-08-19T06:53:06Z

Now it is working:

a = 42

loop do
  case a
  when Int32
  end

  a = "foo"
end

# Error in foo.cr:3: instantiating 'loop()'
#
# loop do
# ^~~~
#
# in foo.cr:3: instantiating 'loop()'
#
# loop do
# ^~~~
#
# in foo.cr:4: found non-exhaustive pattern: String
#
#   case a
#        ^

/cc @asterite

makenowjust · 2017-08-19T13:03:32Z

src/compiler/crystal/semantic/case.cr

+
+    if exhaustive? != is_exhaustive
+      last = expansion
+      last = last.expressions.last if last.is_a?(Expressions)


MEMO: last.expressions.last can be replaced to last.last.

makenowjust · 2017-08-20T13:52:42Z

ping. I don't want to stop discussion about this.

asterite · 2017-08-20T14:24:05Z

I personally think having case be non-exhaustive and case! be exhaustive would work well. This could be stored as a boolean in the AST node (also for to_s). I don't know what others think, though.

Ref crystal-lang#4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

asterite · 2018-06-02T12:56:08Z

Actually, about hierarchy type, maybe it's good not to check for exhaustiveness because code will break if a subclass is added in a separate library or application, and there's no way to fix that (you don't own the code that has the case). So probably with just unions and enums it's fine... Though with unions you could also have the same problem if someone redefines a method, but that's less common.

asterite · 2018-06-02T12:59:24Z

@makenowjust どうもありがとうございます！

asterite · 2018-06-02T13:01:03Z

Ship it!

Having this in 0.25.0 would be really nice, both because it improves the robustness of code, and because it can be tested early in the wild.

Ref #4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

bcardiff · 2018-06-02T17:58:21Z

Letting the case have two different semantics it's hard to understand.
The users might not feel secure if the compiler is performing or not the exhaustive check.

So I think the exhaustive vs non-exhaustive check should be explicit.

Having different keywords it is a clear way to do it: case/case?, case!/case or some other combination. I have come to over/case or even forall/case that I think express more clearly that you want to cover all cases (over or forall). forall is already a keyword but is used in other context without ambiguity.

But I think there is a different approach that could be more powerful.
It has been discussed previously (in #4749) but implementing compile time checks for unreachable would be a more elementary way to achieve the exhaustive checks without diffrent case statements.

case expr
when Int32
when String
else unreachable
end

Then all the case statements would try to omit the codegen of the else branch (or any other branch that is sound to remove) and hence the unreachable wont be emitted.

It is longer to type that a different control structure keyword but is a feature that can be combined with other control structures eventually if redundant code is detected. Note: The implementation would probably not be that different from this PR. The compile time error needs to be deferred, but the exhaustive check is the hardest part.

For me is either unreachable or a different case statement (I prefer unreachable between those). Having to add else nil for the cases (no pun intended) when the compiler was able to compute exhaustive coverage if the user wanted the same behavior as in other cases is way to obscure and hard to understand.

bcardiff

☝️

RX14 · 2018-06-03T11:00:57Z

So currently, this PR falls back to non-exhaustive case depending on the type of expr? That's not good.

I don't like else unreachable, I'll forget to type it everywhere.

Perhaps use case for exhaustive matching (you're looking at every case) and cond for non-exhaustive matching (you're just checking the condition, don't care about each case)?

RX14 · 2018-06-04T00:08:48Z

As for how to implement case/cond, I'd introduce cond and print a warning on non-exhaustive case on one version, then make non-exhaustive case an error on version+1.

makenowjust · 2018-06-04T04:31:03Z

No. It checks exhaustiveness for any typed expr. A user cannot choice exhaustiveness or non-exhaustiveness.

bcardiff · 2018-06-04T08:32:43Z

If the case expr is other type than union or enum, the case is not exhaustive. I see that as implicit because there is nothing in the expression typed by the user that expresses his/her expectation.

makenowjust · 2018-06-04T09:45:49Z

@bcardiff Sorry. I forgot this specification. Oh I see. It is bad point of this. However it needs more and more (180+ cases) appending else # skip if it check exhaustive for single-type case...

else unreachable and case forall are interesting ideas. I prefer case forall because it appears in above of syntax. I feel intuitive.

bcardiff · 2018-06-04T09:57:45Z

It's a subtle thing and is hard to be everybody in the same page.

Maybe the else unreachable would come later and first we can have it's own control structure that could later when else unreachable is implemented be rewritten or left as an implementation detail.

Just to be clear, I was previously proposing the following constructs to allow exhaustive checks:

forall a
when String
end

over a
when String
end

@RX14 suggestions to leave case of exhaustive and cond for the current behaviour is good also. That will require a release of crystal where case and cond have the same semantic and later change the semantic of the case.

Ref crystal-lang#4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

makenowjust · 2018-06-12T13:07:12Z

@asterite I think your opinion is needed to proceed with discussion. bcardiff opinion is right and his ideas are interesting to me. What do you think?

asterite · 2018-06-12T13:21:03Z

@bcardiff said:

Letting the case have two different semantics it's hard to understand.

But that's not true. case has only one semantic: it's always exhaustive. I mean, for types it's exhaustive. If the type is Int32 and you match with integers, you'll always need an else because there are many numbers (and I doubt one will list all of them). Same goes for symbol, etc. So case is always exhaustive, there's simply no confusion, no different semantics.

forall, cond, they are very confusing and add more keywords and noise to the language.

I personally don't mind having to add an else clasue to case for a few cases. It's more explicit that other cases are not considered.

So for me, this PR is perfect. And I would have liked it to be in 0.25.0.

But ultimately, I don't use Crystal anymore, so I shouldn't choose its future.

paulcsmith · 2018-06-12T13:35:15Z

Agreed. As long as it’s exhaustive in all cases I think this should work great. I can hardly wait to try this :)

straight-shoota · 2018-06-12T13:35:57Z

Yes, let's keep it simple, please.

I don't like having different keywords with subtle differences. People will be confused.
The concept of else is widely understood and should be capable of differentiating between exhaustiveness.

RX14 · 2018-06-12T21:21:35Z

@asterite no, this PR isn't exhaustive in all cases, for example:

str = "bar"

case str
when "foo"
  1
end

will not produce a compile error and be type Int32?

This is what we meant by the exhaustiveness depending on the argument.

Let's try making case always exhaustive and see how big the diff is.

asterite · 2018-06-13T00:34:52Z

Oh, I thought that was already the case, because I see else over symbols in the diff, and other primitives.

So yes, either change it to always be exhaustive, or only exhaustive when it makes sense (I'm fine with that too, and I find it intuitive and user friendly, as forcing al else clause over something that the compiler can't verify is a bit useless)

RX14 · 2018-11-06T12:16:38Z

I'd really love to see this PR merged. More correctness is great.

asterite · 2018-11-06T12:32:55Z

Note that this PR is incomplete and doesn't play nicely with the type flow inference.

For example:

a = 1 || "foo"
case a
when Int32
  b = 1
when String
  b = 2
end

puts typeof(b) # => Int32 | Nil

That is, the compiler correctly finds that it's an exhaustive match, but the type for b remains nilable because that logic goes in another place in the compiler. All of that should be unified but it's a bit hard to do.

(that's at least the last thing I remember when I tried this PR, now it needs a rebase but I'm pretty sure it'll still have that problem)

RX14 · 2018-11-06T12:41:09Z

I think we really need to form a consensus on the design first before fixing the implmentation because there are some unresolved issues.

I think the current prevailing design is for case to always be exhaustive and not introduce a second kind of case. However there's still the question of types like String where the compiler will never be able to prove exhaustiveness. For these types the case can either keep being exhaustive and force you to always have an else clause, or the compiler can stop being exhaustive in these cases.

The benefits of being exhaustive in this case are:

simplicity of semantics: the type of the case argument doesn't affect the semantics of case. Since types aren't explicit in crystal this makes case easier to understand on it's own.
It's impossible to accidentally create a non-exhaustive case by accidentally creating a union of (for example) Enum | String instead of Enum in your case argument.

The benefits of not being exhaustive in this case are:

not having to add verbose else nil clauses in the obvious case of case string.

There's also the option to make it so that case is exhaustive if just one of the types in the union can be exhaustively matched. This might make a better semantic in practice, but retains a lot of complexity.

Ideally we'll have a continued discussion of the pros and cons of these three choices of semantics below then a vote in a week or so. Merging any of those three semantics will be better than what we have currently.

Blacksmoke16 · 2020-03-30T00:21:03Z

This can probably be closed now that #8424 is merged?

bcardiff · 2020-03-30T00:25:42Z

Yes, but there is a lot of credit to go on this PR and the discussion 🙇.

makenowjust commented Aug 17, 2017

View reviewed changes

makenowjust force-pushed the feature/crystal/exhaustiveness-check branch from 53bf6bd to 7372c05 Compare August 17, 2017 00:26

ysbaddaden reviewed Aug 17, 2017

View reviewed changes

jhass approved these changes Aug 17, 2017

View reviewed changes

konovod reviewed Aug 17, 2017

View reviewed changes

makenowjust commented Aug 19, 2017

View reviewed changes

makenowjust force-pushed the feature/crystal/exhaustiveness-check branch from 256c621 to abb4f32 Compare August 20, 2017 00:19

makenowjust closed this Aug 20, 2017

makenowjust reopened this Aug 20, 2017

makenowjust mentioned this pull request Jun 2, 2018

Drop 'when _' support #6150

Merged

makenowjust added a commit to makenowjust/crystal that referenced this pull request Jun 2, 2018

Drop 'when _' support

6fdaf42

Ref crystal-lang#4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

asterite approved these changes Jun 2, 2018

View reviewed changes

RX14 pushed a commit that referenced this pull request Jun 2, 2018

Drop 'when _' support (#6150)

8da3b2e

Ref #4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

bcardiff requested changes Jun 2, 2018

View reviewed changes

chris-huxtable pushed a commit to chris-huxtable/crystal that referenced this pull request Jun 6, 2018

Drop 'when _' support (crystal-lang#6150)

d969aff

Ref crystal-lang#4837 I think this syntax has no use-case. It can be replaced with 'else' block always.

asterite mentioned this pull request Jul 26, 2019

[RFC] Exhaustive case #8001

Closed

asterite mentioned this pull request Nov 2, 2019

Exhaustive case #8424

Merged

4 tasks

bcardiff closed this Mar 30, 2020

Implement exhaustiveness check #4837

Implement exhaustiveness check #4837

Conversation

makenowjust commented Aug 17, 2017

makenowjust commented Aug 17, 2017

makenowjust Aug 17, 2017

Choose a reason for hiding this comment

ysbaddaden left a comment

Choose a reason for hiding this comment

makenowjust commented Aug 17, 2017

jhass left a comment

Choose a reason for hiding this comment

konovod Aug 17, 2017

Choose a reason for hiding this comment

konovod Aug 17, 2017

Choose a reason for hiding this comment

konovod Aug 17, 2017 • edited Loading

Choose a reason for hiding this comment

makenowjust Aug 17, 2017

Choose a reason for hiding this comment

RX14 commented Aug 17, 2017

makenowjust commented Aug 17, 2017

ysbaddaden commented Aug 17, 2017

RX14 commented Aug 17, 2017 • edited Loading

faustinoaq commented Aug 17, 2017

makenowjust commented Aug 17, 2017

RX14 commented Aug 18, 2017

makenowjust commented Aug 18, 2017

RX14 commented Aug 18, 2017

makenowjust commented Aug 18, 2017

RX14 commented Aug 18, 2017

straight-shoota commented Aug 18, 2017

makenowjust commented Aug 19, 2017

makenowjust commented Aug 19, 2017

makenowjust commented Aug 19, 2017

makenowjust Aug 19, 2017

Choose a reason for hiding this comment

makenowjust commented Aug 20, 2017

asterite commented Aug 20, 2017

asterite commented Jun 2, 2018

asterite commented Jun 2, 2018

asterite commented Jun 2, 2018

bcardiff commented Jun 2, 2018

bcardiff left a comment

Choose a reason for hiding this comment

RX14 commented Jun 3, 2018 • edited Loading

RX14 commented Jun 4, 2018

makenowjust commented Jun 4, 2018

bcardiff commented Jun 4, 2018 • edited Loading

makenowjust commented Jun 4, 2018

bcardiff commented Jun 4, 2018

makenowjust commented Jun 12, 2018

asterite commented Jun 12, 2018

paulcsmith commented Jun 12, 2018

straight-shoota commented Jun 12, 2018

RX14 commented Jun 12, 2018 • edited Loading

asterite commented Jun 13, 2018

RX14 commented Nov 6, 2018

asterite commented Nov 6, 2018

RX14 commented Nov 6, 2018 • edited Loading

Blacksmoke16 commented Mar 30, 2020

bcardiff commented Mar 30, 2020

konovod Aug 17, 2017 •

edited

Loading

RX14 commented Aug 17, 2017 •

edited

Loading

RX14 commented Jun 3, 2018 •

edited

Loading

bcardiff commented Jun 4, 2018 •

edited

Loading

RX14 commented Jun 12, 2018 •

edited

Loading

RX14 commented Nov 6, 2018 •

edited

Loading