Building Erlang + ZX on Devuan Excalibur

With Ubuntu/Kubuntu out of the running for “works and is mostly sane”, we are having to shift once again over to Devuan, which we have been using for servers for several years now at Tsuriai and QPQ, but not as often on desktops (because Kubuntu was just so convenient and changing habits is annoying).

This post will cover Erlang and ZX, specifically, and I’ll do another one about how the app-level transition feels moving from Kubuntu for desktop to Devuan. (Migrating servers from Ubuntu to Devuan is really easy and a major relief: everything is just simpler, flatter, more boring, and works as any SysV init system should.)

TL;DR

As a pseudo script:

# To run the next stuff as root we 'su -'
su -
apt update
apt upgrade
# If installing on a non-graphical system, omit the libwxgtk dep
apt install \
    gcc curl g++ dpkg-dev build-essential automake autoconf \
    libncurses-dev libssl-dev flex xsltproc libwxgtk3.2-dev \
    wget vim git
# Get out of root now and run everything else as a normal user
exit

# Create directories we'll need
mkdir -p ~/vcs ~/bin
# Open a new terminal session for ~/bin to get into $PATH

cd ~/vcs
git clone https://github.com/kerl/kerl.git
cd ~
ln -s ~/vcs/kerl/kerl ~/bin/kerl
kerl update releases
# Pick any version in the list -- I'm working on R27 right now
ERL_VER=27.3.4.12
kerl build $ERL_VER $ERL_VER
kerl install $ERL_VER ~/.erts/$ERL_VER
echo ". \"\$HOME\"/.erts/$ERL_VER/activate" >> .bashrc
echo ". \"\$HOME\"/.erts/$ERL_VER/activate" >> .bash_profile
. ~/.erts/$ERL_VER/activate

# You already have Erlang, this will get you ZX
wget -q https://zxq9.com/projects/zomp/get_zx && bash get_zx

Discussion

The above scriptish version is the cut sheet for me to use later. I haven’t done a discussion explaining what is going on above in a while, and humans stopped reading (and writing) but AI sucks, so here we go, old school HOWTO blog style…

GUI vs TUI

The difference between the non-graphical and graphical build of Erlang in this context is simple:

  • For GUIs, include the libwxgtk3.2-dev dependency.
  • For TUIs, omit the libwxgtk3.2-dev dependency.

I’ll include it below for completeness, but that’s the only difference.

root vs sudo

On Devuan the default is to use a root account rather than sudo. I tend to log in as root using su - instead of actually logging in as root, but that’s mostly because I do this mostly over SSH, and login as root should always be disabled in the SSH config. If you add yourself to the sudoers file, though, you can do it the sudo way you may be familiar with from Ubuntu.

Installing the deps

Everything in this section will either have to be run as root or with sudo.

apt update
apt upgrade
apt install \
    gcc curl g++ dpkg-dev build-essential automake autoconf \
    libncurses-dev libssl-dev flex xsltproc libwxgtk3.2-dev \
    wget vim git

Setting up for, Building and Installing Erlang

First, we are going to be depending on the ~/bin directory being in our path for a bit of this, so create it if it doesn’t already exist. We’ll also use a directory ~/vcs to keep version controlled stuff in one place (so if you have sync scripts for your $HOME, omit both of those from it):

mkdir -p ~/vcs ~/bin

If ~/bin didn’t exist previously, close your terminal and open a new one — this should show up in your default $PATH now. If it doesn’t take because you have chosen a funky window manager, just log out and log back in to force it to take effect.

Once ~bin exists and is in our $PATH we’re going to jump through the following steps:

cd ~/vcs
git clone https://github.com/kerl/kerl.git
ln -s ~/vcs/kerl/kerl ~/bin/kerl
cd ~
kerl update releases
ERL_VER=27.3.4.12
kerl build $ERL_VER $ERL_VER
kerl install $ERL_VER ~/.erts/$ERL_VER
echo ". \"\$HOME\"/.erts/$ERL_VER/activate" >> .bashrc
echo ". \"\$HOME\"/.erts/$ERL_VER/activate" >> .bash_profile
. ~/.erts/$ERL_VER/activate

I installed 27.3.4.12 in the example above because I’m working on something that still uses it, but you can substitute any current version and it should just work. The current latest stable is 28.5.

At this point you have Erlang. Try running erl at your terminal and it should pop up:

ceverett@soba:~$ erl
Erlang/OTP 27 [erts-15.2.7.8] [source] [64-bit] [smp:16:16] [ds:16:16:10] [async-threads:1] [jit:ns]

Eshell V15.2.7.8 (press Ctrl+G to abort, type help(). for help)
1>

Installing ZX

This is the easiest part:

wget -q https://zxq9.com/projects/zomp/get_zx && bash get_zx

You should see roughly this output:

