Will the new type system allow defining Sum types?

Questions & Help Questions
, ,
4

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:

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.