Will the new type system allow defining Sum types?

Oh, I would very much like to know as well.

Why? I’d expect they’d be written in the BEAM “tuple with a leading atom” idiom. A complex example, from gen_statem:

action() =
    postpone |
    {postpone, Postpone :: postpone()} |
    {next_event,
     EventType :: event_type(),
     EventContent :: event_content()} |
    {change_callback_module, NewModule :: module()} |
    {push_callback_module, NewModule :: module()} |
    pop_callback_module |
    enter_action()

Exhaustiveness checking is mostly a difference of interpretation; if Dialyzer sees code like this:

case some_function_that_returns_action() do
  {:postpone, p_value} -> ...
  :pop_callback_module -> ...
end

it will assume that some_function_that_returns_action can’t return the other variants of action and try to derive a contradiction. It will also complain about dead code if subsequent analysis proves some_function_that_returns_action never returns :pop_callback_module.

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.

@dimitarvp @billylanchantin
Thanks for helping me to get a better understanding of this.

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

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

and translating to something using ADTs like Rust (please excuse likely errors in this example as I haven’t written Rust in a long time and I’m a bit, errr, rusty):

struct Socket {
    socket: String
}

enum Message {
    Timeout,
    Delay(i32)
}

enum MyResult {
    Ok(Socket),
    Err(Message)
}

fn handle(result: MyResult) -> String {
    match result {
        Ok(socket) => socket.socket,
        Err(msg) => helper_fn_to_make_msg_a_string(msg)
    }
} 

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

From my point of view, since the 3 members of your union are disjoint / clearly discriminated, I don’t see any practical difference with a sum type (in fact they look to me like tagged union members).

It would however be trickier with shape-compatible structs, should the struct name behave as a discriminant if the inner data has the same shape ?

What a great explanation of the differences. Thanks for taking the time!

@antoine-duchenet – since Elixir structs are maps with a private __struct__ field I would assume the struct name could be matched on or not just as any other field.

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

could be satisfied by any struct that matches on the specified fields.

iex(1)> defmodule Result do 
    defstruct output: :ok, socket: %{}
end

(2)> s = %Result{}
%Result{output: :ok, socket: %{}}

(3) m = %{output: :ok, socket: %{just_a: :map}}
%{output: :ok, socket: %{just_a: :map}}

(4) fun = fn %{output: :ok} = a -> a.socket
    a -> a
end

(5) fun.(s)
%{}

(6) fun.(m)
%{just_a: :map}

(7) fun.(%{output: :error, message: :timeout})
%{output: :error, message: :timeout}

So I would expect that the __struct__ field would get ignored unless the definition of the type specifically matches on that field.

Yes indeed !

My question was more about the behavior desired by the community than the expected behavior with the “current” implementation, expecially concerning exhaustiveness checking.

With something like that :

$ type result() = %Dog{name: string()} or %Cat{name: string()}

$ result() -> string()
def handle(%{name: name}), do: "Hello  #{name}"

Which could be considered as syntaxic sugar to write this :

$ type result() = %{__struct__: :Dog, name: string()} or %{__struct__: :Cat, name: string()}

$ result() -> string()
def handle(%{name: name}), do: "Hello  #{name}" 

1. If the output type behaves like an union type (the way you assume it would), simplified to something like type result() = %{__struct__: :Dog or :Cat, name: string()} , I’d expect the handle/1 function not to raise a “not exhautive” warning because its matching (seen as a set) “contains” every possible value of the result type.
   To raise a warning, we would have to define def handle(%Dog{name: name}), do: "Hello #{name}" because this definition does not handle the %Cat{} case.

2. In an hypotetical world where the __struct__ field receives some special treatment to behave like the discriminant of the sum (a.k.a. the tag of the tagged union), we could imagine the handle/1 function to raise a “not exhautive” warning because its matching (seen as a set) is fully disjoint with the result type (it could be seen as if it meant def handle(%{__struct__: nil, name: name})). This behavior would be closer to the enum wrappers often used in Rust like Ok/Err.
   In such a world, we would have to define def handle(%Dog{name: name}) and def handle(%Cat{name: name}).

I’m personally fine with 1. since it looks more Elixirish and flexible to me but 2. may have some benefits.

The way you have defined the result type does match on __struct__ though, so I would expect in that situation for option #2 to be enforced because while all Cats and all Dogs contain names not every map that contains a name will be a Dog or a Cat and therefore not sufficient to satisfy the type result.