ceverett@soba:~$ wget -q https://zxq9.com/projects/zomp/get_zx && bash get_zx
2026-06-08 17:37:47 URL:https://zxq9.com/projects/zomp/zx-0.14.0.tar.gz [151486/151486] -> "zx-0.14.0.tar.gz" [1]
Erlang found at /home/ceverett/.erts/27.3.4.12/bin/erl
/home/ceverett/bin was found in $PATH. Good to go.
zx found at /home/ceverett/bin/zx. Checking for upgrade.
Running `zx upgrade`...
Recompile: src/zx_zsp
Recompile: src/zx_userconf
Recompile: src/zx_tty
Recompile: src/zx_sup
Recompile: src/zx_proxy
Recompile: src/zx_peers
Recompile: src/zx_peer_sup
Recompile: src/zx_peer_man
Recompile: src/zx_peer
Recompile: src/zx_net
Recompile: src/zx_local
Recompile: src/zx_lib
Recompile: src/zx_key
Recompile: src/zx_daemon
Recompile: src/zx_conn_sup
Recompile: src/zx_conn
Recompile: src/zx_auth
Recompile: src/zx
Current version: otpr-zx-0.14.0
Running latest version.

Now try a zx command, like zx describe gajudesk:

ceverett@soba:~$ zx describe gajudesk
Package : otpr-gajudesk-0.9.0
Name    : GajuDesk
Type    : gui
Desc    : A desktop client for the Gajumaru network of blockchain networks
Author  : Craig Everett <craigeverett@qpq.swiss>
Web     : https://gajumaru.io
Repo    : https://git.qpq.swiss/QPQ-AG/GajuDesk
Tags    : ["gaju","gm","gajumaru","wallet","blockchain","cryptocurrency",
           "crypto","puck"]

Yay! And now you’re all set.

A note on other systems (MacOS and Windows)…

There are signed one-shot installers for Windows and MacOS that will bring in Erlang R27 and ZX with integrated shortcuts available at the ZX/Zomp downloads page.

If you came here to get GajuDesk, there are installers for GajuDesk and GajuDesk + GajuMine that integrate those apps with the desktop for Windows and MacOS (clicky icons and launchers and so on) available here: GajuMining Downloads

A note on GajuMining…

If you came here to run GajuMining on Linux, the above steps all still apply, but there are a handful of additional steps needed, such as adding the qpq and uwiger code realms. The community setup scripts are maintained at Shane Preater’s repo here: https://github.com/shanepreater/gajumaru

But if you already have zx installed by following the steps above, you can shortcut this with:

wget -q https://github.com/shanepreater/gajumaru/raw/refs/heads/main/qpq.zrf
wget -q https://github.com/shanepreater/gajumaru/raw/refs/heads/main/uwiger.zrf
zx import realm qpq.zrf
zx import realm uwiger.zrf
rm uwiger.zrf qpq.zrf

This is how things should go:

ceverett@soba:~$ wget -q https://github.com/shanepreater/gajumaru/raw/refs/heads/main/qpq.zrf
ceverett@soba:~$ wget -q https://github.com/shanepreater/gajumaru/raw/refs/heads/main/uwiger.zrf
ceverett@soba:~$ zx import realm qpq.zrf 
SHA-512 of qpq.zrf: 59082251ED81C63DFC6C3678926DF503CB42118291B3271D3612BD1E7F63AEBDEB296D81AF7446451555B7085E726B6B9C1EC8DBBF3C4C6EDB296B9C257E3AD4
Imported record locally, including a public key.
Added realm qpq.
ceverett@soba:~$ zx import realm uwiger.zrf 
SHA-512 of uwiger.zrf: 704530801DF3E54D069FACD93F772FCAC8A6E776389CDE8F4F034DE1A0A516B0D44FFB3DDD88C2A82C015CB14218C17172099E477E28B3A5E293D2CC08F20000
Imported record locally, including a public key.
Added realm uwiger.
ceverett@soba:~$ zx list realms
otpr
qpq
uwiger
ceverett@soba:~$ zx describe qpq-gajumine
Package : qpq-gajumine-0.4.2
Name    : GajuMine
Type    : gui
Desc    : Mining client for the Gajumaru Root
Author  : Craig Everett <craigeverett@qpq.swiss>
Web     : https://gajumining.com
Repo    : https://git.qpq.swiss/zxq9/GajuMine
Tags    : ["qpq","gaju","gajumaru","hive","mining","crypto"]

And that’s it. You can do CPU mining with the GUI client by running zx run qpq-gajumine or headless with a GPU setup by following the advice on Shane’s repo.

Permalink

Elixir v1.20 released: now a gradually typed language

In 2022, we announced the effort to add set-theoretic types to Elixir. In June 2023, we published an award winning paper on Elixir’s type system design and said our work was transitioning from research to development.

With Elixir v1.20, we have completed our first development milestone which is to perform type inference and gradually type check every Elixir program, without introducing type annotations. This means Elixir increasingly reports dead code and verified bugs: typing violations that are guaranteed to fail at runtime if executed. Elixir can find verified bugs in existing programs efficiently, without introducing developer overhead, and with an extremely low false positives rate.

