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

Define Refined Types

A refined type is a private wrapper, a checked constructor, and one canonical way to recover the underlying value. Before reaching for it, decide whether the concept deserves a type at all. Checked construction is how a value is admitted, not a reason on its own: if nothing downstream becomes total or loses a branch, the rule belongs in a constraint on the primitive instead. Numeric ranges are the clearest example, F# cannot carry "greater than zero" through arithmetic, so a refined number costs more at every use site than it saves. When not to make a type draws the line, and Customer Id works a full example through.

Define the wrapper and Value projection

Verified
open Reified
open Reified.Refinements

type ContactEmail =
    private
    | ContactEmail of string

module ContactEmail =
    let value (ContactEmail value) = value

Guard construction with a refinement

Use Refinement.define when one constraint from the built-in catalogue describes admission. Those constraints are interpreted: Reified can read the rule as data, so the refinement carries metadata other tools can use, not only a check.

Isolated
open Reified
open Reified.Refinements

type ContactEmail =
    private
    | ContactEmail of string

module ContactEmail =
    let value (ContactEmail value) = value

    let refinement =
        Refinement.define
            Constraint.email
            ContactEmail
            value

    let create raw =
        Refinement.create refinement raw

ContactEmail.create is now the only way in. Construction returns check failures directly:

Fragment
let email : Result<ContactEmail, Violation> =
    ContactEmail.create rawEmail

Combine constraints

Constraint.all checks every listed constraint against the same original value and combines their failures; give the combined constraint to the same Refinement.define used above:

Isolated
open Reified
open Reified.Refinements

type ContactEmail =
    private
    | ContactEmail of string

module ContactEmail =
    let value (ContactEmail value) = value

    let refinement =
        Refinement.define
            (Constraint.all
                [ Constraint.present
                  Constraint.email
                  Constraint.maxLength 254 ])
            ContactEmail
            value

    let create raw = Refinement.create refinement raw

The same constraint values provide executable checks and ConstraintDescription metadata.

Use a metadata-free check

Use Constraint.customWith for an invariant no built-in constraint describes, then hand that opaque constraint to Refinement.define like any other. The check runs, but nothing downstream can read the rule, the trade-off is interpreted versus opaque. customWith's metadata label ("even-number rule" below) only feeds that opaque ConstraintDescription; a caller sees the callback's own Described text on failure, not that string:

Isolated
open Reified
open Reified.Refinements

type EvenInt = private EvenInt of int

module EvenInt =
    let value (EvenInt value) = value

    let private even value =
        if value % 2 = 0 then Ok ()
        else Error(Violation.described "must be an even number")

    let refinement =
        Refinement.define (Constraint.customWith "even-number rule" even) EvenInt value

Projection law

For every successful construction, the reverse projection returns the supplied underlying value:

Isolated
open Reified
open Reified.Refinements

type ContactEmail =
    private
    | ContactEmail of string

module ContactEmail =
    let value (ContactEmail value) = value

    let refinement =
        Refinement.define
            (Constraint.all [ Constraint.present; Constraint.email; Constraint.maxLength 254 ])
            ContactEmail
            value

    let create raw = Refinement.create refinement raw

let result =
    ContactEmail.create "ada@example.com"
    |> Result.map (Refinement.underlying ContactEmail.refinement)

// Ok "ada@example.com"

Choose one concrete underlying representation. For collection refinements, prefer 'a list or 'a array rather than an arbitrary seq<'a>.

Give the type its operations

A wrapper that only checks on the way in leaves callers unwrapping it at first use. What makes the type worth having is the family of operations that preserve its invariant, so the fact stays true without being rechecked:

Isolated
open Reified
open Reified.Refinements

type ContactEmail =
    private
    | ContactEmail of string

module ContactEmail =
    let value (ContactEmail value) = value

    let refinement =
        Refinement.define
            (Constraint.all [ Constraint.present; Constraint.email; Constraint.maxLength 254 ])
            ContactEmail
            value

    let create raw = Refinement.create refinement raw

    // ... as in "Combine constraints" above

    /// Total for this refinement: lower-casing never introduces an `@`, so the `email`
    /// shape survives, and it does not lengthen the text, so `maxLength 254` still holds.
    /// The proof is specific to the constraints in `refinement` — change them and revisit.
    let normalise (input: ContactEmail) = ContactEmail(value input |> fun text -> text.ToLowerInvariant())

Lower-casing is closed under this refinement because the email constraint only tests that the text is two non-empty runs of non-@ characters around one @, and lower-casing never introduces an @, while maxLength 254 survives because ToLowerInvariant keeps the string length. That argument is tied to the rules listed in refinement; if the constraints change to something case-sensitive or length-critical, normalise has to be revisited.

If no operation preserves the invariant, use a constraint instead.

Continue with Schema Integration.