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.
Posts tagged “c++20” (19)
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.
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.
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.
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.
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.
How Loom loads blog content from the local filesystem or a remote git repository using the same interface, parses frontmatter and config without dependencies, extracts image dimensions from raw PNG and JPEG bytes, and derives metadata from git history.
How Loom serves HTTP with a single-threaded epoll event loop, zero-copy request parsing via string_view, pre-serialized wire responses, and a dual write path that avoids allocations on the hot path.
How Loom encodes routes as non-type template parameters, analyzes patterns at compile time, and generates an optimal dispatch chain with zero runtime overhead.
How Loom pre-renders every page into 6 HTTP wire variants, serves them with zero copies and zero allocations, and keeps responses under a millisecond.
A hand-written markdown-to-HTML converter in 1200 lines of C++. Two passes, zero dependencies, custom extensions, and sub-millisecond performance.
How Loom compiles typed theme definitions into CSS using pointer-to-member bindings, fold expressions, structural emitters, a full CSS DSL, and component overrides.
How Loom turns HTML generation into composable C++ expressions with a fold-based DOM builder, control flow primitives, and a JSX-like component system with theme-overridable slots.
How Loom uses phantom type tags, conditional concepts, structural enums, and token types to turn entire categories of bugs into compile errors.