In this announcement, we will break down the type system goals, what the dynamic() type means in Elixir, and how it finds verified bugs. In particular, our implementation performs well in the “If T: Benchmark for Type Narrowing” benchmark. Elixir passes 12 of the 13 categories, showing that it can recover precise type information from ordinary Elixir code, which we use to find verified bugs in dynamically typed programs.

The type system was made possible thanks to a partnership between CNRS and Remote. The development work is currently sponsored by Fresha, and Tidewave.

Types, in my Elixir?

Our goal is to introduce a type system which is:

  • sound - the types inferred and assigned by the type system align with the behaviour of the program

  • gradual - Elixir’s type system includes the dynamic() type, which can be used when the type of a variable or expression is checked at runtime. In the absence of dynamic(), Elixir’s type system behaves as a static one

  • developer friendly - the types are described, implemented, and composed using basic set operations: unions, intersections, and negations (hence it is a set-theoretic type system), with clear error messages

Introducing a type system into an existing language is a complex change. For this reason, our first milestone was to implement the type system without introducing typing annotations but still have it provide value to developers by finding dead code and verified bugs. This is done through the dynamic() type, which in Elixir is quite different from other gradually typed languages. Let’s break it down.

The dynamic() type

Many gradual type systems have the any() type, which, from the point of view of the type system, often means “anything goes” and no type violations are reported. On the other hand, Elixir’s gradual type is called dynamic() and it has two important properties: compatibility and narrowing.

In static type systems, when you have a type of shape integer() or binary() and you invoke a function, said function must accept both types. However, because type systems cannot capture the intention of all of our programs with precision, this may lead to false positives. For example, take the simple code below:

def percentage_or_error(value) when is_integer(value) do
  value_or_error =
    if value > 1 do
      value
    else
      "not well"
    end

  # ... more code ...

  if value > 1 do
    value_or_error / 100
  else
    String.upcase(value_or_error)
  end
end

Although value_or_error has type integer() or binary(), the operator / accepts only numbers, and String.upcase accepts only binaries/strings, the program above is valid and emits no exceptions at runtime. However, a type system would still report two violations, because the types supplied to / and String.upcase are not a subtype of the accepted types.

While the program above could be better written to have no typing violations, type systems will always reject valid programs, and if Elixir were to introduce too many false positives in existing codebases, it would quickly erode the trust in the type system. Therefore, Elixir’s gradual type system tags the value_or_error variable above with the type dynamic(integer() or binary()), which means the type is either integer() or binary() at runtime.

When calling a function with a dynamic() type, Elixir will only emit a typing violation if the supplied types and the accepted types are disjoint. In the program above, even though / expects only numbers, dynamic(integer() or binary()) can be an integer() and given the accepted and supplied types are not disjoint, there are no typing violations. However, if we were to change the program to this:

value_or_error =
  if value > 1 do
    value
  else
    "not well"
  end

Map.fetch!(value_or_error, :some_key)

Because Map.fetch! expects a map data structure, and value_or_error can only be integer or binary at runtime, the accepted and supplied types are disjoint, which turns into a violation. This is known as the compatibility property and it explains how Elixir reports only verified bugs.

However, reporting only verified bugs would not be useful if we can’t find many bugs in the first place. We addressed this problem by making sure Elixir’s dynamic type can be narrowed. Take this code:

def add_a_and_b(data) do
  data.a + data.b
end

In the program above, data starts as a dynamic() type. We then use it as data.a and data.b inside the plus operator, so Elixir will refine the data variable to have type %{..., a: number(), b: number()}, which implies it is a map with both a and b fields with number values (and potentially any other field, hence the leading ...). Therefore, if you were to forget to select the .b field and write this:

def add_a_and_b(data) do
  data.a + data
end

data would be first narrowed to a map of shape %{..., a: number()}, then attempted to be used as a number(), which would emit a violation.

In other words, the dynamic() type in Elixir effectively works as a range, which can be refined as it is used throughout the program and reports violations whenever type checks fall outside of the range. This is a contrast to other gradual type systems, which use the dynamic type to discard all type information.

Behind the scenes, our type inference and type checking algorithms behave as if we annotated all argument types as dynamic(). Once we introduce user-supplied type annotations, Elixir’s type system will behave as any statically typed language as long as dynamic() is not used. And whenever you cross the static-dynamic boundary, we developed new techniques that ensure our gradual typing is sound, without a need for additional runtime checks.

Typing guards, clauses, and more

Most of the work behind this release was to introduce type checking and narrowing to several constructs. Let’s see some of them.

When it comes to guards, we can infer unions, intersections, and negations:

def example(x, y) when is_list(x) and is_integer(y)

The code above correctly infers x is a list and y is an integer.

def example({:ok, x} = y) when is_binary(x) or is_integer(x)

The one above infers x is a binary or an integer, and y is a two element tuple with :ok as first element and a binary or integer as second.

def example(x) when is_map_key(x, :foo)

