⟨⟩ Eubeamgua

← History

Dynamic vs Static Typing on the BEAM

The BEAM was born dynamically typed - so how do Erlang's Dialyzer, Elixir's new gradual set-theoretic types, and Gleam's sound static system each catch type errors, and what does each one promise (or refuse to promise)?

ErlangElixirGleam

The Erlang virtual machine - the BEAM - grew up dynamically typed. A value carries its type with it at runtime, functions accept whatever term you hand them, and the "let it crash" philosophy treats a type mismatch as just another fault for a supervisor to recover from. Erlang, Elixir, and the Lisp-flavoured LFE all live in this world; Luerl inherits Lua's dynamic typing too. Gleam is the outlier - a sound, statically typed language on the same VM.

But "dynamic vs static" on the BEAM is more interesting than a binary. Erlang ships Dialyzer, a static analyzer built on success typings. Elixir is rolling out a gradual set-theoretic type system baked into the compiler. And Gleam offers full sound static typing with inference. Each makes a different bargain about what it will catch, what it will miss, and what it asks of you. This article walks the spectrum.

What "dynamically typed" actually means here

A common confusion: dynamic typing is not weak typing. The BEAM is dynamically and strongly typed. Types are checked - rigorously - but at runtime, and the VM never silently coerces an integer into a string the way a weakly typed language might.

%% Erlang: types are checked at runtime, and checked strictly.
1 + 1.            %% => 2
1 + "1".          %% ** exception error: an arithmetic expression error (no silent coercion)
list_to_integer("oops").  %% ** exception error: badarg

# Elixir: same VM, same strong-but-dynamic semantics.
1 + 1            # => 2
1 + "1"          # ** (ArithmeticError) bad argument in arithmetic expression
String.upcase(:not_a_string)  # ** (FunctionClauseError)

Nothing about the value's type is in doubt at runtime; what's in doubt is whether a given call site will ever be reached with a term of the wrong shape. Dynamic typing defers that question to execution. Static typing answers it before the program runs. Everything below is about who answers, and when.

Erlang and Elixir: dynamic by birth

Both languages lean on the same trio that makes dynamic typing livable on the BEAM: pattern matching, tagged tuples, and supervision. The convention for "a result that might fail" is a tagged tuple the caller pattern-matches:

%% Erlang: {ok, V} | {error, Reason} is a convention, not a checked type.
read_config(Path) ->
    case file:read_file(Path) of
        {ok, Bin}       -> {ok, parse(Bin)};
        {error, Reason} -> {error, Reason}
    end.

# Elixir: the same idiom in friendlier dress - still convention-driven.
def read_config(path) do
  case File.read(path) do
    {:ok, bin}      -> {:ok, parse(bin)}
    {:error, reason} -> {:error, reason}
  end
end

Nothing in either language forces a caller to handle both branches, nor stops a typo'd atom ({:eror, reason}) from slipping through to fail far away. The dynamic bargain is: you trade compile-time guarantees for flexibility, fast iteration, trivial metaprogramming, and hot code loading - and you buy back reliability at runtime with supervisors that restart a crashed process into a known-good state. For a quarter-century of telecom-grade uptime, that bargain held. But teams kept wanting the compiler to catch shape errors earlier. Two very different answers emerged.

Erlang's answer: Dialyzer and success typings

Dialyzer - the DIscrepancy AnaLYZer for ERlang - is a static analysis tool that ships with OTP. You can point it at compiled BEAM files or source and it reports "discrepancies": definite type errors, unreachable clauses, redundant guards, and broken contracts. Crucially, it was designed to be adopted into existing multi-million-line codebases without anyone first annotating them, so it makes an unusual promise.

