Repository F# setup

open Reified
open Reified.Refinements
open Reified.Result

Refined

Maturity: Incubating

Reified.Refinements supplies types that carry an invariant, together with the operations that invariant makes possible. Guarded construction is how a value is admitted, but it is not the reason to reach for a refined type, a wrapper that only checks on the way in leaves callers unwrapping it at first use, and the invariant buys nothing after the boundary.

These types remove checks from later code:

Fragment

let total = NonEmptyList.reduce (+) lines   // no seed, no empty case, no option
let largest = NonEmptyList.max lines        // total
let ratio = UnitInterval.multiply a b       // closed: still in [0, 1]

NonEmptyList.max returns a value rather than an option because the type makes the empty case unrepresentable. A type belongs here if it makes a partial operation total, guarantees a property later operations rely on, encodes a relationship between values, preserves an invariant across useful operations, or removes a branch from consumers.

Validation that fails that test belongs in a constraint instead. Trimmed text and slugs make nothing later total or simpler: no operation on a string needs the ends to be free of whitespace, and none needs a particular pattern. So they are Constraint.trimmed and Constraint.pattern on an ordinary string, not types. See When not to make a type.

Reified.Refinements depends only on Reified.Constraint. It does not parse text and does not normalize input.

dotnet add package Reified.Refinements

Verified

open Reified
open Reified.Refinements

Reified

Refinements

Admission

Every built-in type has a constructor returning Result<'refined, Violation>:

Verified

let name : Result<NonBlankString, Violation> = Refine.nonBlankString "Ada"
let lines : Result<NonEmptyList<string>, Violation> = Refine.nonEmptyList [ "a"; "b" ]

Refine.nonBlankString "  "               // Error (Atomic (Expected (PresenceAtom Present, None)))
Refine.nonEmptyList ([]: string list)    // Error (Atomic (Expected (CardinalityAtom (Minimum 1), Some (Integer 0L))))

name: Result<NonBlankString,Violation>

Microsoft.FSharp.Core.FSharpResult`2

Helper type for error handling without exceptions. Choices and Results

Reified.Refinements.NonBlankString

A string that is not null, empty, or whitespace.

Reified.Violation

Why a value failed its constraint. A diagnostic contract, not an application error union. Domain code maps a whole violation once with Result.mapError; Schema adds the path at which it occurred. Violations are plain comparable data. No closure and no constraint description is reachable from one, so structural equality holds and a violation can be retained and compared long after the constraint that produced it went out of scope. There is no promised wire format. Reified-produced groups are never empty and never unary: a single failing child is returned directly rather than wrapped. The first * rest shape encodes non-emptiness only; non-unarity is a normalization invariant.

Reified.Refinements.RefineModule

Smart constructors for built-in refined values, and the refinements behind them. Text, Character, Collection, and Choice are nested here rather than declared beside Refine. Each names a concept general enough to shadow something a caller already has in scope, and none of them is a companion to a type this package exports, so there is nothing to gain from the type-and-module pairing that keeps NonBlankString and DistinctList at the top level.

nonBlankString: string -> Result<NonBlankString,Violation>

lines: Result<NonEmptyList<string>,Violation>

Reified.Refinements.NonEmptyList`1

A list that contains at least one item. The case is public: non-emptiness is carried by the representation rather than by a checked constructor, so head, last, reduce, min, and max are total and pattern matching is available to callers.

string

An abbreviation for the CLI type . Basic Types

nonEmptyList: 'a seq -> Result<NonEmptyList<'a>,Violation>

list

The type of immutable singly-linked lists. See the module for further operations related to lists. Use the constructors [] and :: (infix) to create values of this type, or the notation [1; 2; 3]. Use the values in the List module to manipulate values of this type, or pattern match against the values directly. See also F# Language Guide - Lists.

Requires & types

Requires: open Reified; open Reified.Refinements (packages: Reified.Constraint, Reified.Refinements)

val name: Result<NonBlankString,Violation>

val lines: Result<NonEmptyList<string>,Violation>

Some types also offer a total constructor, which is the one to prefer when the input has an obvious correct reading:

Fragment

let lines = NonEmpty(first, rest)              // cannot fail
let window = Interval.between finish start     // cannot fail: orders the pair
let ratio = UnitInterval.clamp 1.5             // cannot fail: clamps to 1.0

Read the underlying value through the Value member or the module's value function.

Where the invariant pays