The code above infers x is a map which has the :foo key, represented as %{..., foo: dynamic()}. Remember the leading ... indicates the map may have other keys.

def example(x) when not is_map_key(x, :foo)

And the code above infers x is a map that does not have the :foo key, which has the type: %{..., foo: not_set()}. Hence x.foo within the function body will raise a typing violation.

You can also have expressions that assert on the size of data structures:

def example(x) when tuple_size(x) < 3

Elixir will correctly track the tuple has at most two elements, and therefore accessing elem(x, 3) will emit a typing violation. For maps and lists, we convert size checks into emptiness ones. In other words, Elixir can look at complex guards, infer types, and use this information to find bugs in our code.

When it comes to constructs such as case and conditionals, Elixir uses information from previous clauses to refine subsequent ones:

case System.get_env("SOME_VAR") do
  nil -> :not_found
  value -> {:ok, String.upcase(value)}
end

System.get_env("SOME_VAR") returns either nil or a binary(). Because the first clause matches on nil, the type system knows value can no longer be nil, and therefore it must only be a binary(), which allows the second clause to also type check without violations. Narrowing across clauses also helps the type system find redundant clauses and dead code in existing codebases.

Furthermore, we have typed many functions in the standard library that work with tuples and maps. You can find more details in the release notes.

Compilation time improvements

Elixir v1.20 also improves compilation times once more, especially on applications running on machines with many cores. Even though BEAM languages are efficient to compile in general, our synthetic benchmarks now place Elixir’s build tool as the fastest among them. If you would like to contribute more examples and scenarios, please start a discussion so we can provide a transparent suite of benchmarks and results.

It also introduces a new compiler option called :module_definition, which specifies if the module definition should be :compiled (the default) or :interpreted. This may improve compilation times in large projects and it does not affect the .beam files written to disk, only how the contents inside defmodule are executed. You can enable it by setting elixirc_options: [module_definition: :interpreted] in your mix.exs. Read the documentation to learn more.

What is next?

The biggest question ahead of us is: when will Elixir introduce new type signatures that leverage set-theoretic types? As recently discussed in my ElixirConf EU 2026 keynote, we still have both research and development work ahead of us. We will only introduce type signatures:

  • if we are satisfied with the type system performance in Elixir v1.20 (and we have done extensive work optimizing it)
  • if we can implement recursive types efficiently
  • if we can implement parametric types efficiently
  • if we can implement traversing key-value pairs of maps as an enumerable efficiently (we are still researching the possible solutions here)

Once those problems are tackled, we will start to explore and discuss typed struct definitions and finally type signatures. As usual, we will keep the community posted through news and in the Elixir Forum.

We appreciate everyone who tried the release candidates, ran benchmarks, and gave us feedback! Give Elixir v1.20 a try and remember to fix all of the bugs it will find for free!

Permalink

Erlang/OTP 29.0

OTP 29.0

Erlang/OTP 29 is a new major release with new features, improvements as well as a few incompatibilities. Some of the new features are highlighted below.

Many thanks to all contributors!

Highlights

  • Added support for -unsafe attributes for marking functions as unsafe to use. The compiler will by default now generate warnings for calls to functions in Erlang/OTP known to be always unsafe. Furthermore, xref can now be used to find calls to unsafe functions and functions that lack documentation.

  • The SSH daemon now defaults to disabled for shell and exec services, implementing the “secure by default” principle. This prevents authenticated users from executing arbitrary Erlang code unless explicitly configured.

  • The SFTP subsystem is no longer enabled by default when starting an SSH daemon.

  • In SSL, the post quantum hybrid algorithm x25519mlkem768 is now the most preferred key exchange group in the default configuration.

  • The module io_ansi allows the user to emit Virtual Terminal Sequences (also known as ANSI sequences) to the terminal in order to add colors/styling to text or to create fully fledged terminal applications.

  • The new ct_doctest module allows the user to test documentation examples in Erlang module docs and documentation files.

  • The ignore_xref attribute has been handled as a post-analysis filter by build tools such as Rebar3. In this release, [xref] itself does the filtering, ensuring that all tooling that calls xref for any purpose can rely on these declarations to just work.

General

  • In the default code path for the Erlang system, the current working directory (.) is now in the last position instead of the first.

  • There is no longer a 32-bit Erlang/OTP build for Windows.

New language features

  • Native records as described in EEP-79 has been implemented. A native record is a data structure similar to the traditional tuple-based records, except that is a true data type. Native records are considered experimental in Erlang/OTP 29 and possibly also in Erlang/OTP 30.

  • The new is_integer/3 guard BIF makes it possible to easily verify that a value is both an integer and within a certain range. For example: is_integer(I, 0, 100)

  • Multi-valued comprehensions according to EEP 78 are now supported. For example, [-I, I || I <- [1, 2, 3]] will produce [-1,1,-2,2,-3,3].

  • By enabling the compr_assign feature, it is now possible to bind variables in a comprehensions. For example: [H || E <- List, H = erlang:phash2(E), H rem 10 =:= 0]

