open Reified
open Reified.Refinements
open Reified.Result

Built-in Refined Values

Each type below makes a partial operation total, guarantees a property later operations rely on, or removes a branch from consumers. A wrapper that only validates at construction is a constraint, not a type, see When not to make a type.

open Reified
open Reified.Refinements

What each type buys you

Collections

NonEmptyList carries its non-emptiness in the representation, so the case is public and you can pattern match on it:

let lines = NonEmpty(1, [ 2; 3; 4 ])              // total, no Result

let (NonEmpty(first, rest)) = lines               // total
let total = NonEmptyList.reduce (+) lines         // total, needs no seed
let largest = NonEmptyList.max lines              // total, no option

NonEmptyList.create admits an ordinary sequence and returns Result<NonEmptyList<'T>, Violation>; NonEmptyList.ofList returns an option.

Filtering can remove every item, so filter returns an ordinary list and tryFilter returns an option. traverseResult applies a fallible mapping across the list and accumulates every failure rather than stopping at the first.

NonEmptyArray stays smart-constructed rather than structural. A head-and-tail representation would forfeit contiguous storage and indexed access, which are the reasons to choose an array; the total head/last/reduce/max still apply.

DistinctList exists for toSet: distinct items always produce a set of the same size, where Set.ofList on an ordinary list silently collapses duplicates.

toMap and toMapBy return a Result, because distinctness holds over whole items rather than over keys, [ 1, "a"; 1, "b" ] is a legitimate DistinctList whose entries would collide. They report the collision instead of dropping an entry the way Map.ofList does.

Everyday operations

A refined collection is still a collection. Alongside the operations the invariant makes total, each module carries the everyday list vocabulary, so a pipeline never has to drop back to List and re-admit the result:

let prices = NonEmpty(9.99, [ 4.99; 12.50 ])

let sum     = NonEmptyList.sumBy id lines             // not List.sumBy on a converted list
let mean    = NonEmptyList.average prices             // total: the divisor is never zero
let biggest = NonEmptyList.maxBy id lines             // total: no option

Only the second tier is a reason to use the type:

average is the clearest of the earned ones: List.average [] raises, while the divisor here is the length, which is at least one. item clamps its index into range, and truncate, init, and chunkBySize clamp their count or size, so non-emptiness survives. map2 truncates to the shorter input and returns a non-empty list where List.map2 raises on unequal lengths. skip is total too — a count past the end yields the empty list rather than raising — but it returns an ordinary list, because skipping can consume every item. filter and choose are honest the same way: they return an ordinary list, while tryFilter/tryChoose return an option.

scan is non-empty by construction rather than by inheritance, a scan always emits its seed.

NonEmptyArray mirrors the whole set, and DistinctList carries the operations that cannot introduce a duplicate (sort, sortBy, rev, truncate, filter, fold, sum, sumBy); map and choose deduplicate, because neither a mapping nor a chooser need be injective.

Intervals and bounds

One generic Interval<'T> covers any ordered value. It is always inhabited, so emptiness is reported as an option rather than by a second type:

let window  = Interval.between 1 10             // total: orders its arguments
let other   = Interval.between 5 15
let overlap = Interval.intersect window other   // Interval option, honest about emptiness
let clamped = Interval.clamp 7 window           // total

The ends are Lower and Upper: they name the two bounds' roles, not a traversal. An interval has no direction, so between 5 1 equals between 1 5.

That is why there are two constructors. between accepts either order and repairs it; create asserts the pair is already ordered and fails when it is not. Reach for between in code, and create at a boundary, where an inverted pair is a caller error worth reporting rather than silently swapping.

union returns None when the two intervals do not overlap, because joining them would invent a gap; span closes the gap deliberately.

For instants, DateRange abbreviates Interval<DateTimeOffset> and RefinedSchemas.dateRange uses start/end on the wire. That is a schema-level naming choice, not a second type, every Interval operation applies unchanged.

Bounded<'T> pairs a value with the interval it must stay inside. Bounds are carried at run time, so Bounded.clamp is total and Bounded.map re-clamps, a mapping cannot break the invariant.

Why there are no refined numbers

There is no PositiveInt, NonNegativeDecimal, or NonZeroInt here, and that is deliberate.

F# cannot propagate an invariant through arithmetic. A language with refinement types infers that a + b is positive when a and b are; F# cannot, so every step has to re-establish the fact by hand. Since integer arithmetic is unchecked , Int32.MaxValue + 1 is negative, an addition returning PositiveInt would be unsound, which leaves returning Result:

// what a refined numeric type costs for ((2 + 3) * 4) + 1
PositiveInt.add a b
|> Result.bind (fun s -> PositiveInt.multiply s c)
|> Result.bind (fun m -> PositiveInt.add m d)

Unwrapping, computing, and re-admitting add bulk at every use site and can hide arithmetic mistakes.

Numeric ranges are therefore constraints:

field _.Quantity { constrain (Constraint.greaterThan 0) }

If you want a nominal type for a numeric identifier, where the point is identity rather than arithmetic, define one over the same constraint. Refinement is public, and Customer Id works it through.

Floating point

FiniteFloat excludes NaN and the infinities. Its value is that aggregation means something: one bad reading destroys a whole aggregate, silently.

List.sum     [ 12.5; 3.0; nan; 8.25 ]   // NaN
List.average [ 12.5; 3.0; nan; 8.25 ]   // NaN

The aggregate returns NaN without an exception or an obvious cause. Admitting through FiniteFloat localises that to the one bad reading at the boundary. Infinity poisons sum and average identically, which is why the type excludes both rather than only NaN.

NaN also makes List.contains and List.distinct wrong, since both use IEEE equality under which NaN is not equal to itself.

match FiniteFloat.create 12.5 with
| Ok value ->
    FiniteFloat.negate value |> ignore                    // closed
    FiniteFloat.average (NonEmpty(value, []))             // one Result at the end, not one per step
| Error _ -> failwith "unreachable"

It is not needed for sorting or for Map, Set and Dictionary keys. F# generic comparison already orders NaN consistently, compare nan nan is 0, and NaN sorts first, so those work on plain float. What stays broken is a comparison hand-written with < and >: it reports NaN equal to every value, which is intransitive and makes sortWith return unsorted output without raising.

For the same reason there are no refined numbers, it offers no pairwise arithmetic: unwrap with value, compute in plain float, and re-admit once.

UnitInterval holds a proportion in [0, 1]. It is the only type here closed under multiplication, which is the reason to reach for it:

match UnitInterval.create 0.3, UnitInterval.create 0.6 with
| Ok a, Ok b ->
    UnitInterval.multiply a b |> ignore         // total and closed
    UnitInterval.complement a |> ignore         // total
    UnitInterval.lerp 0.0 10.0 a |> ignore      // total, always lands between the endpoints
    UnitInterval.inverseLerp 0.0 10.0 3.0       // the inverse: where v sits, clamped
    |> ignore
    UnitInterval.saturatingAdd a b              // not closed under +, so this clamps
| _ -> failwith "unreachable"

complement is an involution only up to floating-point rounding, exact for dyadic values, approximate otherwise.

FiniteFloat32 carries the same guarantee for single precision. It has no canonical wire schema, because JSON has no single-precision number, widen with toFiniteFloat at a boundary.

Bounded<'T> gets its schema from RefinedSchemas.bounded bounds itemSchema: the bounds belong to the field rather than to each value, so they are supplied once.

Text

NonBlankString preserves accepted text exactly, and its operations preserve inhabitation:

match NonBlankString.create "hello", NonBlankString.create " world " with
| Ok first, Ok second ->
    NonBlankString.append first second |> ignore   // total
    NonBlankString.trim second |> ignore            // total, trimming inhabited text leaves it inhabited
    NonBlankString.split "," first                  // NonEmptyList<NonBlankString>, never empty
| _ -> failwith "unreachable"

When not to make a type

Trimmed text, slugs, email addresses, and length bounds carry no invariant that any later operation uses. Nothing about a string becomes total or loses a branch once you know its ends are free of whitespace, so a wrapper would only be unwrapped at first use. That is the test, not closure: trimmedness happens to survive concatenation, and it still earns no type. Slug does not even get that far, joining two slugs can break the pattern.

Express them as constraints on a primitive instead, the metadata reaching interpreters is identical:

field _.DisplayName { constrain Constraint.trimmed }

field _.Slug {
    constrain Constraint.present
    constrain (Constraint.pattern slugPattern)
}

The field's schema is inferred from its type, so a constraint needs no withSchema, and each constraint can sit on its own line.

If you do want a nominal type in your own domain, the machinery is still here, see Define Refined Types.

Schema resolution

Every type above has a canonical wire schema, so a bare field resolves it with no withSchema. The 64-bit and floating-point types sit on the Schema.int64 and Schema.float primitives rather than being mapped onto decimal, which would change their meaning. Note that JSON has no literal for NaN or the infinities: a schema that must reject them should use FiniteFloat, whose finite constraint is inspectable metadata like any other.

Continue with Compose Parse and Refinement and Define Refined Types.