Paradox Documentation

What is Paradox?

Paradox is a domain specification language that compiles to multiple target languages. You define your types, validation rules, and display logic once in .dox files, and Paradox generates correct, idiomatic code for TypeScript, Haskell, Rust, Python, Elixir, C++, OCaml, Scala, C#, Java, SQL, Bash, Nix, JSON, YAML, and a typed AST spec format.

Paradox includes SMT-verified refinement types (powered by Z3), an interactive REPL, a Language Server Protocol implementation, a standard library of algebraic types and collection operations, and a pure functional expression language with pattern matching, interfaces, and higher-order functions.

Key Features

  • Multi-target code generation — Define once, generate for every major language

  • Refinement types — Validation rules verified at compile time via Z3

  • Pure expressions — A functional expression language with pattern matching, lambdas, and recursion

  • Interfaces — Typeclass-style polymorphism with valid, illuminate, and for

  • Interactive REPL — Explore types, generate code, and evaluate expressions interactively

  • Language Server — Hover, completion, go-to-definition, references, formatting, and diagnostics

  • State machines — Define finite state machines with compile-time verification of determinism, reachability, deadlock freedom, coverage, and liveness

  • Standard library — Algebraic types (Either, Maybe, Tuple, These), collection operations, numeric wraps, and function combinators

Quick Example

A simple domain model with validation and display logic:

import std

union Species
  cat
  dog
  horse
  snake

type Pet
  name: Text
  age: Integer
  species: Species

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

illuminate Pet
  name ++ " " ++ age as Text

Generate TypeScript:

$ paradox generate --typescript

Produces typed interfaces, branded wraps, discriminated unions, and validator functions — all from a single .dox source.

Documentation

Language Reference

  • Types — Products, unions, wraps, primitives, composites

  • Expressions — Literals, interpolation, operators, lambdas

  • Functions — Constants, named parameters, higher-order functions

  • Pattern Matching — Match on unions, arrays, sets, optionals

  • Validation — Refinement types, SMT verification, error messages

  • Illumination — Human-readable display logic

  • Interfaces — Typeclass-style polymorphism

  • Modules — Import system and project structure

CLI Reference

Standard Library

  • Overview — What ships with Paradox

  • std — Core interfaces and types

  • numeric — Natural, Positive, Negative, Port types

  • collection — for, reduce, filter, map, zip, and more

  • algebra — Either, Maybe, Tuple, These

  • function — identity, const, compose, flip, and more

  • machine — Finite state machines with compile-time verification

Code Generation

  • Overview — How code generation works

  • TypeScript — Interfaces, branded wraps, validators

  • Haskell — Data types, newtypes, Aeson instances

  • Rust — Structs, enums, mod.rs

  • Python — Dataclasses, package structure

  • Elixir — Structs, typespecs

  • C++ — C++23 namespaced structs, variants

  • OCaml — Records, variant types

  • Scala — Scala 3 case classes, enums

  • C# — C# records, nullable types, System.Text.Json

  • Java — Java records, sealed interfaces

  • SQL — SQLite and PostgreSQL DDL

  • Bash — Shell variable output

  • Nix — Nix attribute sets

  • JSON / YAML — Constant serialization

  • Spec — Typed AST JSON output

Framework Generators

Advanced Topics