We combine every technique from this series — algebraic types, pattern matching, phantom types, typestate, concepts, compile-time data, parametricity, linear logic, F-algebras — to build a compile-time verified protocol where violations are type errors, not runtime surprises.
~/ 20 posts
A list contains lists. A tree contains trees. How do you define a type in terms of itself? Fixed points, F-algebras, and catamorphisms — the formal machinery behind every fold, every visitor, and every recursive data structure.
Classical logic lets you copy and discard premises freely. Remove those abilities and you get the logic of resources — linear, affine, relevant, ordered. RAII, move semantics, and unique_ptr are fragments of this theory. C++ is a substructural language and doesn't know it.
If a function works for any type and never inspects it, its behavior is constrained by the type signature alone. You get theorems without proofs. This is parametricity — and it explains why phantom types, generic algorithms, and templates are more powerful than they look.
C++20 lets values enter the type system. This is the gateway to dependent types — Pi types, Sigma types, and the calculus of constructions. The compiler becomes a staged computation engine.
Twelve posts of theory. Now we build. A complete, compilable, interactive terminal renderer — style interning, 8-byte cells, cell-level diffing, transition cache, synchronized output, threaded compositor. Copy it. Compile it. Resize your terminal. Watch zero flicker.
C++20 concepts are propositions in intuitionistic logic. Requires-expressions are constructive proofs. Subsumption is modus ponens. This is natural deduction, hiding in your compiler.
States as types. Transitions as functions that consume and produce. Grounded in linear logic — where every resource must be used exactly once — typestate turns protocol violations into compile errors.
The spinner thread and the main thread both want stdout. They can't have it. The Compositor is the bouncer: one lock, one writer, zero corruption. Plus the self-pipe trick, mutable regions, and why the mutex must cover the write() syscall.
A phantom type parameter exists only in the type system — it carries no data, occupies no memory, and vanishes in the binary. Parametricity guarantees it works. Representation independence makes it free.
Pattern matching is the elimination form for algebraic types — the way you take apart what introduction rules put together. Exhaustiveness, nested patterns, guards, refutability, and the deep reason why the compiler insists you handle every case.
Two buffers. Swap every frame. Clear, render, replay, diff, emit, swap. The complete lifecycle of a single frame, from event trigger to terminal update, in ~230 microseconds.
Types form a semiring. Products multiply, sums add, and the distributive law lets you factor types like polynomials. Initial algebras, catamorphisms, and the deep reason why std::visit is the only operation you need.
In 1991, the entire web fit in 8MB. A Hello World app now requires 500MB. We made software 62,500 times larger to do the same thing. If this were any other discipline, there'd be a congressional hearing.
Type judgments, formation rules, Curry-Howard, and the lambda cube — real type theory, made concrete in modern C++. A program is a formal system, and the compiler is its first reviewer.
The terminal can shift rows for you. You just have to ask nicely with CSI sequences, and then lie to your own diff engine about what the previous frame looked like. Result: 99% reduction in scroll I/O.
Stack Overflow serves 1.3 billion page views a month with 9 web servers. WhatsApp hit 450M users with 32 engineers. You have 500 users and three Kubernetes clusters.
The single highest-leverage optimization in the entire pipeline. Computing the minimal ANSI to go from style A to style B, caching it forever, and never computing it again. 30-50% reduction in terminal output with one hash map.
Your ORM is quietly sending 247 database queries to render one page. It smiled warmly while loading your entire database into memory one row at a time, like a golden retriever fetching every stick in the park.
The heart of the renderer: compare two screen buffers cell by cell, emit the minimal ANSI to transform one into the other. Every optimization upstream exists to make this loop faster. Every optimization here directly reduces bytes to stdout.