Nim: Case does not check all cases.

[sheganinans]

proc case_test(): string = 
  case "1":
  of "": return "empty"
  of "a": return "aye"
  of "b": return "bee"

echo (case_test())

Given this program, I'm expecting the exhaustiveness checker to complain and not compile. But it compiles, returns an empty string, and a 0 exit code.

Additional Information

$ nim -v
Nim Compiler Version 0.20.0

[dumjyl]

This is expected behavior, you'll see the same behavior for floats too.
from the manual:

If there is no else part and not all possible values that expr can hold occur in a slicelist, a static error occurs. This holds only for expressions of ordinal types.

A string is not an ordinal type. There are far too many combinations to do anything useful anyway. Perhaps you would like to use a char?

[Araq]

Indeed, works as designed.

[sheganinans]

Well, this is very strange for a language where the docs claim that case performs exhaustiveness checking. Why would the compiler, behind your back, return a default value such as "" or 0.0??

Because case statements are checked for exhaustiveness during semantic analysis, the value in every of branch must be a constant expression.

I may be misunderstanding but the docs quite clearly say that if the type is non-ordinal, then an else is required. This seems like the compiler should at least complain about the lack of an else, and ideally list the cases that are not covered.

For non ordinal types it is not possible to list every possible value and so these always require an else part.

It seems completely unreasonable for a language that claims to perform static analysis for these common bugs, yet is happy to compile a program where an arbitrary default value is returned instead of an exception. This would be disastrous for larger projects, where tracking back to exactly where in the code the default value was returned would be very difficult.

Compare how this works F#, which is like any other language that actually performs exhaustiveness checking:

// matching on a string, not a char
let case_test () : string =
  match "1" with
  | "" -> "empty"
  | "a" -> "aye"
  | "b" -> "bee"

[<EntryPoint>]
let main argv =
    printfn "%s" <| case_test ()
    0

As expected, you get a warning at compile time, which lists cases that have not been exhausted

/home/ace/src/nim-basics/Program.fs(2,9): warning FS0025: Incomplete pattern matches on this expression. For example, the value '"aa"' may indicate a case not covered by the pattern(s). [/home/ace/src/nim-basics/nim-basics.fsproj]

And when run, it raises an exception with a very nice stacktrace.

Unhandled Exception: Microsoft.FSharp.Core.MatchFailureException: The match cases were incomplete
at Program.case_test() in /home/ace/src/nim-basics/Program.fs:line 5
at Program.main(String[] argv) in /home/ace/src/nim-basics/Program.fs:line 9

As well as, after the program is ran, it returns a proper error code.

ace@xiix:~/src/nim-basics
$ echo $?
134

[nc-x]

@sheganinans

Why would the compiler, behind your back, return a default value such as "" or 0.0??

yet is happy to compile a program where an arbitrary default value is returned instead of an exception.

proc case_test(): string
Because your proc returns a string, and you do not have an explicit return/result in your code, the default value for string (which is empty string) is returned. It has absolutely nothing to do with case. There is an RFC and probably other issues opened regarding removing implicit returns.

ideally list the cases that are not covered.

That is shown where it is possible. For strings (and few others) it is absolutely not possible. A string can have infinitely many possible values.

Maybe, the compiler should always require an else for such cases, cc @Araq .

[dumjyl]

That is an unfortunate inconsistency in the docs.

Case _expressions_ do require exhaustiveness, though the error message could be improved.

proc case_test(): string = 
  return case "1": # static error
  of "": "empty"
  of "a": "aye"
  of "b": "bee"

Maybe, the compiler should always require an else for such cases

FWIW I'm in favor of this, but would likely break a good bit of code right before 1.0.
A --warning[CaseCoverage] would be good if not already existing.

[sheganinans]

@nc-x That seems right. I personally think implicit returns are a bad, bad idea.. As you can see, it interacts really strangely with case. Yes there are an infinite number of cases, so why is it possible for F#, as in my example, to show a subset of the missing values at compile time?

@dumjyl Ah. I didn't consider the case where the return is on the outside. Ah the joys terrors of languages that make the statement/expression distinction..

Here is the error for your version of case_test for reference:

/home/ace/src/nim-basics/basics.nim(3, 17) Error: expression '"empty"' is of type 'string' and has to be discarded

[nc-x]

why is it possible for F#, as in my example, to show a subset of the missing values at compile time

Well technically, it should also be possible for nim, but

For example, the value '"aa"' may indicate a case not covered by the pattern(s).

I personally don't like this error message. I shows a single example of a failure, and if I add another branch with the value given in the example, it would still not compile but now fail with a different example.

IMO, this is more confusing than just saying that 'else' is mandatory with 'case' on type string/whatever because they can have infinitely many possible values

Anyways, making 'else' mandatory should probably be a very small patch.

I personally think implicit returns are a bad, bad idea

(Almost) everybody thinks the same. Hopefully a decision regarding this is made for the 1.0 release.

[sheganinans]

@nc-x Ok, good. I'm glad you say its possible. I was a little confused as to why you said it wouldn't be possible. I guess the error message is just bikeshedding at this point, since case will display the missing cases in an enum.

[sheganinans]

@dumjyl Also, I'm glad to see you're in favor of making this an error/warning. It's said that it's better to break code now and pay the smaller cost, than never be able to fix it. So should this issue be reopened?

[Araq]

The manual is wrong. String cases do not require the else section. IMO. Alternatively the compiler is wrong. :P

[sheganinans]

Well, personally I'd like to see the exhaustiveness checker improved.

At worst you can update the manual to be clear about these special cases.

[Araq]

What's there to be "improved"? You cannot check for string cases "exhaustively". Either the else: discard is assumed or it's enforced. I personally dislike the enforcement but it is what the manual says what should be done.

[andreaferretti]

I think it makes sense for the else: to be enforced, to guarantee exhaustiveness. It is just inconsistent the exhaustiveness is checked for some types and not for others

[sheganinans]

@Araq Well, yes. Following the spec would be an improvement..

Also didn't you see my F# example? It used strings, and they were checked.

In every other relevant language, exhaustiveness is checked on every type.

---

A String is just a product of sums (PoS): https://en.wikipedia.org/wiki/Canonical_normal_form

Put simply:

A Char is just a sum of it's instances:
type Char = 'a' | 'b' | 'c' | ... | 'A' | 'B' | 'C' | ... | '8' | '9' | '0'

And a String is just a product (struct/tuple/list/array/etc) of that sum:
type String = [Char]

This is actually exactly how String is defined in Haskell, as a linked list of char.
It's not very efficient, and that's why there is the packed variant Text, but at least String is simple and sane.

Every non-ordinal type can be decomposed into either a SoP or a PoS. I guarantee this, there is no exception.

Given this view that all non-ordinal types are either a SoP or a PoS, exhaustiveness checking becomes very simple to implement in a generic fashion for all types.

---

This is really just Algebraic DataTypes 101: https://en.wikipedia.org/wiki/Algebraic_data_type

And for a language that claims to support ADTs, I would hope this would have been figured out years ago.

[dumjyl]

Where does nim claim to support ADTs?
Anyway, theory not required. The change is just adding something like this to semCase:

elif caseTyp.kind in {tyFloat..tyFloat128, tyString} and not hasElse:
  localError(c.config, n.info, "error")

and dealing with code breakage.

[sheganinans]

@dumjyl You're right, it doesn't explicitly say that. I inferred that from the term object variant, which 'variant' is commonly understood to be a sum and from this nim wiki entry on sum types.

True, no theory required. Just the minor change you mentioned, and of course all the fallout.