Compiler and JIT improvements

  • In the documentation for the [compile] module, there is now a section with recommendations for implementors of languages running on the BEAM.

  • The JIT now generates better code for matching or creating binaries with multiple little-endian segments.

  • The compiler will generate more efficient code for map comprehensions with constant values that don’t depend on the generator. Example: #{K => 42 || K <- List}

Compiler warnings

There are several new compiler warnings enabled by default. For each such warning, there is an option to disable it.

  • There will now be a warning when using the catch operator, which has been deprecated for a long time. It is recommended to instead use try…catch but is also possible to disable the warning by using the nowarn_deprecated_catch option.

  • There will now be a warning when exporting variables out of a subexpression. For example: file:open(File, AllOpts = [write, {encoding,utf8}]). This warning can be disabled using the nowarn_export_var_subexpr compiler option.

  • The compiler will now warn for uses of the and and or operators. This warning can be disabled using the nowarn_obsolete_bool_op compiler option.

  • The compiler will now warn for matches such as {a,B} = {X,Y}, which is better written as {a=X,B=Y}. This warning can be disabled using the nowarn_match_alias_pats option.

For a long time, there has been a warning for using the obsolete guard tests (such as list(L) instead of is_list(L). In Erlang/OTP 30, the old guards will be removed from the language.

STDLIB

  • There are new functions for randomly permutating a list: rand:shuffle/1 and rand:shuffle_s/2.

SSH

  • The default key exchange algorithm is now mlkem768x25519-sha256, a hybrid quantum-resistant algorithm combining ML-KEM-768 with X25519. This provides protection against both classical and quantum computer attacks while maintaining backward compatibility through automatic fallback to other algorithms when peers don’t support it.

For a full list and more details about new features and potential incompatibilities see the README.

Permalink

Erlang/OTP 28.5 Release

OTP 28.5

Erlang/OTP 28.5 is the fourth maintenance patch package for OTP 28, with mostly bug fixes as well as a few improvements.

HIGHLIGHTS

There is a new “Secure Coding Guidelines” document in Design Principles describing how to write secure Erlang code.

Improvements and New Features

  • A new configure option --{enable,disable}-use-embedded-3pp-alternatives has been added. When enabled, configure is forced to find alternatives, to a subset, of the embedded third-party products (3pps) in the runtime system, and when disabled, configure will use all internal embedded 3pps. Currently this option affects zstd, zlib, ryu (with STL), openssl and tcl. The default is to use all built-in embedded 3pps except for zlib which by default will use zlib on the OS if available.

    Requirements for alternatives:

    • zstd - Static library and include files of at least version 1.5.6 needs to be available.
    • zlib - Library and include files of at least version 1.2.5 needs to be available.
    • ryu (with STL) - A usable C++ compiler with C++17 support.
    • openssl - No requirements. Our own MD5 implementation will be used.
    • tcl - The strerrorname_np() function (introduced in glibc 2.32) mapping errno integers to symbolic names needs to be available.

    The argument embedded_3pps has been added to erlang:system_info/1. It returns a map with information about the use of embedded 3pps in the runtime system.

For details about bugfixes and potential incompatibilities see the Erlang 28.5 README

The Erlang/OTP source can also be found at GitHub on the official Erlang repository, https://github.com/erlang/otp

Download links for this and previous versions are found here:

Permalink

Lazy BDDs with eager literal differences

In a previous article, we discussed how we optimized intersections in Elixir set-theoretic types to improve performance.

In a nutshell, lazy BDDs allow us to represent set-theoretic operations at any depth. And while this is useful in many cases, they offer a downside when it comes to intersections. For example, take this type:

(%Foo{} or %Bar{} or %Baz{} or %Bat{}) and %Bar{}

While we could store the above as-is in the BDD, from a quick glance it is clear that the above can only be equal to %Bar{}. To address this, we made intersections eager, removing the size of BDDs and drastically improving compilation times.

Lately, Elixir v1.20.0-rc.2 introduced new improvements to the type checker. Among them is the ability to propagate type information across clauses and check for redundant clauses. For example, take this code:

def example(x) when is_binary(x), do: ...
def example(x) when is_integer(x), do: ...
def example(x), do: ...

In the first clause, we know the argument is a binary. In the second, we know it is an integer. Therefore, in the third one, even though there are no guards, we know x has type not binary() and not integer(). In other words, the type of a given clause is computed by the type of its patterns and guards, minus the types of the previous clauses.

Furthermore, we can now check if a clause is redundant by checking if its type definition is a subset/subtype of the previous ones. For example, if you have three clauses, each with type clause1, clause2, and clause3, you know clause3 is redundant if its type is contained in the union of the types of clause1 and clause2:

clause3 ⊆ (clause1 ∪ clause2)

In set-theoretic types, a type is a subtype of the other if it is a subset of said type, so we will use these terms interchangeably. Furthermore, checking if a type is a subset/subtype of another can be done by checking if the difference between clause3 and the union of the clauses is empty. In Elixir terms:

empty?(difference(clause3, union(clause1, clause2)))

Long story short: with Elixir v1.20.0-rc.2, the type system is seeing an increasing number of differences. Projects where modules had 1000+ of clauses were taking too long to compile, so it was time to derive new formulas and optimizations.

As with previous articles, we discuss implementation details of the type system. You don’t need to understand these internals to use the type system. Our goal is simply to document our progress and provide guidance for future maintainers and implementers. Let’s get started.

A recap on lazy BDDs and literals

A lazy BDD has type:

type lazy_bdd() = :top or :bottom or
  {type(), constrained :: lazy_bdd(), uncertain :: lazy_bdd(), dual :: lazy_bdd()}

where type() is the representation of the actual type. For example, if the type being represented is a tuple, type() would be a list of all elements in the tuple. In literature, type() is known as literal.

Throughout this article, we will use the following notation to represent lazy BDDs:

B = {a, C, U, D}

where B stands for BDD, a is the literal, C is constrained, U is uncertain, and D is dual. Semantically, the BDD above is the same as:

B = (a and C) or U or (not a and D)

Which means the following expression, where foo, bar, baz, and bat below represent types:

(foo and not (bar or (baz and bat))

will be stored as:

{foo,
 {bar, :bottom, :bottom,
  {baz, :bottom,
   {bat, :bottom, :bottom, :top}, :top}, :bottom, :bottom}

Eager literal differences

The main insight of the previous article was, when intersecting two BDDs:

B1 = {a1, C1, U1, D1}
B2 = {a2, C2, U2, D2}

if the intersection between a1 and a2 is disjoint (i.e. it returns the empty type), we can likely build new formulas that eliminate many nodes from the BDD recursively.

The goal is to apply the same optimization for differences. In particular, there are two properties that we can leverage from differences. Take the difference between a1 and a2. If they are disjoint, they have nothing in common, and the result is a1. On the other hand, if a1 is a subtype of a2, then the difference is empty.

Furthermore, for simplicity, we will only optimize the cases where at least one of the sides is exclusively a literal, which means that C = :top, U = :bottom, and D = :bottom. Let’s get to work!

Literal on the right-hand side

We want to derive new formulas for the difference when B2 is a literal. Let’s start with the base formula:

B1 and not B2

where B1 is (a1 and C1) or U1 or (not a1 and D1) and B2 is simply a2. So we have:

((a1 and C1) or U1 or (not a1 and D1)) and not a2

Now let’s distribute and not a2:

(a1 and not a2 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

When they are disjoint, a1 and not a2 is simply a1, so we have:

(a1 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

When a1 is a subtype of a2, a1 and not a2 is empty, plus not a1 and not a2 is the same as not (a1 or a2), which is the same as not a2. So we have:

(U1 and not a2) or (D1 and not a2)

In both formulas, and not a2 is then applied using the same eager literal difference recursively.

Literal on the left-hand side

Now let’s derive new formulas for the difference when B1 is a literal. This means we want to compute:

B1 and not B2

Which we can expand to:

a1 and not ((a2 and C2) or U2 or (not a2 and D2))

Now let’s distribute the not over the right-hand side:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

When a1 and a2 are disjoint, we know that a1 and (not a2 or not C2) is a1. This is because if we distribute the intersection, we end up with (a1 and not a2) or (a1 and not C2). And since a1 and not a2 is a1, we end up with a1 unioned with a type that is a subset of a1, hence a1.

So we end up with:

a1 and (not U2) and (a2 or not D2)

And if a1 and a2 are disjoint, the intersection between them is empty, so we are left with the following disjoint formula:

a1 and not D2 and not U2

When a1 is a subtype of a2, we can simplify two expressions in the initial formula. Let’s look at it again:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

First we distribute the intersection in a1 and (not a2 or not C2). We will have two parts, a1 and not a2, which is empty, unioned with a1 and not C2, resulting in:

a1 and (not C2) and (not U2) and (a2 or not D2)

Now we can distribute a1 and (a2 or not D2). And because a1 and a2 is a1 (since a1 is a subset), we end up with a1 or (a1 and not D2), which is a1. So our subset formula becomes:

a1 and not C2 and not U2

As you can see, these new formulas can reduce the amount of nodes in the BDD drastically, which lead to much better performance.

One last trick: one field difference

The optimizations above lead to excellent performance. Projects that would take dozens of seconds to compile could now do so in milliseconds. However, there were still some cases where the optimizations could not kick-in, leading to worse performance. In particular, with structs.

When working with a struct in Elixir, the fields will most often have the same type, except for one. For example:

def example(%MyStruct{x: x}) when is_binary(x)
def example(%MyStruct{x: x}) when is_integer(x)
def example(%MyStruct{x: x})

In the example above, x in the third clause starts with the value of term, so the last struct is a supertype of the other ones, and our optimizations do not apply. Therefore, the type of the third clause would be:

%MyStruct{x: term()} and not %MyStruct{x: integer()} and not %MyStruct{x: binary()}

However, whenever only one of the fields are different, we can translate the above as the difference of said field, so instead we could have:

%MyStruct{x: term() and not integer() and not binary()}

All we need to do is to compute new formulas. So let’s do it one last time. For our last batch of formulas, we will need three new types: a_diff which is a new literal where we compute the difference between the only different field (as done above), as well as a_int and a_union, which is respectively the intersection and union of the distinct field.

Literal on the right-hand side

Our formula for B1 and not B2 with a literal on the right-hand side is:

(a1 and not a2 and C1) or (U1 and not a2) or (not a1 and not a2 and D1)

a1 and not a2 is a_diff. not a1 and not a2 is the same as (not (a1 or a2)) which is the same as not a_union, so we end up with:

(a_diff and C1) or (U1 and not a2) or (not a_union and D1)

Literal on the left-hand side

Our starting point is:

a1 and (not a2 or not C2) and (not U2) and (a2 or not D2)

By distributing the first intersection, we have:

((a1 and not a2) or (a1 and not C2)) and not U2 and (a2 or not D2)

We know that a1 and not a2 is a_diff. So let’s slot that in and change the order of operations:

(a_diff or (a1 and not C2)) and (a2 or not D2) and not U2

We now distribute (a_diff or (a1 and not C2)) and (a2 or not D2):

((a_diff and (a2 or not D2)) or
 ((a1 and not C2) and (a2 or not D2))) and not U2

a_diff and a2 is empty, so the first and becomes a_diff and not D2. Then we distribute the second and and, after replacing a1 and a2 by a_int, we get the following:

((a_diff and not D2) or
 (a_int and not C2) or
 (a1 and not C2 and not D2)) and not U2

At this point, I thought no further simplifications were possible. That’s when I reached to a coding agent to explore alternative variations and it suggested the following “obvious-only-in-hindsight” simplication. We know that a1 = a_diff or a_int, so let’s slot that in:

((a_diff and not D2) or
 (a_int and not C2) or
 ((a_diff or a_int) and not C2 and not D2)) and not U2

Now if we distribute (a_diff or a_int) and not C2 and not D2), we get:

((a_diff and not D2) or
 (a_int and not C2) or
 (a_diff and not C2 and not D2) or
 (a_int and not C2 and not D2)) and not U2

However, we know that (a_diff and not D2 and not C2) is a subtype of (a_diff and not D2) (as it is the same set minus C2), and the same applies to (a_int and not C2 and not D2). And then union of two types a or b, when b is a subset, is always a. Therefore both terms can be fully discarded, so we end up with:

((a_diff and not D2) or (a_int and not C2)) and not U2

Summary

We implemented all simplifications above and they will be available in full as part of Elixir v1.20.0-rc4. At the moment, we have measured clear impact from the “literal on the left-hand side” optimizations, allowing us to drastically improve the type system performance when checking thousands of clauses or large structs. At the moment, we did not spot any scenarios where the right-hand side optimizations were useful, most likely because it does not show up in codebases (yet).

We will continue assessing the performance of the type system as we add more features based on community feedback.

Permalink

Lazy BDDs with eager literal intersections

In a previous article, we discussed how Elixir changed its set-theoretic types representation from Disjunctive Normal Forms (DNFs) to Lazy Binary Decision Diagrams (Lazy BDDs).

In a nutshell, DNFs allow us to represent unions, intersections, and negations as a flat data structure:

(c1 and not d1) or (c2 and not d2) or (c3 and not d3) or ...

This meant that any operation between complex types was immediately flattened. For example, intersections of unions, such as (foo or bar) and (baz or bat), had to be immediately flatten into the cartesian production (foo and baz) or (foo and bat) or (bar and baz) or (bar and bat). Even worse, unions of differences could lead to exponential expansion.

Elixir v1.19 then introduced BDDs with lazy unions (in short, lazy BDDs). They are trees which allow us to represent set-theoretic operations of any arbitrary depth, without flattening them, while also detecting duplicate types. A lazy BDD has type

type lazy_bdd() = :top or :bottom or
  {type(), constrained :: lazy_bdd(), uncertain :: lazy_bdd(), dual :: lazy_bdd()}

where type() is the representation of the actual type. For example, if the type being represented is a tuple, type() would be a list of all elements in the tuple. In literature, type() is known as literal.

Throughout this article, we will use the following notation to represent lazy BDDs:

B = {a, C, U, D}

where B stands for BDD, a is the literal, C is constrained, U is uncertain, and D is dual. Semantically, the BDD above is the same as:

B = (a and C) or U or (not a and D)

Which means the following expression, where foo, bar, baz, and bat below represent types:

(foo and not (bar or (baz and bat))

will be stored as:

{foo,
 {bar, :bottom, :bottom,
  {baz, :bottom,
   {bat, :bottom, :bottom, :top}, :top}, :bottom, :bottom}

The conversion to lazy BDDs and a few optimizations we added to their formulation in literature allowed us to type check Elixir programs faster, despite Elixir v1.19 performing more type checks than v1.18!

However, when working on Elixir v1.20, which introduced type inference of all constructs, we noticed some of the downsides of lazy BDDs. This article explores these downsides and how we addressed them.

As with previous articles, we discuss implementation details of the type system. You don’t need to understand these internals to use the type system. Our goal is simply to document our progress and provide guidance for future maintainers and implementers. Let’s get started.

The trouble with laziness

As we described above, lazy BDDs allow us to represent set-theoretic operations at any depth. And while this is useful in many cases, they offer a downside when it comes to intersections. For example, take this type:

(%Foo{} or %Bar{} or %Baz{} or %Bat{}) and %Bar{}

While we could store the above as a BDD, it is also clear that the above can only be equal to %Bar{}. In other words, if we resolve intersections eagerly, we will most likely reduce the tree size, speeding up all future operations! To do this, we need to compute the intersection between literal types (the first element of the BDD node), rather than intersections between BDDs. So we are naming these new optimizations eager literal intersections.

Eager literal intersections

Our goal is to apply intersections between literals as soon as possible as it helps us reduce the size of the tree whenever literal intersections are empty.

Take two BDDs:

B1 = {a1, C1, U1, D1}
B2 = {a2, C2, U2, D2}

And imagine there is a function that can compute the intersection between a1 and a2 (which is the intersection of literals, not BDDs). The optimization works as long as one of C1 or C2 are :top. In this case, let’s choose C2, so we have:

B1 = (a1 and C1) or U1 or (not a1 and D1)
B2 = a2 or U2 or (not a2 and D2)

The intersection of B1 and B2 can be computed as:

B1 and (a2 or U2 or (not a2 and D2))

Let’s distribute it:

(a2 and B1) or (U2 and B1) or ((not a2 and D2) and B1)

And expand the first B1:

(a2 and ((a1 and C1) or U1 or (not a1 and D1))) or
  (U2 and B1) or ((not a2 and D2) and B1)

And now let’s distribute a2 while reordering the arguments:

(((a1 and a2) and C1) or (a2 and U1) or ((a2 and D1) and not a1) or
  (U2 and B1) or ((not a2 and D2) and B1)

In the first term of the union, we have a1 and a2 as a literal intersection. If a1 and a2 is empty, then the whole C1 node can be eliminated.

Then we proceed recursively intersect a2 with every literal node in a2 and U1 and a2 and D1. And, if their literal nodes are empty, those subtrees are eliminated too. This may allows us to cut down the size of tree considerably! In our benchmarks, these optimizations allowed us to reduce type checking of a module from 10s to 25ms.

The remaining terms of the union are U2 and B1 and (not a2 and D2) and B1. If desired, we could apply the same eager literal intersection optimization to U2 and B1 (as long as the constrained part in either U2 or B1 are :top).

This optimization has worked quite well for us but there are some pitfalls one must be aware of. The first of them is to consider how expensive it is to compute that the literal intersection is empty. Since this is an optimization, the check itself does not have to be complete and you can optimize only certain idioms.

Another option is to have the “eager literal intersection” always compute a new literal, which is then reinserted into the BDD. This is the approach done by the Elixir compiler but one has to be additionally careful because, if a new literal node is computed, then it has to be resorted within the BDD, which may be too expensive. If most of the intersections are eliminated, then computing the eager literal intersections is still beneficial, but that may not always be the case.

Let’s explore one example where these trade-offs may be problematic by discussing open vs closed types.

Open vs closed types

Elixir’s type system can represent both open and closed maps. When you write:

user = %{name: "john", age: 42}

We are certain the map has keys :name and :age and only those keys. We say this map is closed, as it has no other keys, and it would have the type %{name: binary(), age: integer()}.

However, when you pattern match on it:

def can_drive?(%{age: age}) when is_integer(age) and age >= 18

Because pattern matching only validates the age key, a map given as argument may have other keys! Therefore, we say the map is open and it has the type %{..., age: integer()}. This type says the map may have any keys but we are sure the age is integer().

The trouble is that, when we are intersecting two maps, because the open map is very broad, their intersection rarely eliminate entries. For example, the intersection between %{..., age: integer()} and %{..., name: binary()} is the map %{..., name: binary(), age: integer()}.

So when we have to compute the intersection between (foo or bar) and (baz or bat) and foo, bar, baz, and bat are open maps with different keys, then it will generate a cartesian product of all combinations! However, if they were closed maps, the end result would be empty. For this reason, we recommend applying the eager literal intersection only when the intersection will often lead to empty types.

Results

We initially implemented eager literal intersections as part of Elixir v1.20 release, which reduced the type checking time of one of the pathological cases from 10 seconds to 25ms!

However, our initial implementation also caused a performance regression, as we did not distinguish between open and closed maps. This regression was addressed by applying the optimization only to closed maps, as discussed in the article.

Permalink

Copyright © 2016, Planet Erlang. No rights reserved.
Planet Erlang is maintained by Proctor.