The smallest contrast is one partial operation becoming total:

Fragment

List.max lines            // throws on an empty list
NonEmptyList.max lines    // total: returns the value

Avoiding the exception means writing the option version by hand, and then every caller unwraps it:

Verified

let tryMax lines =
    if List.isEmpty lines then None else Some (List.max lines)

tryMax: 'a list -> 'a option

lines: 'a list

Microsoft.FSharp.Collections.ListModule

Contains operations for working with values of type . Operations for collections such as lists, arrays, sets, maps and sequences. See also F# Collection Types in the F# Language Guide.

isEmpty: 'T list -> bool

Returns true if the list contains no elements, false otherwise. The input list. True if the list is empty. [ ] |> List.isEmpty Evaluates to true [ "pear"; "banana" ] |> List.isEmpty Evaluates to false

None

The representation of "No value"

Some

The representation of "Value of type 'T" The input value. An option representing the value.

max: 'T list -> 'T

Return the greatest of all elements of the list, compared via Operators.max. Raises if list is empty The input list. Thrown when the list is empty. The maximum element. let inputs = [ 10; 12; 11 ] inputs |> List.max Evaluates to 12 let inputs = [ ] inputs |> List.max Throws System.ArgumentException.

Requires & types

val tryMax: 'a list -> 'a option

That option is the empty case travelling downstream. NonEmptyList settles it once, at construction, and every later caller reads a value.

The same saving shows up in aggregates:

Isolated

open Reified.Refinements

type OrderLine = { Total: decimal }

// plain: every caller re-establishes what is already true
let averageLinePlain (lines: OrderLine list) =
    if List.isEmpty lines then None
    else Some (List.sumBy _.Total lines / decimal lines.Length)

// refined: the empty case cannot arise, so there is nothing to return an option for
let averageLineRefined (lines: NonEmptyList<OrderLine>) =
    NonEmptyList.averageBy _.Total lines

Reified

Refinements

FsLiveDocsGeneratedPage40_163BCE492C58.OrderLine

Total: decimal

decimal

An abbreviation for the CLI type . Basic Types

averageLinePlain: OrderLine list -> decimal option

lines: OrderLine list

list

Microsoft.FSharp.Collections.ListModule

Contains operations for working with values of type . Operations for collections such as lists, arrays, sets, maps and sequences. See also F# Collection Types in the F# Language Guide.

isEmpty: 'T list -> bool

None

The representation of "No value"

Some

The representation of "Value of type 'T" The input value. An option representing the value.

