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

open FsSpec
type InventoryCount = private InventoryCount of int
module InventoryCount = 
    let spec = Spec.all [Spec.min 0; Spec.max 1000]
    let tryCreate n =
      Spec.validate spec n 
      |> Result.map InventoryCount

// Generate data
let inventoryAmounts = Gen.fromSpec InventoryCount.spec |> Gen.sample 0 10

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

type PhoneNumber = private PhoneNumber of string
module PhoneNumber = 
    let tryCreate str =
      if (Regex(@"\d{3}-\d{4}-\d{4}").IsMatch(str))
      then Some (PhoneNumber str)
      else None 

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.

let inventorySpec = Spec.all [Spec.min 0; Spec.max 1000]

// Validation
Spec.isValid inventorySpec 20

// Explanation: understand what constraints failed (as a data structure)
Spec.explain inventorySpec -1

// Validation Messages
Spec.explain inventorySpec -1 |> Formatters.prefix_allresults // returns: "-1 failed with: and [min 0 (FAIL); max 1000 (OK)]"

// Data Generation (with FsCheck)
Gen.fromSpec inventorySpec |> Gen.sample 0 10  // returns 10 values between 0 and 1000

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

let spec = Spec.predicate "predicate min/max" (fun i -> 0 < i && i < 5)

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.