I’m wondering if Elixir’s new type system will permit sum types to be declared…

I don’t believe so. A sum type is a concept from algebraic type systems. Elixir’s type system will use set theoretic types. Briefly,

Algebraic types have:

• Sum types
• Product types

Set theoretic types have:

• Intersection types
• Union types
• Negation types

In both systems, you build more complicated types from the respective primitives. But although there are similarities, the way you compose the types are different.

However,

… and used with exhaustiveness checking?

From the technical paper:

• https://arxiv.org/pdf/2306.06391.pdf (p. 11)

Exhaustivity Checking Type analysis makes it possible to check whether clauses of
a function definition, or patterns in a case expression, are exhaustive, that is, if they
match every possible input value. For instance, consider the following code:

$ type result() =
%{output: :ok, socket: socket()} or
%{output: :error, message: :timeout or {:delay, integer()}}

$ result() -> string()
def handle(r) when r.output == :ok, do: "Msg received"
def handle(r) when r.message == :timeout, do: "Timeout"

We define the type result() as the union of two record types: the first maps the atom :output to the (atom) singleton type :ok and the atom :socket to the type socket(); the second maps :output to :error and maps :message to a union type formed by an atom and a tuple. Next consider the definition of handle: values of type %{output: error, message: {:delay, integer()}} are going to escape every pattern used by handle, triggering a type warning:

Type warning:
| def handle(r) do
      ^^^^^^^^^
    this function definition is not exhaustive.
    there is no implementation for values of type:
      %{output: :error, message: {:delay, integer()}}

Note that the type checker is able to compute the exact type whose implementation is missing, which enables fast refactoring since, as the type of result() or the implementation of handle are modified, the type checker will issue precise new warnings to point out the places where code changes are required.

So although there are no sum types, I believe there will be exhaustiveness checking.

Disclaimer: I have no inside knowledge! I’m just following along as best I can.

Theoretical underpinnings aside, is there any practical difference between an algebraic sum type and a set theoretic union type?

This is a great question and I’m not qualified to answer it fully. I think once us Elixir developers get their hands on the upcoming typing tools, the community will be clamoring articles with titles like these:

• Teach me Set theoretic types like I know the basics of Algebraic types
• Why did Elixir get Set theoretic types instead of Algebraic types?

But I’ll take a stab. Here is one example of how sum types differ from union types: as I understand it, sum types are “tagged” while unions are “untagged”. Take this example:

$type matrix_pills() = :blue or :red
$type light_sabers() = :blue or :green
$type scifi_colors() = matrix_pills() or light_sabers()

Here, :blue is automatically a member of scifi_colors(). There’s no notion of “which” :blue you mean since the union is untagged (it doesn’t matter where it came from).

Contrast that with enum from Rust. If you start with two enums:

enum MatrixPills { Blue, Red }
enum LightSabers { Blue, Green }

There’s no way to combine them such that you get a flat collection of the inner types. You’re stuck with doing things like:

enum ScifiColors1 { MatrixPills, LightSabers }
enum ScifiColors2 { Blue, Red, Green }

With ScifiColors1, Blue is not a member since you need to specify MatrixPills(Blue) or LightSabers(Blue) (i.e. you have to “tag” Blue). With ScifiColors2, Blue is a member but the definition makes no reference to the original enums. So you didn’t really combine them like we were able to with union types.

(This doesn’t mean tagged unions are bad! They’re just different.)

I highly recommend José’s talk from ElixirConf if you want to learn more:

• ElixirConf 2023 - José Valim - The foundations of the Elixir type system

A gradual typesystem cannot prevent runtime errors. It can only make them less likely by checking the inputs of known shape against the expected type, while leaving the unknown shapes unchecked.