Elixir: Lazier Binary Decision Diagrams (BDDs) for set-theoretic types

[NewsBot]

A new Elixir blog post/announcement has been posted!

The Elixir team and the CNRS are working on a set-theoretic type system for Elixir which, simply put, is a type-system powered by unions, intersections, and negations. As part of the implementation of said type systems, we need an efficient way of representing said operations. This article discusses the existing approaches found in theory and practice, as well as the improvements we have introduced as part of Elixir v1.19.

This article covers the implementation details of the type system. You don’t need to understand these internals to use the type system, just as you don’t need to know virtual machine bytecodes or compiler passes to use a programming language. Our goal is to document our progress and provide guidance for future maintainers and implementers. Let’s get started.

DNFs - Disjunctive Normal Forms

A Disjunctive Normal Form (DNF) is a standardized way of expressing logical formulas using only disjunctions (unions) of conjunctions (intersections). In the context of set-theoretic type systems, DNFs provide a canonical representation for union and intersection types, represented respectively as or and and in Elixir.

In Elixir, we would represent those as lists of lists. Consider a type expression like (A and B) or (C and D). This is already in DNF, it’s a union of intersections, and it would be represented as: [[A, B], [C, D]]. This means performing unions between two DNFs is a simple list concatenation:

<code...

Get the full details here: Lazier Binary Decision Diagrams (BDDs) for set-theoretic types - The Elixir programming language