Repository F# setup
open Reified
open Reified.Refinements
open Reified.ResultInterpreted and opaque
Constraints come in two tiers, distinguished by whether tools other than the runtime can understand the rule.
Interpreted constraints
The built-in catalogue is a closed algebra. Each constructor builds exactly one ConstraintAtom and puts that same
value in both its description and any violation it produces, so a primitive's identity and its failure cannot drift
apart.
open Reified
let nameLength : Constraint<string> = Constraint.maxLength 80
(Constraint.inspect nameLength).Expression
// Atom (CardinalityAtom (Cardinality.Maximum 80))
Constraint.check nameLength (String.replicate 81 "a")
// Error (Atomic (Expected (CardinalityAtom (Cardinality.Maximum 80), Some (Integer 81L))))
ReifiednameLength: Constraint<string>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
stringAn abbreviation for the CLI type . Basic Types
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
maxLength: int -> Constraint<^value>Requires text or a collection to have at most the supplied size. let summary : Constraint<string> = Constraint.maxLength 280
Expression: ConstraintExpressionThe constraint's logical form.
inspect: Constraint<'value> -> ConstraintDescriptionReturns the constraint's inspectable description. let requiredName : Constraint<string> = Constraint.present (Constraint.inspect requiredName).Expression
check: Constraint<'value> -> 'value -> Result<unit,Violation>Runs a constraint, returning why the value failed. let retryCount = Constraint.between 0 10 42 |> Constraint.check retryCount |> Result.mapError Violation.render
Microsoft.FSharp.Core.StringModuleFunctional programming operators for string processing. Further string operations are available via the member functions on strings and other functionality in System.String and System.Text.RegularExpressions types. Strings and Text
replicate: int -> string -> stringReturns a string by concatenating count instances of str. The number of copies of the input string will be copied. The input string. The concatenated string. Thrown when count is negative. "Do it!" |> String.replicate 3 Evaluates to "Do it!Do it!Do it!".
Because the description is data with a known meaning, other tools can read it: JSON Schema lowers it, SchemaGen generates values that satisfy it, documentation describes it, and a future solver can reason about it.
You reach this tier by composing built-ins and naming the composition, which covers most real domain invariants. There is no registration API for user-defined interpreted primitives, and no authored string or argument can claim inspectable logic. That restriction is what makes the tier trustworthy: a name proves nothing, and an annotation that nobody checks against the predicate it describes will eventually lie.
Atoms are shape-neutral. Cardinality.Maximum 5 says nothing about text versus lists; the interpreter combines it
with the surrounding schema shape to reach maxLength, maxItems, or maxProperties.
Opaque constraints
Opaque constraints run at runtime but cannot be exported or proved.
let isValidIsbn (value: string) = value.Length = 13 && value.StartsWith "978"
let isbn : Constraint<string> =
Constraint.custom "must be a valid ISBN" isValidIsbn
isValidIsbn: string -> boolvalue: stringstringAn abbreviation for the CLI type . Basic Types
Length: int(=): 'T -> 'T -> boolStructural equality The first parameter. The second parameter. The result of the comparison. 5 = 5 // Evaluates to true 5 = 6 // Evaluates to false [1; 2] = [1; 2] // Evaluates to true (1, 5) = (1, 6) // Evaluates to false
(&&): bool -> bool -> boolBinary 'and'. When used as a binary operator the right hand value is evaluated only on demand The first value. The second value. The result of the operation.
StartsWith: string -> boolisbn: Constraint<string>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
custom: string -> ('value -> bool) -> Constraint<'value>Runs an arbitrary predicate, reporting the supplied prose when it fails. Opaque by construction. It executes and composes normally, may appear in Schema and refinements, and is documented honestly by exporters — but it is invisible to export enforcement and to proof, because an arbitrary host-language closure has no logical meaning to translate. No authored code or argument may claim inspectable logic. let isValidIsbn (isbn: string) = isbn.Length = 13 in Constraint.custom "must be a valid ISBN" isValidIsbn
custom takes a predicate and reports the supplied prose on failure. customWith takes a metadata label first,
then a callback that returns its own violation, for when the failure deserves a structured reason. Its callback is exactly the shape of
Constraint.check applied to a rule, so the usual way to supply one is to reuse a built-in rather than build a
violation by hand:
let supportedCurrencies = [ "USD"; "EUR"; "GBP" ]
let currency : Constraint<string> =
Constraint.customWith "supported currency rule" (Constraint.check (Constraint.oneOf supportedCurrencies))
Constraint.check currency "CAD"
// Error (Atomic (Expected (MembershipAtom (OneOf [ ConstraintValue.Text "USD"; ConstraintValue.Text "EUR"; ConstraintValue.Text "GBP" ]),
// Some (ConstraintValue.Text "CAD"))))
supportedCurrencies: string listcurrency: Constraint<string>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
stringAn abbreviation for the CLI type . Basic Types
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
customWith: string -> ('value -> Result<unit,Violation>) -> Constraint<'value>Runs an arbitrary callback that reports its own violation. Use this when the failure deserves a structured reason a bare predicate cannot give. Because the callback supplies only a violation-returning function, test runs it and discards the error, so a failing test costs whatever the callback allocates. Returning an Expected leaf makes no false portable claim: the enclosing description is still opaque. The callback's shape is exactly Constraint.check applied to a constraint, so the usual way to supply a structured reason is to reuse a built-in rather than build a violation by hand. labels the opaque description; the callback's violation supplies the user-facing failure message. let supported = [ "USD"; "EUR" ] in Constraint.customWith "supported currency rule" (Constraint.check (Constraint.oneOf supported))
check: Constraint<'value> -> 'value -> Result<unit,Violation>Runs a constraint, returning why the value failed. let retryCount = Constraint.between 0 10 42 |> Constraint.check retryCount |> Result.mapError Violation.render
oneOf: 'value seq -> Constraint<'value>Requires the value to equal one of the supplied choices. let currency : Constraint<string> = Constraint.oneOf [ "AUD"; "NZD" ]
The two halves answer different questions. Constraint.inspect currency stays opaque: it reports only the
"supported currency rule" prose, so JSON Schema export, generation, and documentation see nothing of the oneOf
inside. The failure is not opaque — the callback is Constraint.check applied to an interpreted oneOf, so a
failed check returns the interpreted leaf that inner rule produces, and Violation.tryExpectation recovers the
MembershipAtom. An interpreted failure leaf does not make the enclosing rule inspectable: the description stays
opaque, and with it export and proof. Construct a Violation directly only when no built-in states what you mean.
Descriptions are required and must be non-blank, because they are the only thing a renderer has to work with. They
are also, by default, untranslatable, see Custom rules for customLocalized, which lets you
attach your own catalogue key.
Constraint.contramap is opaque for the same reason: an arbitrary projection changes the proposition in a way no
description can express. The inner description is retained beneath the boundary so documentation stays readable, and
an opaque child never erases its interpreted siblings, the rest of the expression stays inspectable.
Negation
Several rules are already negative, and each is a first-class interpreted primitive rather than a complement applied to something else:
| Rule | Negates | Stays interpreted |
|---|---|---|
Constraint.blank |
present |
yes, exact complements for every supported shape |
Constraint.notEqualTo |
equalTo |
yes |
Constraint.noneOf |
oneOf |
yes, exports as a refused enum |
Constraint.notContains |
contains |
yes, exports as a refused contains |
Constraint.notWith |
anything | no, opaque, and requires prose |
Reach for the specific one whenever it says what you mean. A reserved-name rule is noneOf, not a negated oneOf:
let handle : Constraint<string> =
Constraint.noneOf [ "admin"; "root" ]
handle: Constraint<string>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
stringAn abbreviation for the CLI type . Basic Types
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
noneOf: 'value seq -> Constraint<'value>Requires the value to equal none of the supplied choices. A primitive, not a negation: it builds its own atom, so it stays inspectable, exportable, and generatable where Constraint.notWith (Constraint.oneOf …) would be opaque. Use notWith only for rules the catalogue cannot state. let handle : Constraint<string> = Constraint.noneOf [ "admin"; "root" ]
Both run the same predicate, but only the primitive is inspectable: it lowers to JSON Schema, generates, and documents itself, where a negated rule can do none of those.
Why there is no general not
Constraint.notWith is the only general negation, and it requires prose because its failure has no reason to derive:
let isbnPrefixAllowed : Constraint<string> = Constraint.oneOf [ "978-0-"; "978-1-" ]
Constraint.notWith "must not be a supported ISBN prefix" isbnPrefixAllowed
isbnPrefixAllowed: Constraint<string>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
stringAn abbreviation for the CLI type . Basic Types
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
oneOf: 'value seq -> Constraint<'value>Requires the value to equal one of the supplied choices. let currency : Constraint<string> = Constraint.oneOf [ "AUD"; "NZD" ]
notWith: string -> Constraint<'value> -> Constraint<'value>Negates a constraint. The result is opaque: it runs normally but cannot be exported or proved, and reports the supplied prose. The prose is required because there is no honest general complement to derive one from. Membership, format, uniqueness, and numeric families have no complement inside their family; float comparisons are not complementable under NaN, where both x > y and x <= y are false; and a cardinality complement would need bounds this catalogue rejects, such as a maximum of -1. An operation that is sometimes interpreted, sometimes needs prose, and sometimes cannot be constructed is worse than one that is honestly opaque. Constraint.notWith "must not be a reserved name" (Constraint.oneOf [ "admin"; "root" ])
The catalogue could not offer an interpreted not honestly. Format, uniqueness, and the numeric properties have no
complement inside their family. Float comparisons are not complementable under NaN, where both x > y and
x <= y are false. A cardinality complement would need bounds the catalogue rejects, such as a maximum of -1. An
operation that is sometimes interpreted, sometimes needs prose, and sometimes cannot be constructed at all is worse
than one that is honestly opaque, so where a complement is expressible, it is published under its own name in the
table above instead.
Operands Reified cannot describe
Interpreted rules put their comparison value, the operand, into their description, so tools downstream can read
it. That description is a closed data model, ConstraintValue: text, integers, decimals, Booleans, null, and lists of
those. It is deliberately small, because every interpreter has to understand all of it.
A rule can compare values that do not fit. Constraint.atLeast works on anything comparable, and plenty of comparable
types are not in that list:
type Version = { Major: int; Minor: int } // comparable, but not a ConstraintValue
let supportedVersion : Constraint<Version> =
Constraint.atLeast { Major = 2; Minor = 0 }
FsLiveDocsGeneratedPage8_6BB268B4E740.VersionMajor: intintAn abbreviation for the CLI type . Basic Types
Minor: intsupportedVersion: Constraint<Version>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
atLeast: 'value -> Constraint<'value>Requires a value greater than or equal to the supplied bound. let age : Constraint<int> = Constraint.atLeast 13
The rule runs perfectly well. Version compares, so checking a value is exact. What Reified cannot do is convert
{ Major = 2; Minor = 0 } into ConstraintValue, so the description declines to name it:
(Constraint.inspect supportedVersion).Expression
// Opaque (UnsupportedOperand (Relation AtLeast))
Expression: ConstraintExpressionThe constraint's logical form.
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
inspect: Constraint<'value> -> ConstraintDescriptionReturns the constraint's inspectable description. let requiredName : Constraint<string> = Constraint.present (Constraint.inspect requiredName).Expression
supportedVersion: Constraint<Version>This has three consequences:
- Checking is unaffected. The constraint accepts and rejects exactly the values it should.
- Export cannot name the value. JSON Schema, generated documentation, and test-data generation see an opaque rule and say nothing about it, rather than inventing a rendering.
- A derived message cannot print it.
Violation.renderproduces"must be at least the required value", the relation, without the operand.
If that message is not good enough for your users, author the rule with prose instead, and keep the typed check:
let supportedVersionProse : Constraint<Version> =
Constraint.custom "must be version 2.0 or later" (fun value -> value >= { Major = 2; Minor = 0 })
supportedVersionProse: Constraint<Version>Reified.Constraint`1A reusable description of valid values, coupled to the closures that execute it. One constraint value serves direct checking, refined-value admission, Schema, documentation, and export. There is no separate check type: check is the operation, Constraint is the noun. Both closures are retained deliberately. They are not duplicates of one rule: test over a conjunction may stop at the first failing child, while check must run every child to accumulate. Interpreted atoms and custom predicates therefore have a Boolean path that does no violation work, and combinators preserve that property when every child has it. A customWith constraint supplies only a violation-returning callback, so its test runs that callback and discards the error. The description is never interpreted during execution. Closures are composed once, at construction.
FsLiveDocsGeneratedPage8_6BB268B4E740.VersionReified.ConstraintModuleCreates, executes, composes, and inspects constraints.
custom: string -> ('value -> bool) -> Constraint<'value>Runs an arbitrary predicate, reporting the supplied prose when it fails. Opaque by construction. It executes and composes normally, may appear in Schema and refinements, and is documented honestly by exporters — but it is invisible to export enforcement and to proof, because an arbitrary host-language closure has no logical meaning to translate. No authored code or argument may claim inspectable logic. let isValidIsbn (isbn: string) = isbn.Length = 13 in Constraint.custom "must be a valid ISBN" isValidIsbn
value: Version(>=): 'T -> 'T -> boolStructural greater-than-or-equal The first parameter. The second parameter. The result of the comparison. 5 >= 1 // Evaluates to true 5 >= 5 // Evaluates to true [1; 5] >= [1; 6] // Evaluates to false
Major: intMinor: intProse that is not a rule
Constraint.describe attaches documentation:
Constraint.between 0 10
|> Constraint.describe "Retries before the call is abandoned."
Reified.ConstraintModuleCreates, executes, composes, and inspects constraints.
between: 'value -> 'value -> Constraint<'value>Requires a value inside the supplied inclusive bounds. let retryCount : Constraint<int> = Constraint.between 0 10
(|>): 'T1 -> ('T1 -> 'U) -> 'UApply 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
describe: string -> Constraint<'value> -> Constraint<'value>Attaches documentary prose to a constraint. Non-diagnostic: it reaches inspection, documentation, and generated schema prose, but never a violation and never the constraint's logical meaning. Use custom or customWith to change what a failure says. Constraint.between 0 10 |> Constraint.describe "Retries before the call is abandoned."
This reaches inspection and generated schema prose. It never reaches a violation and never changes what the
constraint means. To change what a failure says, author the rule as custom or customWith, there is no message
override, because one would let the reported failure diverge from the description that was published.
Because it never reaches a violation, describe takes no catalogue key and is not localized: it is documentation
about a rule rather than a message to a user, so translating it is a matter of generating the document per locale.
Localization applies to failures, and is covered there.
What export does with each tier
Interpreters divide by what they claim:
- Admission and value generation fail closed.
Schema.parse,Schema.check, refinement creation, and SchemaGen either execute every applicable constraint or report the one they cannot support, with its path. - Trusted structural codecs make no constraint claim at all. They enforce wire shape and construction, and stay outside constraint interpretation entirely.
- Documentation and export degrade honestly. JSON Schema emits every keyword the target really enforces and
retains the rest as readable prose plus
x-reified-runtime-constraintsentries, so a published document never implies a rule is enforced when it is not.
Lowering has three fidelities:
| Fidelity | Meaning | Example |
|---|---|---|
| Exact | the keyword means what the runtime rule means | maxLength, enum, Constraint.email |
| Weakened | the keyword never rejects what the runtime accepts; the exact rule is also retained as runtime metadata | Constraint.present, Constraint.trimmed |
| Runtime-only | no keyword is sound; the rule is retained as metadata alone | an authored Constraint.pattern |
Constraint.present and Constraint.trimmed are weakened rather than exact because blankness
covers a few characters a validator does not. That direction is safe; the reverse would not be, which is why the
blank set is defined to make it impossible.
An authored Constraint.pattern stays runtime-only because the .NET regex dialect is not ECMA-262, \d, for one,
matches any Unicode decimal digit on .NET and only [0-9] under ECMA-262, so publishing an authored pattern could
silently change what it means. Reified's own patterns are written in the common subset and lower exactly:
Constraint.email emits its exact runtime pattern, and Constraint.numeric is defined as ASCII digits for
precisely this reason.
Keywords that JSON Schema allows only once per node are merged rather than duplicated: several excluding rules
become one not: {anyOf: [...]}, and several pattern-shaped rules become one allOf.
SchemaFormat.email is a separate annotation that lowers to format: "email". It makes no validation
claim of its own, and declaring it alongside Constraint.email emits both.