LetItCrash

The role of types in programming, and why this site teaches Elixir

LLM-authored, human-reviewed

Foundations

If you’ve spent time in programming communities, you’ve seen the type debate. One person says static types catch bugs; another says they’re ceremony that gets in the way. They’re talking past each other because “strong typing” and “weak typing” aren’t one axis. They’re several axes mashed together, and the conversation treats them as one.

This article separates them. It draws on the type-systems literature and on the choices made by TypeScript, Elixir, Erlang, Gleam, Haskell, and PureScript. It ends with why this site teaches the dynamically-typed one of those and not the typed BEAM cousin.

The first mistake: “static” and “strong” are different questions

The most common error in the type debate is conflating two independent axes. Benjamin Pierce’s Types and Programming Languages, the standard graduate text, effectively says to drop the words “strong” and “weak” altogether because they have no agreed technical definition. The argument actually contains two separate questions.

Static vs. dynamic asks when the check runs. A static type system reasons about the program’s text before it runs; a dynamic system checks at run time, at the moment an operation is about to be applied to a value. TypeScript, Haskell, Java, and Gleam check statically. JavaScript, Python, Elixir, and Erlang check dynamically (though Elixir has recently added a static layer on top, which is a story we’ll get to).

Strong vs. weak asks how much implicit coercion the system tolerates. A weak system silently reinterprets values of one type as another to make an operation succeed; a strong system refuses and raises an error. JavaScript sits at the extreme weak end, and every JavaScript developer has paid for it:

"5" + 3        // "53"   - number coerced to string
"5" - 3        // 2      - string coerced to number
[] + {}        // "[object Object]"
null == undefined  // true

Each of those “works.” The runtime reinterpreted the operands instead of reporting a type error. C sits at the weak end too - it lets you cast a float’s bytes to an int and read garbage:

float f = 3.14f;
int *p = (int *)&f;   // legal: reinterpret the bits
printf("%d\n", *p);   // prints 1078523331, not 3

Now cross the two axes and you get four quadrants. The surprises are the off-diagonal ones:

Static checking Dynamic checking
Strong (little coercion) Haskell, OCaml, Gleam, Java Python, Ruby, Elixir, Erlang
Weak (coercion tolerated) C, C++ JavaScript, PHP

The off-diagonal cells expose the mistake. C is statically checked and weak: every type is known at compile time, yet casts and pointer arithmetic let you reinterpret representations freely - so “statically typed” does not buy safety. Python is dynamically checked and strong: types are only known at run time, but "5" + 3 raises TypeError rather than silently producing "53". JavaScript is the unusual occupant of the weak+dynamic corner: checked late, and permissive even then. This is the hole TypeScript was built to fill.

So the next time someone asks “is Python strongly typed?” and a fight breaks out, check which axis each person means. One is pointing at Python’s refusal to coerce (strong axis); the other at Python’s refusal to check before run time (dynamic axis). Both are correct. They’re answering different questions.

The three dials that actually matter

Separate the axes and a subtler fact appears: two type systems in the same quadrant can make radically different promises. TypeScript and Haskell are both static, but they do not promise the same thing. The binary “strong vs. soft” dissolves into three independent dials, and every real system is a point in this three-dimensional space.

Dial 1: Soundness (does the checker ever lie?)

A type system is sound when its verdicts can be trusted: if it assigns a program a type, the program will not produce a value outside that type at run time. Soundness is a theorem about the system. Here is the fact that surprises most TypeScript developers: soundness is an official TypeScript Design Non-Goal. The design goals document states the project will not “apply a sound or ‘provably correct’ type system,” but will instead “strike a balance between correctness and productivity.”

The consequence is practical. TypeScript treats mutable arrays as covariant, so this type-checks - even in strict mode - and crashes at run time:

const names: string[] = ["a", "b"];
const items: (string | number)[] = names;  // allowed: covariance
items.push(42);                             // allowed
const first: string = names[2];             // type says string; value is 42

The checker lied. It certified first as a string that is in fact a number. Haskell’s and Gleam’s checkers do not lie in this way. That’s the first dial turned all the way up.

Dial 2: Coverage (what fraction of the program is checked?)

The second dial is coverage: how much of the program is inside the checked region? A fully covered system checks every expression; a partial-coverage system checks only what you annotate and treats the rest as dynamically typed. This is what “gradual typing” means.

