Type-driven and Domain-driven approaches commonly represent constrained values as a type. This approach is good, but generally leaves the constraints implicitly buried in functions. FsSpec exposes those constraints as data so they can be programmatically understood for validation, data generation, and more.
Short Motivation
FsSpec represents value constraints as data to reuse one constraint declaration for validation, data generation, error explanation, and more.
It also makes for a concise and consistent Type-Driven approach
|
|
Longer Motivation
Type-Driven and/or Domain-Driven systems commonly model data types with constraints. For example,
- a string that represents an email or phone number (must match format)
- an inventory amount between 0 and 1000
- Birthdates (can’t be in the future)
We centralize these constraints by wrapping them in a type, such as
|
|
This is great. It prevents defensive programming from leaking around the system and clearly encodes expectations on data. It avoids the downsides of primitive obsession.
However, we’re missing out on some power. We’re encoding constraints in a way that only gives us pass/fail validation. We have to duplicate constraint information if we want to explain a failed value, generate data, or similar actions.
FsSpec represents these constraints as data so that our programs can understand the constraints on a value.
|
|
There are also other possibilities FsSpec doesn’t have built-in. For example,
- Comparing specifications (i.e. is one a more constrained version of the other)
- Serialize and interpret constraints for use in different UI technologies
- Automatic generator registration with property testing libraries (e.g. FsCheck)
Limitations
FsSpec interpreset constraint data for many purposes, but not all data is created equal.
In particular, custom constraints are added to FsSpec as predicates. These are very flexible for validation, but their meaning cannot be generally inferred. This means that cannot intelligently generate data from custom constraints. The best it can do is filter unconstrained data based on the predicate.
Consider
|
|
The above case will probably not generate. It is filtering a list of randomly generated integers, and it is unlikely many of them will be in the narrow range of 0 to 5. FsSpec can’t understand the intent of the predicate to create a smarter generator. Users can always extend the core operations with wrappers that handle their custom types if desired.
Original Experiments and Language-integrated constraints
FsSpec is latest step in a long journey to better leverage value constraints in our code. This has led me through testing approaches (and their pitfalls), dependent type systems, and math proofs.
Originally, I tried to extend F#’s type system with constrained values. However, F# intentionally does not include macros or other language extension mechanisms.
It also turns out adding constraints to the type system has already been done, and much more thoroughly. Languages like F*, Idris, or Dafny use constraints on types to prove qualities of a program at compile-time. For example, F* can prove that a program handles all it’s input values and the general bounds of resource usage. This class of languages is called a dependent-type system, or a proof-oriented language.
Learning about these languages pivoted my approach. FsSpec instead leans into the static type system. It allows the existing type system to enforce expectations (i.e. via constrained construction) while the library focuses on making the constraint data accessible and consumable.
Conclusion
FsSpec exposes value constraints as data. This allows programs to operate on the constraints themselves and resuse a single declaration for many purposes. I have high hopes this approach can normalize and simplify type-driven development, ultimately leading to clearer and safer systems.