The Unreasonable Effectiveness of Constructive Data Modeling

TL;DR: By treating types as positive space that constructs new values rather than negative space that restricts existing ones, and by making proper use of product types and sum types, we can precisely model data invariants without complex type system features, thus avoiding fights with the type checker. ## From the Dark Ages of Static Typing to a Renaissance The speaker originally worked on the Haskell compiler and later developed care software for nursing homes using Scala at August Health. The software involves medication management, where errors can have serious consequences, so the team placed great emphasis on correctness, extensively using tests and static typing. In the early days of static typing, mainstream languages were Java and C++. Java was conservative, restrictive, and tightly coupled with object orientation; C++ was complex and not safety-focused. This led many programmers to consider static typing outdated, embracing dynamic languages like JavaScript and Ruby. In recent years, Rust and TypeScript have brought about a renaissance of static typing—Rust emphasizes safety, and TypeScript adds types to JavaScript. All of this has made static typing "cool" again. ## The Dilemma of Type System Complexity However, the speaker is not satisfied with the current state. Type system complexity is growing too fast; most TypeScript programmers don't understand how it works and often "fight" with the type checker. Java is frustrating because it is too restrictive, and TypeScript is frustrating because it is too complex. Many think they need fancy features (like dependent types) to solve problems. But the speaker believes that by shifting perspectives and using simple product types and sum types, invariants can be effectively captured, and this works in most languages that support these features. ## Core Idea: Types Are Construction, Not Restriction ### Negative Space vs. Positive Space People usually think of types as restrictions: draw small circles in the `unknown` universe, excluding unwanted values. But Java's class definition not only restricts existing values but also introduces a new class of runtime values (e.g., `Point` structs). Therefore, types can be seen as constructing positive space from nothing. Take natural numbers as an example: if you want to represent non-negative integers only using signed integers, you would want to restrict the value set, but refinement types are hard to implement. If you first define an unsigned integer type (positive space) that contains only the desired values, then extending upward is simple. ### Non-empty List and Even-length List - **Non-empty list**: consists of "one element" and "zero or more elements". Represent it using a tuple, no complex type features needed. - **List with an even number of elements**: elements come in pairs, can be represented as a `list of pairs`. Although operations on the list need adaptation, as long as the representation and interpretation of data are decoupled, flexible modeling is possible. ### User Example: At Least One of Email or Phone Suppose there is a user struct in a database containing email and phone fields, at least one must be set. One might think dependent types are needed (the type of "email" depends on the value of "phone"). But by introducing an additional enum type that explicitly lists all possible states, the problem is solved: ``plaintext type ContactMethod = | Email(string) | Phone(string) | Both(email: string, phone: string) `` This way, the type system enforces at least one contact method. If a new state is needed later (e.g., no contact method), just add a new variant. ## Summary and Shift in Perspective The key is to shift from "type as restriction" to "type as construction". Most languages provide product types (records, tuples) and sum types (enums, unions, algebraic data types). Combined with exhaustive pattern matching, they can precisely model data invariants. Instead of pursuing overly complex type system features, think about how to construct the desired positive space using simple combinations. This approach allows programmers to regain control over the type system and reduce fights with the type checker. --- Source: YouTube: The Unreasonable Effectiveness of Constructive Data Modeling (https://www.youtube.com/watch?v=0BXuYlNrUmE)