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!

1 Like

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.

2 Likes

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)

2 Likes

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
1 Like

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.

1 Like

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.

1 Like

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)}})
│└────────────────────
4 Likes