Is there a way to statically ensure an if-block covers all enum cases?

Consider:

@enum Level LOW MEDIUM HIGH

function do_stuff(level::Level, args...)
    if level == HIGH
        println("High level")
    elseif level == MEDIUM
        println("Medium level")
    elseif level == LOW
        println("Low level")
    else
        @assert false "Unexpected Level: $level"
    end
    # ... do stuff...
end

Is there any way to statically (ideally at parse-time) enforce that the function is covering all the enum cases?

I think this basically needs to be a macro, like

@full_enum if level == HIGH
    ...
end

or something. Or maybe it needs to be a full blown switch syntax macro in order to ensure it’s parseable.

Does anyone know of a good one here?
Maybe one of the various pattern matching repos?

Thanks!

I’m far from being an expert and probably not the best person to answer this, but no one has answered immediately and it’s something I tried somewhat casually to figure out myself. I do know that SumTypes.jl will generate runtime errors for nonexhaustive matches even when you match against a case that you have covered. And, when I tried it, my memory is that it seemed to play nicely with JET.jl to identify nonexhaustive matches statically.

I believe Moshi.jl has this feature when using its pattern matching via @match (though you’ll need to use it’s ADT created with @data rather than @enum)

Here’s an example!

julia> using Moshi: Data.@data, Match.@match

julia> @data X begin
           a
           b
       end;

julia> @match X.a() begin
           X.a => 1
       end
ERROR: matching non-exhaustive
...

Although I’m a bit confused about this case.

julia> @match X.a() begin
           X.a() => 1
       end
1

I know in Java + IntelliJ, as well as Typescript in VS Code (not sure on the exact configuration here), it’s more of the linter’s job where it will highlight a switch statement on an enum type that doesn’t have a case for all known enum values. That’s tricky for us because we don’t have a dedicated switch statement, but maybe it’s possible to make the Julia linter smart enough to recognize an if-elseif block that is checking enum values? Others would know better, but that sounds pretty hard.

Otherwise, doing a @switchenum macro specific to covering/checking all enum values sounds like it wouldn’t be too hard to implement + have fairly clear/simple semantics.

Speaking purely about @enum, this should actually be possible, but you’ll need some JET plugin/custom abstract interpretation to do so. @enum basically creates a primitive type that subtypes Base.Enum, and keeps a (expanded at parse time!) list of valid enum objects in instances:

julia> @enum A B=2 C=0x1

julia> supertype(A)
Enum{Int32}

julia> instances(A)
(B, C)

julia> B
B::A = 2

julia> C
C::A = 1

julia> B isa A
true

Since this list (barring an invalidation of the instances method…) can’t be changed in a given world age and the individual instances of the enum can’t semantically hold mutable state (thereby ensuring any B is the same as any other B), theoretically a JET plugin/custom abstract interpreter should be able to recognize if/elseif/else syntax attempting to check enum membership for completeness. This would then run whenever type inference runs into branches whose boolean value depends on some function (or only ==) that only takes same-kind enum objects.

One problem here is that the elseif nested nature of the parsed expression no longer exists once the code is lowered:

julia> Meta.@dump if x == B
           print("foo")
       elseif x == C
           print("bar")
       end
Expr
  head: Symbol if
  args: Array{Any}((3,))
    1: Expr
      head: Symbol call
      args: Array{Any}((3,))
        1: Symbol ==
        2: Symbol x
        3: Symbol B
    2: Expr
      head: Symbol block
           # print(foo)
    3: Expr
      head: Symbol elseif
          [...] # check x == C, nested in `Expr(:if)` 

vs.

julia> f(x) = if x == B
           print("foo")
       elseif x == C
           print("bar")
       end
f (generic function with 1 method)

julia> @code_lowered f(A)
CodeInfo(
1 ─ %1 = Main.:(==)
│   %2 = (%1)(x, Main.B)
└──      goto #3 if not %2
2 ─ %4 = Main.print("foo")
└──      return %4
3 ─ %6 = Main.:(==)
│   %7 = (%6)(x, Main.C)
└──      goto #5 if not %7
4 ─ %9 = Main.print("bar")
└──      return %9
5 ─      return nothing
)

So it’s a bit hard to “reextract” that elseif information once you run type inference. It could after all be written as two consecutive if in the original source code!

It’s also a little bit ambiguous if you intentionally only want to check for part of the enum, but for the common case of “I get an A back and need to handle every variant” it should be good enough. Of course, official switch/pattern matching syntax would be even better for this, but I have little hope of that making it into the language.

I think you need the parentheses to construct an instance of the sum type to match against. So your second example would be the correct one. Carrying on from your example:

julia> @match X.a() begin
         X.a => 1
         X.b => 2
       end
ERROR: matching non-exhaustive

julia> typeof(X.a)
DataType

julia> typeof(X.a())
Main.X.Type

So this is a more mundane failure in which the match fails because neither of the types X.a or X.b match the value X.a(). Moshi.jl has a lot of other really nice features, but I don’t think this is one of them.

Oh, thanks for the clarification!

Here’s how you’d do this in SumTypes.jl:

julia> using SumTypes

julia> @sum_type Level begin
           LOW
           MEDIUM
           HIGH
       end

julia> function f(x::Level)
           @cases x begin
               LOW => 1
               MEDIUM => 2
           end
       end

and then we can check with JET.jl to see that it’s statically known that f will error:

julia> using JET

julia> report_call(f, Tuple{Level})
═════ 1 possible error found ═════
┌ f(x::Level) @ Main /home/masonp/.julia/packages/SumTypes/aO6qd/src/cases.jl:118
│┌ assert_exhaustive(::Type{Val{(:LOW, :MEDIUM, :HIGH)}}, ::Type{Val{(:LOW, :MEDIUM)}}) @ SumTypes /home/masonp/.julia/packages/SumTypes/aO6qd/src/cases.jl:6
││ Inexhaustive @cases specification. Got cases (:LOW, :MEDIUM), expected (:LOW, :MEDIUM, :HIGH): SumTypes.assert_exhaustive(::Type{Val{(:LOW, :MEDIUM, :HIGH)}}, ::Type{Val{(:LOW, :MEDIUM)}})
│└────────────────────