I'm publishing this series ahead of Code BEAM Europe this October, where I'll reveal Bondy, a new declarative language for the BEAM: statically typed, functional, relational and rule-based.
Data validation is one of the most boring and error-prone (yet critical) jobs we do. It happens at the edges of our systems, where data arrives from a request, a config file or another service. It has to happen before the data means anything. Once the data is inside, code can trust it and not check it again.
Here is how that usually looks for a config record in Erlang:
-type config() :: #{
max_tokens := pos_integer(),
refill_rate := pos_integer()
}.
-spec new(map()) -> config().
new(#{max_tokens := Max, refill_rate := Rate} = M)
when is_integer(Max), Max > 0, Max =< 10000,
is_integer(Rate), Rate > 0 ->
M;
new(_) ->
error(badarg).Count the places the same fact lives. The -type says max_tokens is a positive integer, for Dialyzer[1]. The guard says it again, for the runtime. The ceiling of 10000 appears only in the guard, because the type spec cannot express it. So the type is now a rough summary of the guard rather than the truth.
And the whole thing covers one way of building a config. Add optional fields, or a config that arrives in pieces, and you write another function with another copy of the rules.
The second post showed the other half of the problem: rules that relate two fields, like "a discount must not exceed a tenth of the total". They don't fit in any schema DSL, so they become control flow. This post covers both halves.
Shapes
In Bondy, a shape is a value that describes which values are allowed. These are all shapes:
| Expression | Meaning |
|---|---|
Int | an integer |
Int & >= 18 | integers from 18 up |
:standard | :premium | one of two atoms |
{name: String, age: Int & >= 0} | a closed record |
{name: String, age: Int & >= 0, ...} | an open record allowing extra fields |
Int & >= 18 is a refinement: Int with a condition attached. The values are still plain integers. The condition only excludes some of them. Shapes with named fields, like the last two, are structural shapes. The others are atomic shapes. Both kinds work the same way everywhere below.
Shapes are ordinary values. You can bind one to a variable, return it from a function, and combine it with other shapes at runtime:
public function adult_check(age) ->
let adult = Int & >= 18
age & adultadult_check(20) => 20
adult_check(15) => Never([#{:code => :conflict,
:message => "Expected value >= 18, got 15", ...}])The & in that function is the most important operator in the language, and it has a name.
Unification
Unification, written &, combines two descriptions of a value into one that satisfies both, or reports that no such value exists. You already use it every time you write a refinement: Int & >= 18 is the shape Int unified with the predicate >= 18.
What it does depends on what you give it, but the idea is always the same: keep everything both sides say, and fail if they disagree.
A value and a shape. The result is the value, if the shape allows it. This is validation:
public function person_check(data: Map) ->
data & {name: String, age: Int & > 0, ...}person_check(#{:name => "Ann", :age => 0})
=> Never([#{:code => :conflict, :message => "Expected value > 0, got 0",
:path => [:age], ...}])The error says which field broke which rule. The ... makes the shape open: data can carry fields the shape does not mention.
Two shapes. The result is a shape that requires both. You can build requirements from pieces:
public function merged(data: Any) ->
let named = {name: String, ...}
let aged = {age: Int & > 0, ...}
data & (named & aged)merged(#{:name => "Ann", :age => 3}) => UnifiedStruct(anonymous){name: "Ann", age: 3}
merged(#{:name => 7, :age => 3})
=> Never([#{:code => :type_mismatch, :message => "Expected 'String', got 7",
:path => [:name], ...}])Two values. The result merges them if they agree, and fails on the first key where they don't:
#{:a => 1} & #{:b => 2} => #{:a => 1, :b => 2}
#{:a => 1} & #{:a => 2} => Never([#{:code => :value_conflict, :path => [:a], ...}])When the compiler can prove that no value satisfies both sides, it reports the conflict before anything runs. Writing 1 & 2 is a type error, "1 & 2 denotes no value". Two map literals that disagree, as above, are caught at runtime.
Data that is not complete yet. This is where unification earns its keep: it accepts data that is not complete yet. Give it a map that has a name but no age:
public function known_so_far(data: Any) ->
data & {name: String, age: Int & > 0, ...}The result is not an error. It is a value with name set and age still open: it records that an age must be a positive integer, but not which one. Unify it later with the rest of the data and it completes. Ask for a finished value too early, with require_concrete, and you get a precise answer instead of a crash:
Error(#{:code => :incomplete,
:message => "Value is not concrete: field `age` is not fully specified", ...})That is how Bondy handles a form completed over several steps, or a config assembled from several files. You unify each piece in as it arrives, and a wrong piece fails at once with its path. The value is usable only once it is complete. There is one set of rules, not one validator per stage.
A failed unification produces a Never (the bottom type) value carrying the reasons, not an exception, so you decide what to do with it. The same operation appears across the language: matching a pattern in a function head is one-sided unification. So is matching a fact in a rule, which the next posts rely on.
Structural types
A structural type is a structural shape with a name (a.k.a. brand):
type Config = {
max_tokens: Int & > 0 & =< 10000,
refill_rate: Int & > 0
}The name matters. It gives Config an identity: a plain map with the right keys is not a Config until you build one. A function that expects a Config does not accept a map. So the checks run in one place, when a value becomes a Config, and never again after that.
There are three ways to build one, and they differ in how much they check.
1. Config(...) checks everything. With a literal, the compiler does the check:
public function bad() :: Config ->
Config(max_tokens: -3, refill_rate: 1)-- TYPE CHECK FAILED ---------------------------------
|
9 | Config(max_tokens: -3, refill_rate: 1)
| ^ field max_tokens: a value of type -3 is not a value of the declared field type Int & > 0 & =< 10000With a value that only exists at runtime, the same predicate runs when the constructor is called:
public function from_input(max_tokens: Int, refill_rate: Int) :: Config ->
Config(max_tokens: max_tokens, refill_rate: refill_rate)from_input(-3, 5) => error: runtime — cannot construct Config: Expected value > 0, got -3 (field `max_tokens`)Look at the two snippets again. The refinement you wrote for the compiler is the one the runtime enforces.
2. construct(data, Config) checks without crashing. It takes a map from the outside world and returns Ok or Error, with the path of every field that failed:
construct(#{:max_tokens => 20000, :refill_rate => 5}, Config)
=> Error(#{:code => :construct_failed,
:message => "Unification failed",
:reasons => [#{:message => "Expected value =< 10000, got 20000",
:path => [:max_tokens], ...}]})This is the one to use at the edge of your system.
3. Config!(...) trusts you. It builds the value and skips the runtime check: given a max_tokens of -3 that only exists at runtime, Config!(max_tokens: max_tokens, refill_rate: 5) returns Config(max_tokens: -3, refill_rate: 5). The compiler still refuses what it can see is wrong, such as a literal -3 or a String where an Int belongs. It does not demand proof of > 0. Use it for values you already know are good, which is most values once they are inside the system.
Fields can also say whether the data must supply them, and a string field can carry a pattern (=~):
type User = {
name: String,
age: Int & >= 0,
email?: String & =~ "^[^@\\s]+@[^@\\s]+$", %% may be absent; checked when present
tls!: Bool %% must be supplied by the caller
}construct(#{:name => "Ann", :age => 30}, User)
=> Error(... "Required field tls must be provided ..." ...)
construct(#{:name => "Ann", :age => 30, :tls => true}, User)
=> Ok(User(name: "Ann", age: 30, tls: true))
construct(#{:name => "Ann", :age => 30, :tls => true, :email => "ann"}, User)
=> Error(... "Value \"ann\" does not match pattern ..." ... :path => [:email] ...)And a field can be computed from its siblings. The leading dot means "this value's field":
type Invoice = {
quantity: Int,
unit_price: Float,
subtotal: .unit_price * .quantity,
tax: .subtotal * 0.1,
total: .subtotal + .tax
}Invoice(quantity: 3, unit_price: 10.0)
=> Invoice(quantity: 3, unit_price: 10.0, subtotal: 30.0, tax: 3.0, total: 33.0)The fields are computed in dependency order, from the fields you supply, so the arithmetic that used to sit in a constructor lives in the type.
Rules between fields
That leaves the rules from the second post, the ones no schema DSL could hold: the order line's new/1. A discount must not exceed a tenth of the total, and a total above 10000 needs an approver. In Bondy they go on the fields, with when:
%% Amounts are in pence.
type OrderLine = {
price: Int & > 0,
quantity: Int & > 0,
total: .price * .quantity when .total =< 10000 or .approved_by !== null,
discount: Int & >= 0 = 0 when .discount * 10 =< .total,
approved_by?: String
}The 10% rule is written as .discount * 10 =< .total: whole-number arithmetic, so the check never divides and needs no rounding policy. The approval rule sits on total, not on approved_by, because a when on an optional field runs only when the field is there. An absent approved_by reads as null. These are the results of construct on seven order lines, straight from the program:
| price × quantity | discount | approved_by | case | result |
|---|---|---|---|---|
| 100 × 3 | — | — | no discount given | accepted, with discount: 0 |
| 100 × 3 | 30 | — | exactly 10% | accepted |
| 100 × 3 | 31 | — | 10% and a penny | rejected: the when rule fails at discount |
| 100 × 3 | -1 | — | negative | rejected: "Expected value >= 0, got -1" at discount |
| 5000 × 2 | — | — | total of exactly 10000 | accepted |
| 5001 × 2 | — | — | large order, no approver | rejected: the when rule fails at total |
| 5001 × 2 | — | "ana" | large order, approved | accepted |
In an Ecto changeset these rules live on one write path, and hold only for values that pass through that function. A code path that skips the changeset skips the rules. Here they live on the type, so every OrderLine in the system satisfies them, whichever path built it.
What gets checked, and when
A shape does not make checking free. It changes where the check lives and how often you write it.
- Known at compile time: a literal that breaks a refinement never compiles. Neither does a meet the compiler can prove empty, such as
1 & 2. - Known only at runtime: the check runs once, where the value is built or unified, and returns the field path that failed. After that the value is trusted.
- Vouched for:
Config!(...)skips the runtime check. - Not complete yet: unification keeps what is known, fails early on anything wrong, and tells you exactly which field is still missing.
You still pay for the checks the compiler cannot prove away. What changes is that you stop writing them by hand, and stop scattering them across every path that might forget one.
From one value to many
Everything in this post checks one value, in one direction: the data arrives, and the shape says yes or no. A when on a field sees the other fields of the same value and nothing else.
Real systems have rules that span many values: a request is allowed only while its bucket has tokens, an alarm clears only when someone acknowledges it. Those rules are not attached to a type. They watch a collection of values and act when a combination of them appears. That is the next noun, the rule, and the next post.