Dialyzer is built on success typings. Where a traditional type checker tries to prove a program cannot go wrong (and rejects anything it can't prove safe), a success typing works the other way: it infers, for each function, the most permissive type that describes every way the function could possibly succeed. Dialyzer then warns only when it can prove that two such typings can never overlap - that a call is guaranteed to fail at runtime if reached.

The consequence is a deliberate, signature design choice:

That asymmetry - "sound warnings, incomplete coverage" - is the whole point. It means a clean Dialyzer run is cheap to trust and never cries wolf, at the cost of being a safety net with real holes.

You sharpen Dialyzer by writing optional -spec contracts. These are documentation the tool actually checks:

-module(bank).
-export([withdraw/2]).

%% A type spec: developer-declared input and output types.
-spec withdraw(Balance :: non_neg_integer(),
               Amount  :: pos_integer()) ->
                  {ok, non_neg_integer()} | {error, insufficient_funds}.
withdraw(Balance, Amount) when Amount =< Balance ->
    {ok, Balance - Amount};
withdraw(_Balance, _Amount) ->
    {error, insufficient_funds}.

Dialyzer compares your -spec against the success typing it inferred from the code. If they conflict, you get a warning. Two named relationships matter:

A spec that contradicts the code - say, claiming withdraw/2 can return {ok, atom()} - is flagged outright. Custom types compose, so specs can be quite expressive:

-type account()  :: #{id := binary(), balance := non_neg_integer()}.
-type tx_error() :: insufficient_funds | account_frozen.

-spec transfer(account(), account(), pos_integer()) ->
                  {ok, account(), account()} | {error, tx_error()}.

Elixir exposes the very same machinery through @spec/@type and the dialyxir wrapper, because under the hood it is the same Dialyzer running over BEAM bytecode:

@type account :: %{id: binary(), balance: non_neg_integer()}

@spec withdraw(non_neg_integer(), pos_integer()) ::
        {:ok, non_neg_integer()} | {:error, :insufficient_funds}
def withdraw(balance, amount) when amount <= balance,
  do: {:ok, balance - amount}

def withdraw(_balance, _amount),
  do: {:error, :insufficient_funds}

Dialyzer is genuinely valuable - it catches dead clauses, impossible matches, and contract violations across module boundaries - but it is opt-in, runs as a separate (often slow) pass, and by construction will never catch every shape error. That gap is exactly what Elixir's newer effort, and Gleam, set out to close from opposite directions.

Elixir's answer: gradual set-theoretic types in the compiler

Rather than bolt analysis on the side, Elixir is growing a type system inside the compiler, so type checking happens on every mix compile with no extra tool. The theory was published in an award-winning 2023 paper (Castagna, Duboc, and Valim), and the implementation has shipped incrementally ever since.

It is a set-theoretic system: types are built and combined with the basic set operations - unions, intersections, and negations. integer() or atom() is a union; dynamic() and integer() is an intersection. This algebra lets the checker describe Erlang/Elixir's wonderfully heterogeneous values (an atom or a tuple or a map of a specific shape) far more naturally than a classic ML system can.

It is also gradual, anchored by a special dynamic() type. dynamic() is not a hole that disables checking like any() in many gradual systems; it is checked optimistically and narrowed as a value is used. Code with no type information is treated as dynamic(), so existing programs keep compiling, while the checker still reports a violation the moment it can prove the supplied and expected types are disjoint - provably non-overlapping.

That disjointness rule is what gives the system its extremely low false-positive rate: it only flags things guaranteed to fail. The milestone-by-milestone rollout, in this environment's timeline:

The headline is that this is all inference-driven. You write ordinary Elixir; the compiler reconstructs types from your patterns and guards and reports two kinds of finding: dead code (clauses that can never match) and verified bugs (typing violations guaranteed to crash at runtime if reached).

def describe(value) when is_integer(value) do
  # Inside this clause the compiler has narrowed `value` to integer().
  # Calling a String function on it is a *provable* mismatch:
  String.upcase(value)
  #             ^^^^^ warning: expected a binary, got integer()
end

def classify(:ok), do: "fine"
def classify(:error), do: "broken"
# A guard the compiler can prove is unreachable given the clauses above:
def classify(x) when is_integer(x) and is_binary(x) do
  # warning: this clause can never match - integer() and binary()
  # are disjoint, so the intersection is the empty type (none()).
  "impossible"
end

Because it is inference-first, the system finds bugs in code that predates it without anyone editing a line. The roadmap (toward v1.21 and beyond) tackles the harder pieces needed before user-written type signatures arrive: recursive types, parametric types, and typed structs. For now Elixir occupies a genuinely distinct point on the spectrum - stronger than Dialyzer (built in, always on, no setup) and yet softer than Gleam (gradual, annotation-free, and forgiving wherever a type is genuinely unknown).

Gleam's answer: sound static typing, no escape hatches

Gleam (stable v1.0 on 4 March 2024, by Louis Pilfold) takes the opposite stance from everything above: it is statically typed by default, sound, and fully inferred, descending from the Hindley-Milner lineage of ML, OCaml, and Elm. There is no dynamic(), no any, no unchecked cast. If Gleam cannot prove your program type-correct, it will not compile - the inverse of Dialyzer's "warn only when provably wrong."

The same fallible-result idiom that is a convention in Erlang/Elixir is an enforced type in Gleam:

import gleam/int

pub fn withdraw(balance: Int, amount: Int) -> Result(Int, String) {
  case balance >= amount {
    True  -> Ok(balance - amount)
    False -> Error("insufficient funds")
  }
}

pub fn run() -> String {
  // The compiler forces you to handle BOTH outcomes - you cannot
  // forget the Error branch, and you cannot mistype the tag.
  case withdraw(100, 30) {
    Ok(remaining) -> "left: " <> int.to_string(remaining)
    Error(reason) -> "failed: " <> reason
  }
}

Two words define Gleam's bargain:

import gleam/list

// No annotations - the compiler infers fn(List(Int)) -> List(Int).
pub fn double_all(numbers) {
  list.map(numbers, fn(n) { n * 2 })
}

Gleam also makes case exhaustiveness mandatory, so absence and new variants can't be forgotten - add a constructor to a type and every unhandled case becomes a compile error pointing you at the work. And it removes whole bug classes by construction: no null (absence is the explicit Option type), and no exceptions for expected failure (recoverable errors are Result values). Compare the contract from the top of this article, now with the absent case forced into the open:

import gleam/option.{type Option, None, Some}

pub fn first_even(numbers: List(Int)) -> Option(Int) {
  case numbers {
    [] -> None
    [n, ..] if n % 2 == 0 -> Some(n)
    [_, ..rest] -> first_even(rest)
  }
}
// Every caller must acknowledge the None case - there is no
// "just dereference it and hope," because there is no null.

The price of soundness is rigidity: there is no dynamic() to lean on when you genuinely don't know a type, and crossing into untyped BEAM code requires a deliberate, typed FFI declaration with @external that you vouch for. That trade - give up flexibility, gain a guarantee - is precisely the one the dynamic languages declined, and it is why Gleam feels like a different philosophy rather than a different syntax.

The other two: LFE and Luerl stay dynamic

For completeness, the family's remaining members sit firmly at the dynamic end. LFE (Lisp Flavoured Erlang) uses Erlang's exact data types and runtime, so it is dynamically and strongly typed just like Erlang - and it can use Dialyzer and -spec-style contracts through the same OTP machinery, since it compiles to the same Core Erlang. Luerl runs Lua 5.x inside the BEAM and inherits Lua's dynamic typing wholesale; types live on values at runtime, with no static checking layer at all.

;; LFE: dynamic and strongly typed, Erlang terms as S-expressions.
(defun withdraw
  ((balance amount) (when (=< amount balance))
   (tuple 'ok (- balance amount)))
  ((_balance _amount)
   (tuple 'error 'insufficient-funds)))

-- Luerl runs this Lua on the BEAM: dynamic typing, runtime checks only.
local function withdraw(balance, amount)
  if amount <= balance then
    return balance - amount        -- a number
  else
    return nil, "insufficient funds" -- nil + message, Lua's idiom
  end
end

The spectrum at a glance

The BEAM family now spans the full range from "no static checking" to "sound static checking," with two genuinely novel midpoints:

erlang elixir gleam lfe luerl
Runtime typing dynamic, strong dynamic, strong static, strong dynamic, strong dynamic, strong
Static checker Dialyzer (opt-in) built-in, always on compiler (mandatory) Dialyzer (opt-in) none
Foundation success typings gradual set-theoretic Hindley-Milner success typings n/a
Sound type system? no (unsound by design) gradual (sound where typed) yes, fully sound no no
False positives none (sound warnings) extremely low n/a (compile errors) none n/a
Annotations optional -spec none required (yet) optional (inferred) optional -spec none
Null / absence undefined, atoms nil none - Option atoms nil

A few honest caveats. "Sound" is doing double duty in that table: Dialyzer's warnings are sound (it never cries wolf), but as a type system it is unsound (it misses real errors) - the opposite axis from Gleam, whose type system is sound (it rejects all type-incorrect programs) at the cost of rejecting some correct-but-unprovable ones. Elixir's effort is the moving target: annotation-free inference today, user-written signatures and typed structs on the roadmap.

Choosing a point on the spectrum

There is no single "right" answer, which is rather the point of a multi-language VM:

The remarkable thing is that all five interoperate on one runtime. You can wrap a battle-tested Erlang library behind a sound Gleam interface, call it from Elixir whose compiler quietly type-checks the surrounding code, and supervise the whole thing with the same OTP tree - choosing, function by function, exactly how much the compiler should prove for you.

Further reading