Type-level design uses a static type system to encode program information and constraints so invalid programs are rejected before they run. Rather than relying on step-by-step debugging to discover mismatches, it treats the compiler as a gatekeeper for whole classes of errors and aims for valid-by-construction behavior. section 1.5.2 section 5.1
The technique starts with a design question: which operations, values, or combinations should be impossible? Algebraic data types can constrain ordinary inputs; richer type-level features can express relationships between models, interfaces, and extensibility points. The goal is not type machinery for its own sake, but a safer domain representation that directs development toward correct operations. section 1.5.2 section 5.1 section 3.1.2
Rejecting an invalid shape operation
A Shape type permits Circle values with a radius and Rectangle values with width and height. An area function accepts Shape and returns Double. Calling area with an integer fails compilation because Integer does not match Shape, preventing the error before execution. section 1.5.2
A practical use is placing a typed layer over a simple but unsafe boundary. A raw key–value interface can use strings as common ground across databases, while a typed interface separates database representations from domain values and makes conversions safe. This improves correctness without requiring the raw storage mechanism itself to become typed. section 11.0 section 11.3
Type-level design appears at several architectural boundaries:
- Embedded DSLs can formally represent a subsystem’s domain and constrain its permitted operations. section 3.1.2 section 5.1
- A single type-level HTTP schema can describe routes, payloads, formats, methods, and response types for typed servers and clients. section 14.1.1
- Database schemas can use higher-kinded data, associated types, and backend constraints to validate supported columns and table details at compilation. section 12.2.2
Expressiveness has a cost. Type classes, type families, functional dependencies, generalized ADTs, existential types, phantom types, and higher-kinded types can model powerful constraints, but generic library interfaces may expose difficult machinery and increase coupling. A design should therefore assess interfaces in several use cases and keep type-level detail from leaking unnecessarily into application code. section 11.2.2 section 12.2.2 section 11.3
Listing 14.2 HTTP schema for the server and client
type AstroAPI
= ( "meteor" #1
:> ReqBody '[JSON] MeteorTemplate #2
:> Post '[JSON] MeteorId #3
)
:<|>
( "asteroid" #4
:> ReqBody '[JSON] AsteroidTemplate #5
:> Post '[JSON] AsteroidId #6
)
This schema shows type-level declarations encoding two HTTP endpoints, including paths, JSON request bodies, POST methods, and response identifiers. section 14.1.1