Coverage is independent of soundness, and that distinction matters. TypeScript-with-any is unsound and partial. Elixir’s new gradual system is sound-by-design but partial, using a dynamic() type to fence off regions the inference can’t see through yet. Haskell is sound and (modulo explicit escape hatches) total. Two systems with identical soundness can still feel completely different because their coverage dials sit at different settings: “the compiler checks everything I write” versus “the compiler checks the files I opted in.”

Dial 3: Error philosophy (no false positives vs. no false negatives)

The third dial is the least known outside the BEAM, and it matters most when you compare Erlang and Elixir. When the checker can’t decide whether code is correct, which way does it err?

A no-false-positives system never warns unless it can prove the program is wrong. It will silently miss real bugs, but every warning it does emit is genuine. Erlang’s Dialyzer lives here: every Dialyzer warning is a real discrepancy, but a clean Dialyzer run proves nothing.

A no-false-negatives system never misses a provable bug. It will sometimes warn about code that is actually fine, but it won’t let a real bug through silently. Elixir’s new type system occupies this pole: it warns on “verified bugs” - typing violations guaranteed to fail at runtime if executed.

TypeScript’s answer is a third position: tolerate both. Unsoundness means some real bugs are unreported (false negatives), while strictness checks produce warnings on code that will run fine (false positives). There’s no theorem on either side, which is exactly what “soundness is a non-goal” purchases.

The strong end: Hindley–Milner and its descendants

Walk to the strong end of the spectrum: the Hindley–Milner (HM) family, where the compiler - not the programmer - computes the type of every expression, and the type it computes is provably the most general one possible. If you’re coming from TypeScript, where inference is a convenience layered over annotations, HM is a different species: inference is the defining feature, annotations are optional.

The theoretical core was proved in a six-page paper at POPL 1982: Luis Damas and Robin Milner’s “Principal type-schemes for functional programs.” The result has three parts. Soundness: every type the algorithm reports is a valid type. Completeness: every typable program gets an answer. Principality: the algorithm infers principal types, where a principal type subsumes all other types assignable to the same program. Write the identity function and HM doesn’t guess Int -> Int or String -> String; it derives a -> a, the single most general answer from which every concrete instance follows.

The practical consequence is what makes this family feel alien to a TypeScript developer: HM can deduce the most general type of a given program without any annotations from the programmer. It does so in almost linear time with respect to the size of the source.

Why full inference needs immutability, no subtyping, no null

This is where the “why don’t all languages have this” question gets its answer. Three common language features - mutation, subtyping, and nullable references - each attack a load-bearing assumption of HM. The languages with the strongest inference all restrict or forbid them.

Mutation breaks generalization. If let r = ref None were generalized to “a reference holding any optional type,” one caller could store a String and another could read an Int, and soundness collapses. The ML family’s fix is the value restriction: only immutable values get the most general type. F#’s documentation states the rule plainly: automatic generalization applies “only on complete function definitions that have explicit arguments, and on simple immutable values.”

Subtyping attacks unification, the engine of the algorithm. HM solves type constraints by finding substitutions that make two type expressions equal. Subtyping replaces equality with an inequality relation, and the clean most-general answer disappears. TypeScript is the working demonstration: it runs over JavaScript’s mutable, structural, subtyped object model, so full inference is impossible.

Null acts as a hidden subtype of everything. A null that inhabits every type breaks the “if it type-checks, the shape is guaranteed” contract. It is not a coincidence that the HM languages banish null outright.

Put those together and a pattern emerges that’s easy to misread as fashion. The languages with full inference - Haskell, OCaml, Standard ML, F#, PureScript, Gleam - are all functional-first, and the reason is structural, not cultural. HM inference requires the language to be about functions and immutable values. A language built on mutable objects, inheritance, and null references - JavaScript’s object model - simply has no ledge for the algorithm to stand on. When you choose a language, you choose its semantics; the type system’s ceiling follows from that choice.

The family portrait

The HM family makes this concrete. Two members compile to the same VM Elixir does, and one is the subject of the Gleam color note at the end of this article.

Haskell is the research flagship: HM at the core, then decades of extensions. Laziness (non-strict evaluation) is its defining non-type feature. Type classes provide ad-hoc polymorphism. Inference is full and annotations are optional, though the industrial norm is a signature on every top-level binding - inference computes types, signatures pin them.

PureScript is Haskell’s semantics compiled to JavaScript, with one deliberate deviation: it’s strict, not lazy. It carries full HM inference, algebraic data types, type classes, and enforced purity (side effects live in an Effect type that’s visible in the signature) into the JS ecosystem. The contrast with TypeScript is instructive: both compile to JS, but PureScript changes the source language’s semantics (immutability, no null, no subtyping) and is rewarded with sound, global inference. TypeScript preserves JS semantics and accepts local inference and deliberate unsoundness. The JS runtime can host the strong end of the spectrum; the JS object model cannot.

