Reified
Repository F# setup
open Reified
open Reified.Refinements
open Reified.Result

Order Totals Tutorial

This tutorial builds an order from untrusted input and then calculates over it. Each invariant admitted at the boundary removes a branch, an option, or a guard from downstream code.

Verified
open System
open Reified
open Reified.Refinements
open Reified.Result
open Reified.ResultDSL

Model the domain

Verified
type OrderLine =
    { Sku: NonBlankString
      Quantity: int
      UnitPrice: decimal }

type Order =
    { Reference: NonBlankString
      Lines: NonEmptyList<OrderLine>
      Discount: UnitInterval
      Delivery: Interval<DateTimeOffset> }

The refined field types specify the order's invariants. An order has at least one line. The discount is a proportion, so it cannot be 140% or NaN. The delivery window's start is not after its end. None of those facts needs restating later, because none of them can be false.

Quantity and price are ordinary numbers, so their "greater than zero" rule lives in the orderLine constructor below rather than in the type: a caller who builds an OrderLine record directly can still put a negative quantity or price in it. They are not refined types because F# cannot carry "greater than zero" through arithmetic, see why there are no refined numbers.

Admit the input

Verified
let orderLine rawSku rawQuantity rawPrice =
    result {
        let! sku = Refine.nonBlankString rawSku
        let! _ = Constraint.check (Constraint.greaterThan 0) rawQuantity
        let! _ = Constraint.check (Constraint.greaterThan 0m) rawPrice
        return { Sku = sku; Quantity = rawQuantity; UnitPrice = rawPrice }
    }

The orderLine constructor is where quantity and price are admitted, and each refined constructor rejects its own invalid input:

Verified
orderLine "SKU-1" 0 9.99m      // Error, quantity must be positive
orderLine "   " 1 9.99m        // Error, sku is blank
Refine.nonEmptyList ([]: OrderLine list)
                               // Error, an order needs at least one line
UnitInterval.create 1.4        // Error, outside [0, 1]
UnitInterval.create Double.NaN // Error, NaN is outside every interval

All four field constructors fail with the same Violation type, so one result { } block admits the whole order without an error-union mapping:

Verified
let order
    rawReference
    (rawLines: (string * int * decimal) list)
    rawDiscount
    rawFrom
    rawTo
    =
    result {
        let! reference = Refine.nonBlankString rawReference

        let! lines =
            rawLines
            |> Result.traverse (fun (sku, quantity, price) -> orderLine sku quantity price)
            |> Result.bind Refine.nonEmptyList

        let! discount = UnitInterval.create rawDiscount
        let! delivery = Interval.create rawFrom rawTo

        return
            { Reference = reference
              Lines = lines
              Discount = discount
              Delivery = delivery }
    }

Result.traverse runs orderLine over every raw line and stops at the first failure; Refine.nonEmptyList then checks that the collected lines form a non-empty list, so an empty order is rejected before the Order exists.

Verified
let orderFrom = DateTimeOffset(2026, 6, 1, 0, 0, 0, TimeSpan.Zero)
let orderTo = DateTimeOffset(2026, 6, 5, 0, 0, 0, TimeSpan.Zero)

order "ORD-1" [ "SKU-1", 2, 9.99m ] 0.15 orderFrom orderTo
// Ok { Reference = …; Lines = …; Discount = …; Delivery = … }

order "ORD-1" [] 0.15 orderFrom orderTo
// Error, an order needs at least one line

Two of the four fields have a total constructor, which is the one to prefer when the input has an obvious correct reading:

Verified
let requestedFrom = DateTimeOffset(2026, 6, 1, 0, 0, 0, TimeSpan.Zero)
let requestedTo = DateTimeOffset(2026, 6, 5, 0, 0, 0, TimeSpan.Zero)
let rawDiscount = 0.15

let window = Interval.between requestedFrom requestedTo  // cannot fail: orders the pair
let discount = UnitInterval.clamp rawDiscount            // cannot fail: clamps into [0, 1]

