Validation

Validation is Paradox’s system for expressing invariants on types. Validation rules are refinement types — constraints that restrict the set of valid inhabitants of a type. Paradox verifies these constraints at compile time using SMT solving (Z3) and generates runtime validators in every target language.

Product Validation

Add constraints to product types with valid:

type Pet
  name: Text
  age: Integer
  species: Species

valid Pet
  name != "" | Pet's gotta have a name
  age > 0 | No such thing as a negative age for a pet

Each line in the valid block is a boolean expression. If the expression is followed by |, the text after the pipe is a custom error message.

Multiple constraints are combined with logical AND — all must hold simultaneously.

Union Validation

Validate specific tags of a union type:

union Status
  approved: Integer
  rejected
  pending

valid Status
  approved: amount. amount > 0 | approved amount must be positive
  rejected: true
  pending: true

Each tag gets its own validation rule. Tags with payloads bind a variable for use in the constraint.

Wrap Validation

Validate the inner value of a wrap type using unwrap:

wrap Natural: Integer

valid Natural
  unwrap >= 0

wrap Positive: Natural

valid Positive
  unwrap as Integer != 0

wrap Port: Natural

valid Port
  unwrap as Integer <= 65535

Wrap validation is the foundation of refinement types in Paradox. The unwrap keyword accesses the inner value, and as casts through the wrap chain.

Match in Validation

Use pattern matching inside validation for field-dependent constraints:

valid Pet
  name != "" | Pet's must have a name
  age > 0 | No such thing as a negative age for a pet
  match address.country:
    usa: species = Species.cat
    _: true
  match species:
    cat: age > 1
    horse: (name as Text) = "tonto"
    dog: true

Match expressions inside valid blocks dispatch on field values, allowing different constraints for different cases.

Implication

The -> operator expresses conditional constraints:

valid Pet
  name = "tonto" -> age > 13

This means: "if the name is tonto, then age must be greater than 13." Implication is equivalent to not a || b — the constraint only applies when the antecedent is true.

Error Messages

Custom error messages follow the | pipe after the constraint expression:

valid User
  first != ""
  last != ""
  age > 18 | Must be an adult

If no error message is provided, a default message is generated from the expression itself.

SMT Verification

Paradox uses Z3 (an SMT solver) to verify validation rules at compile time. This catches two categories of errors:

Overconstrained Types

If constraints are logically contradictory, the type is uninhabitable:

type BadRectangle
  width: Integer
  height: Integer
  area: Integer

valid BadRectangle
  width > 0
  height > 0
  area = width * height
  area < 0

[error 22]: Overconstrained validation for BadRectangle

  12 │ valid BadRectangle
  13 │   width > 0
  14 │   height > 0
  15 │   area = width * height
  16 │   area < 0

     │ Note: These constraints make constructing BadRectangle impossible

The SMT solver proves that no values can satisfy all constraints simultaneously.

Refinement Violations

When constructing a refined type, the value must provably satisfy the constraint:

wrap PositiveInt: Integer

valid PositiveInt
  unwrap > 0

badZero: PositiveInt
  PositiveInt 0

[error 40]: Refinement type constraint violated

   7 │   unwrap > 0 | Must be positive
     •   ╰╸ valid PositiveInt is defined here

  15 │   PositiveInt 0
     •   ╰╸ this value does not satisfy the constraint: unwrap > 0

     │ Hint: The value must satisfy: unwrap > 0

This also catches more subtle violations, like arithmetic that might produce invalid values:

wrap StockCount: Integer

valid StockCount
  unwrap >= 0

decrementStock: current:StockCount. quantity:Integer. StockCount
  StockCount (current.unwrap - quantity)

The SMT solver recognizes that current.unwrap - quantity might be negative, violating the unwrap >= 0 constraint.

Generated Validators

For every type with validation, Paradox generates runtime validator functions in every target language. For example, given:

type Pet
  name: Text
  age: Integer

valid Pet
  name != "" | Pet's gotta have a name
  age > 0

The TypeScript output includes:

export const validPet = (input: unknown): Pet => {
  const _x = input as globalThis.Record<string, unknown>;
  // ... field type checking ...
  const x = input as Pet;
  const errors: string[] = [];
  if (x.name === "") errors.push(`Pet's gotta have a name`);
  if (x.age <= 0) errors.push(`Validation failed: age > 0`);
  if (errors.length > 0) throw new Error(errors.join('; '));
  return x;
}

And the Haskell output:

validPet :: Pet -> Either Text Pet
validPet x =
  let errors = catMaybes
        [ if x.name == "" then Just "Pet's gotta have a name" else Nothing
        , if x.age <= 0 then Just "Validation failed: age > 0" else Nothing
        ]
  in if null errors then Right x else Left (T.intercalate "; " errors)