Gleam is full HM inference on the BEAM - the same VM Erlang and Elixir run on. Its creator’s announcement describes a type system with “full type inference without annotations, generics, flexible and ad-hoc records using row types, first class modules, ADT style enums, and no null/nil/undefined or subtyping.” Every item on the inferability checklist is present.

// No annotations required; the compiler infers everything.
pub type Shape {
  Circle(radius: Float)
  Rect(width: Float, height: Float)
}

pub fn area(shape) {           // inferred: Shape -> Float
  case shape {
    Circle(r) -> 3.14159 *. r *. r
    Rect(w, h) -> w *. h
  }
}

The interesting design decision is what Gleam refuses. Type classes are “not planned,” because they “can make it easy to make challenging to understand code, tend to have confusing error messages, make consuming the code from other languages much harder, have a high compile time cost.” The result is a language that keeps the strongest inference in the family while deliberately shrinking the abstraction surface.

Language Inference core Abstraction over types Null Subtyping
Haskell Full HM Type classes No No
OCaml Full HM Modules, functors No No
PureScript Full HM Type classes, instance chains No No
Gleam Full HM None (no classes planned) No No

Read the table row by row. The pattern is visible in miniature. The rows with full HM inference and no asterisks are precisely the rows with no null and no subtyping. The strength is not free; the family differs mainly in where it chooses to spend.

The softer end: gradual, success-typed, and optional systems

Not every type system tries to prove your program correct. A large family occupies a softer middle ground: it checks what it can, stays silent where it can’t, and treats adoption by working programmers as a first-class design constraint.

TypeScript: deliberately unsound, massively adopted

TypeScript is the most widely used statically-checked language in the JavaScript ecosystem, and it is also, by its own documentation, not a sound one. The design rationale is economic. A sound static system for JavaScript would have to reject idioms that real codebases depend on, which would destroy TypeScript’s core value proposition: any valid JavaScript program is already a valid TypeScript program, and strictness is an opt-in ratchet rather than an entry fee.

The three escape hatches every TS developer should be able to name:

  • any: a value typed any is assignable to and from everything. It doesn’t narrow or propagate information; it discards it.
  • Type assertions: ("23" as any) as number compiles fine and crashes later.
  • Covariant mutable arrays: a string[] is assignable to (string | number)[], so pushing a number through the wider alias is accepted - even in strict mode.

None of this makes the checker useless - it catches large classes of errors and underpins the tooling that drove its adoption. It means the guarantees are probabilistic rather than logical. The compiler’s silence does not mean the code is safe; it means the code is consistent with annotations the compiler chose to trust.

The BEAM’s two answers: Dialyzer, then Elixir’s set-theoretic types

The BEAM has hosted static analysis for two decades but never a conventional sound type checker in the compiler - until recently. The history is best read as two successive bargains.

Dialyzer’s “no false positives” bargain. Dialyzer is built on success typings, and its documentation states the bargain plainly: “ensuring sound warnings without false positives.” Every warning Dialyzer emits corresponds to a real discrepancy, but the absence of warnings guarantees nothing. For a developer, fix a Dialyzer warning immediately; it’s almost certainly a real bug. A clean Dialyzer run is weak evidence of correctness.

The design intent came from deploying the analysis on Ericsson’s AXD301 ATM switch codebase, where the authors concluded that false alarms destroy adoption of static analysis in an industrial setting. This is not academic taste - it’s hard-won experience from telephone switches that needed to run for years.

Elixir’s “no false negatives” bargain. Elixir’s type system, designed by Giuseppe Castagna, Guillaume Duboc, and José Valim, is the most theoretically ambitious soft system in production use. Set-theoretic means union, intersection, and negation types are first-class - integer() and not 0 is a type. Semantic subtyping means subtyping is decided by set inclusion of what values the types actually denote, not by syntactic rules, which is exactly what pattern matching and guards need.

The system shipped in stages. By Elixir v1.20, every Elixir program is gradually type-checked, and the headline framing is the pole opposite Dialyzer’s: “verified bugs” - typing violations guaranteed to fail at runtime if executed, at an “extremely low false positives rate.” The central mechanism is dynamic(), which is explicitly not TypeScript’s any. Where any means “anything goes,” dynamic() works as a range that narrows as the value flows through the program.