sumBy: ('T -> ^U) -> 'T list -> ^U

Returns the sum of the results generated by applying the function to each element of the list. The function to transform the list elements into the type to be summed. The input list. The resulting sum. let input = [ "aa"; "bbb"; "cc" ] input |> List.sumBy (fun s -> s.Length) Evaluates to 7.

_arg1: OrderLine

(/): ^T1 -> ^T2 -> ^T3

Overloaded division operator The first parameter. The second parameter. The result of the operation. 16 / 2 // Evaluates to 8

decimal: ^T -> decimal

Converts the argument to System.Decimal using a direct conversion for all primitive numeric types. For strings, the input is converted using UInt64.Parse() with InvariantCulture settings. Otherwise the operation requires an appropriate static conversion method on the input type. The input value. The converted decimal. decimal "42.23" // evaluates to 42.23M decimal 0xff // evaluates to 255M decimal -10 // evaluates to -10M

Length: int

Gets the number of items contained in the list

averageLineRefined: NonEmptyList<OrderLine> -> decimal

lines: NonEmptyList<OrderLine>

Reified.Refinements.NonEmptyList`1

Reified.Refinements.NonEmptyListModule

Operations over lists that carry their non-emptiness in the type.

averageBy: ('value -> ^a) -> NonEmptyList<'value> -> ^a

Averages a projection of the items. Total, for the same reason as average.

The collection types carry the ordinary list vocabulary, sum, sumBy, average, choose, countBy, item, alongside operations the invariant makes total. A refined type that only offered the clever operations would push you back through toList for everyday work, and the invariant would be lost halfway down the pipeline. See the catalogue.

Order Totals works this through on a realistic domain.

There are no refined numbers

F# cannot propagate an invariant through arithmetic the way a refinement-typed language can, so a PositiveInt would have to re-establish "greater than zero" at every step. With unchecked integer arithmetic, Int32.MaxValue + 1 is negative, that means returning Result from addition, and a Result per arithmetic step is bulk that hides mistakes rather than catching them.

Numeric ranges are constraints instead:

Fragment

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

FiniteFloat prevents NaN and infinity from silently destroying an aggregate: List.average [ 12.5; 3.0; nan; 8.25 ] is NaN. Its purpose is not arithmetic or ordering. See the catalogue.

Define your own

The machinery is public, so an application type gets the same treatment:

Verified

type CustomerId =
    private
    | CustomerId of int

    member this.Value =
        let (CustomerId value) = this
        value

module CustomerId =
    let refinement = Refinement.define (Constraint.greaterThan 0) CustomerId _.Value
    let create value = Refinement.create refinement value

type CustomerId with
    static member Schema(_: CustomerId) : Schema<CustomerId> =
        Schema.int |> Schema.refine CustomerId.refinement

FsLiveDocsGeneratedPage39_163BCE492C58.CustomerId

CustomerId

int

An abbreviation for the CLI type . Basic Types

this: CustomerId

Value: CustomerId -> unit -> int

value: int

FsLiveDocsGeneratedPage39_163BCE492C58.CustomerIdModule

refinement: Refinement<int,CustomerId>

Reified.Refinements.Refinement

Creates and applies reusable refinement definitions.

define: Constraint<'underlying> -> ('underlying -> 'refined) -> ('refined -> 'underlying) -> Refinement<'underlying,'refined>

Defines a refinement from one constraint, a constructor, and the reverse projection. Compose several rules with Constraint.all before defining, and reach for Constraint.custom when the rule is an arbitrary predicate. Both produce an ordinary constraint, so there is no separate plural or check-taking constructor. type RetryCount = RetryCount of int let retryCount = Refinement.define (Constraint.between 0 10) RetryCount (fun (RetryCount value) -> value)

Reified.ConstraintModule

Creates, executes, composes, and inspects constraints.

greaterThan: 'value -> Constraint<'value>

Requires a value strictly greater than the supplied bound. let quantity : Constraint<int> = Constraint.greaterThan 0

_arg1: CustomerId

Value: int

create: int -> Result<CustomerId,Violation>

create: Refinement<'underlying,'refined> -> 'underlying -> Result<'refined,Violation>

Constructs a refined value, reporting why the raw value was not admitted. type RetryCount = RetryCount of int let retryCount = Refinement.define (Constraint.between 0 10) RetryCount (fun (RetryCount value) -> value) 3 |> Refinement.create retryCount |> Result.mapError Violation.render

Schema: CustomerId -> Schema<CustomerId>

Reified.Schema`1

Describes a typed value's portable structure and construction for schema interpreters. A schema records shape and construction metadata without tying that metadata to input parsing, diagnostics, validation, codecs, UI generation, or workflow execution. Primitive, collection, optional, union, refined, and record declarations all produce Schema<'value>. Record declarations use the schema<'value> { } computation expression. Each field may contain withSchema, constrain, constraints, refine, and validate operations before the declaration finishes with construct or constructResult.

Reified.Schema

Construction, composition, parsing, and checking for universal schemas.

int: Schema<int>

Describes a 32-bit integer.

(|>): 'T1 -> ('T1 -> 'U) -> 'U

Apply a function to a value, the value being on the left, the function on the right The argument. The function. The function result. let doubleIt x = x * 2 3 |> doubleIt // Evaluates to 6

refine: Refinement<'raw,'value> -> Schema<'raw> -> Schema<'value>

Maps a raw schema through a reusable bidirectional refinement. The smart constructor runs during parsing. Inspection supplies the raw representation during checking and encoding.

Requires & types

Requires: open Reified; open Reified.Refinements (packages: Reified.Constraint, Reified.Refinements, Reified.Schema)

val refinement: Refinement<int,CustomerId>

val create: int -> Result<CustomerId,Violation>

Refinement.constraints exposes the same rules to Schema and other interpreters, so the type describes itself at a boundary without restating the rule. The static member Schema above registers the type's canonical schema. Customer Id builds both end to end.

Once the type is registered that way, a schema field of that type needs nothing but the field: field _.Id resolves the canonical schema, and a failure at that field is reported with its path alongside every other field's. Without the registration, the field needs an explicit schema via withSchema/refine. See Refined Schemas.

Refined

Admission

Where the invariant pays

There are no refined numbers

Define your own

Read next

Overview

Docs

API Reference