Interval.between accepts the two instants in either order. Use Interval.create instead when an inverted pair means the caller made a mistake you would rather report than repair.

Calculate, without re-checking anything

Line and order totals

The numbers are plain, so the arithmetic is plain:

Verified
let lineTotal (line: OrderLine) = decimal line.Quantity * line.UnitPrice

let subtotal (order: Order) =
    order.Lines |> NonEmptyList.map lineTotal |> NonEmptyList.reduce (+)

reduce needs no seed or empty case, and adds no Result between operations.

Discount

Verified
let payable (order: Order) =
    let multiplier = UnitInterval.complement order.Discount
    subtotal order * decimal (UnitInterval.value multiplier)

complement is total and closed, so multiplier is guaranteed to be in [0, 1]. For an order admitted through orderLine, quantity and price are positive, so the subtotal is nonnegative and the payable amount cannot exceed the subtotal or go negative — no discount value allows either. That guarantee comes from admission, not from the record types: a directly constructed OrderLine with a negative price breaks it, and decimal arithmetic can still overflow on very large values.

The conversion to decimal is deliberate rather than hidden. UnitInterval is a double, money is a decimal, and mixing the two is a rounding decision that belongs in your code.

Statistics

Verified
let largestLine (order: Order) =
    order.Lines |> NonEmptyList.maxBy (fun line -> line.Quantity)

let lineCount (order: Order) =
    NonEmptyList.length order.Lines

let averageUnitPrice (order: Order) =
    order.Lines |> NonEmptyList.averageBy (fun line -> line.UnitPrice)

maxBy returns an OrderLine, not an option. averageBy returns a decimal, not an option, because the divisor is the length and the length is at least one. Each of those is a branch the plain-list version would have had to write. For contrast only, not part of the running example:

Isolated
type OrderLine = { Quantity: int; UnitPrice: decimal }

// what the same three functions cost over an ordinary list
let largestLine lines = lines |> List.sortByDescending (fun l -> l.Quantity) |> List.tryHead
let averageUnitPrice lines =
    if List.isEmpty lines then None
    else Some (List.sumBy (fun (l: OrderLine) -> l.UnitPrice) lines / decimal (List.length lines))

The collection modules carry the everyday operations (sum, sumBy, average, choose, countBy) as well as the total ones, so nothing here converts back to a list to do ordinary work.

Delivery window

Verified
let isDeliverable (order: Order) (candidate: DateTimeOffset) =
    Interval.contains candidate order.Delivery

let overlapWith (order: Order) (other: Interval<DateTimeOffset>) =
    Interval.intersect order.Delivery other   // Interval option, None when disjoint

intersect returns an option because two windows may not overlap. An empty interval is not representable, so the option reports emptiness without creating a value whose Lower is above its Upper.

Catch a duplicate the type system can see

Distinctness is a relationship between values, so it needs a checked constructor, but the resulting type then converts to a map without silently dropping entries:

Verified
let skus (order: Order) =
    order.Lines
    |> NonEmptyList.map (fun line -> NonBlankString.value line.Sku)
    |> NonEmptyList.toList
    |> DistinctList.create      // Error, rejected: the same SKU appears twice

let lineBySku (order: Order) =
    order.Lines
    |> NonEmptyList.toList
    |> List.map (fun line -> NonBlankString.value line.Sku, line)
    |> DistinctList.create
    |> Result.bind DistinctList.toMap

Map.ofList on an ordinary list keeps only the last of each duplicate key and reports nothing. DistinctList.toMap returns a Result instead: distinctness holds over whole pairs rather than over keys, so it checks the keys and tells you about a collision rather than losing an entry.

What the invariants removed

Fact carried by a type Branch it removed
NonEmptyList has a first item no tryHead, no option from max/reduce
NonEmptyList has a positive length no divide-by-zero on an average
UnitInterval is in [0, 1] no clamping the multiplier before applying it
Interval has Lower <= Upper no "did they send these backwards" check
DistinctList has no duplicates no silent collapse building a set; a reported failure building a map
NonBlankString is never empty or whitespace no blank-string guard at every read site

Next