# Inference alone can flag this - no annotations needed:
def downcase_name(%{name: name}) when is_binary(name) do
  String.downcase(name)
end

def downcase_name(user) do
  String.downcase(user.name)
  # warning: user.name may not be a binary - verified bug
end

For a TypeScript developer, the disorienting part is that Elixir’s checker can know your code is wrong more precisely than tsc does, despite the language being dynamically typed at runtime. The reason is structural: immutable data, first-class functions, and pattern matching are inferable, and set-theoretic union and negation types let the compiler model the dynamic idioms ({:ok, _} | {:error, _} tagged tuples) that HM-style systems struggle to express.

The retrofit pattern

The same retrofit pattern repeats across mainstream dynamic languages, driven by codebase scale rather than language theory: mypy for Python (Dropbox reached four million annotated lines), Sorbet for Ruby (Stripe, fifteen million lines), Hack for PHP (Facebook). Every retrofit checker chose erasure plus an information-discarding escape type, because inserting runtime checks into a VM that wasn’t designed for them is expensive. Elixir is the outlier because the BEAM was designed with pervasive runtime type tests; its checker exploits checks that already exist.

What the evidence actually shows

Advocacy for strong typing is easy to find; measurement is not. Set aside the essays and examine the small body of quantitative work. The verdict should disappoint both camps: the effect of static types on defects is real, modest, and confounded. All three, at once.

Real: A peer-reviewed ICSE 2017 study (Gao, Bird, Barr) took 400 fixed public JavaScript bugs, annotated them, and ran TypeScript and Flow over the pre-fix code. Both checkers detected 15% - and the authors called this conservative, since it counts only bugs that survived review.

Modest: 15% is not 80%. José Valim is right to call “a static type system would catch 80% of my bugs” an unrealistic claim; nothing in the literature supports numbers like that. The largest cross-language GitHub study (Ray et al., FSE 2014) found language effects “significant, but modest” and “overwhelmingly dominated by process factors such as project size, team size, and commit size.”

Confounded: A 2019 reproduction (Berger et al., TOPLAS) re-derived the largest study’s results and found that most language-level associations did not survive - “only four languages are found to have a statistically significant association with defects, and even for those the effect size is exceedingly small.” Some of the original study’s “TypeScript projects” were actually C++ projects. Controlled experiments with human subjects (Hanenberg, OOPSLA 2010) found static typing helped on some tasks and hurt on others.

The honest synthesis is simple: anyone quoting a single study as settling the question is doing advocacy, not reading. The defect-reduction evidence is weak-to-moderate. But the industry’s actual reasons for adopting types aren’t primarily about bug counts.

What the industry actually votes for: the economics of change

Whatever the laboratory evidence says, the market has voted, and it voted once. Every major dynamically-typed language has added static or gradual typing, and none has removed it. The migration record is the strongest behavioral evidence available:

Company From → To Scale Stated motivation
Facebook PHP → Hack nearly entire codebase “fast development cycle of PHP with the discipline of static typing”
Dropbox Python → Python + mypy ~4 million lines dynamic typing “made code needlessly hard to understand”
Stripe Ruby → Ruby + Sorbet 15M+ lines engineers “scared to make sweeping changes”

The table’s most important row is the one that doesn’t exist: the reverse migration. There is no comparably documented case of a large organization removing static types to return to dynamic typing. State this carefully as absence-of-evidence - nobody writes the triumphant blog post “we deleted our type annotations” - but the asymmetry is striking, because the costs of these migrations were immense. Dropbox funded the mypy core team. Stripe built an entire type checker in-house. Facebook built a language. Firms do not spend millions of engineer-hours on fashion.

The consistent stated motivations - comprehension, refactoring confidence, onboarding - point at the real benefit: strong static types change the economics of change. Refactors become compiler-guided instead of fear-guided. Change an algebraic data type by adding a variant, and the compiler enumerates every case/match site that must be updated, with exhaustiveness checking guaranteeing nothing was overlooked. This is what the community shorthand “if it compiles, it works” gestures at - a slogan its own community treats as aspirational, not absolute.

The skeptics, taken seriously

The debate is not one-sided, and the strongest skeptical voices come from inside traditions this site is adjacent to.

Robert C. Martin (“Uncle Bob”) makes the categorical argument: “Types do not specify behavior. Types are constraints placed, by the programmer, upon the textual elements of the program.” A compiler accepts a well-typed function that sorts descending when you needed ascending. Types check shape, not behavior - the discipline that actually prevents defects remains test-driven development, in any language.

Dan Luu’s literature review is the canonical methodological critique. Study by study, he finds the classic results small, confounded, or mutually contradictory. His bottom line: “the measured differences between type systems are far smaller than the difference between subjects’ programming abilities.”

Rich Hickey’s “Maybe Not” (Clojure/conj 2018) makes the evolution argument. His target is Maybe/Either option types, and his claim is that they make compatible changes breaking: strengthening a return type from Maybe Y to Y - strictly more useful - breaks every caller that pattern-matched on the wrapper. The type couples all call sites to today’s level of certainty. His constructive position is that verification should survive change, not freeze it.

The BEAM tradition. Joe Armstrong’s design philosophy - formalized in his 2003 PhD thesis - assumes errors will happen at runtime regardless of language discipline, and puts the engineering weight on detection, isolation, and restart: lightweight processes, supervision trees, “let it crash.” A compile-time proof that arguments are well-typed says nothing about the failures that take down telecom systems - deadlocks, hardware faults, corrupt network messages, races under load. Recalling the 1997 attempt by Phil Wadler and Simon Marlow to type Erlang, Armstrong wrote: “only a subset of the language was type-checkable, the major omission being the lack of process types and of type checking inter-process messages.” The parts of Erlang that matter most - processes and messages, exactly where supervision earns its keep - were the parts the type system could not see.

The apparent contradictions dissolve on inspection. The advocates and skeptics are guarding against different failure modes. Minsky’s “make illegal states unrepresentable” guards against maintenance-time failure. Hickey’s “Maybe Not” guards against evolution-time failure. The BEAM tradition guards against runtime failure. José Valim guarded against expression-time failure - type systems that reject valid dynamic idioms - until set-theoretic types let him stop rejecting them.

If the debate were about a measurable fact, thirty years of production experience would have settled it. It hasn’t, because the disagreement is about which failure hurts most in your domain - a values question wearing a facts costume.

Why this site teaches Elixir, not Gleam

This site’s job is to teach Elixir. Elixir is dynamically typed (with a new gradual static layer), and this is not a compromise the site is making despite itself - it’s the point.

Here is the color note. We originally had Gleam - full Hindley–Milner inference on the BEAM, the typed cousin in the family portrait above - as a language on this platform. It was a technical nightmare to execute. Gleam compiles to Erlang source, and our execution model is built around Elixir’s runtime semantics, hot code loading, and the specific shape of BEAM process messaging that Elixir’s standard library assumes. Running learner-authored Gleam code in a sandbox alongside our existing runners required a toolchain integration that fought us at every boundary. Gleam is part of the BEAM ecosystem in the same sense that Elixir is - they share the VM - but “shares the VM” does not mean “shares the execution harness,” and the harness is where the cost lived.

We are considering eventually adding PureScript, which has an Erlang backend (purerl) and at least one long-running production deployment in live media streaming. PureScript’s learning curve is, by its own creator’s and core contributors’ accounts, among the steepest of any language in this space - its creator Phil Freeman advised learning Haskell first as a prerequisite, and a core contributor told a prospective adopter on the official forum that “this was the hardest language for me to learn.” The concept ladder before hello-world is real: in PureScript, the first console.log equivalent already requires understanding why a function returns Effect Unit instead of performing its side effect directly. That is a serious teaching challenge, and not one to take on until the Elixir path is complete.

But the main point stands: this site’s goal is to teach Elixir. Elixir is not a worse Gleam or a dynamically-typed Haskell. It is a deliberate answer to a different question - what does a language look like when it optimizes for runtime resilience, hot code loading, and supervision rather than compile-time proof? The answer is a language where the supervision tree is the primary safety artifact, where type machinery is layered on a runtime that already assumes failure, and where the new set-theoretic type system delivers contracts at function boundaries without paying the costs the skeptics correctly identified.

The type debate’s three dials - soundness, coverage, error philosophy - are real, and understanding them makes you a better programmer in any language. You’ll write TypeScript with a clearer eye for where any is a coverage hole you chose. You’ll read Elixir’s new type warnings knowing they’re “verified bugs,” not guesses. You’ll understand why Gleam can infer everything and why that luxury is bought with semantic restrictions. But when you sit down to practice on this site, you’re practicing Elixir - because Elixir’s bet, that runtime malleability and supervision are worth keeping even where they cost static certainty, is the bet this site is built to teach you to work within.

Where to go next

Related exercises

← Back to articles

Exercises