Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Rex Documentation

Rex (short for Rush Expressions) is a strongly-typed, pure functional language built to be an excellent target for LLM-generated programs, with a focus on data processing. At a high level, you write transformations over lists, records, ADTs, and other values using familiar functional building blocks like map, filter, folds, pattern matching, and composition. The language is designed to make dataflow clear and predictable, with types and pure expressions doing most of the heavy lifting.

Rex is designed first and foremost to be embedded inside Rust applications. In that model, your Rust program acts as the host runtime and injects native functions into Rex so scripts can orchestrate real work while staying in a concise, declarative style. This makes Rex a practical scripting layer for workflow-style systems where you want strong typing and explicit control at the host boundary.

Because Rex programs are pure and free of side effects in the language itself, the runtime can safely execute host-provided async functions in parallel when it is valid to do so. In practice, that means users can write straightforward functional code and still benefit from concurrency without directly managing threads, locks, or low-level async orchestration.

All Rex code samples in this documentation are interactive. Edit them, run them, and use the output to learn by experimentation. A good place to start is the sample below.

If you are using Rex as a code-generation target, read LLMs early. It covers the LLM-first semantic workflow, syntax pitfalls, and validation steps that reduce iteration time.

Try editing and running this intro data-processing demo:

let
  values = [3, 12, 7, 20, 15, 4],
  selected = filter (\n -> n >= 10) values,
  adjusted = map (\n -> n - 2) selected,
  total = foldl (\acc n -> acc + n) 0 adjusted
in
  (values, selected, adjusted, total)

This documentation is organized into several sections:

Rex as a target for LLMs

Rex is the world’s first parallel functional language explicitly designed to be a useful target for LLMs. Its strong static type system gives rapid, high-signal feedback on generated programs, so both users and models can quickly identify mismatches and converge on correct code.

That typechecking loop works especially well with Rex’s functional, expression-oriented style. Because programs are written as pure data transformations, LLM-generated code tends to be easier to inspect, reason about, and refine than imperative scripts with hidden state or side effects.

Together, these properties make Rex a strong fit for LLM-generated data analysis pipelines and scientific workflows. Models can generate high-level orchestration in Rex, while host-provided Rust functions handle domain-specific execution, giving a clean split between deterministic workflow logic and host capabilities.

Rex Tutorial

This tutorial is a guided walk-through of writing Rex code.

All code samples are interactive in the docs, so you can edit and run each snippet as you go.

If you want a compact reference instead, see the Language Reference. For locked semantics and edge cases, see the Specification.

The tutorial is divided into three sections:

Section 1 — Basics

This section covers the fundamental concepts and syntax of the Rex language.

Chapters

  1. Getting Started
  2. Expressions
  3. Let Bindings
  4. Functions
  5. Operators
  6. Collections
  7. Algebraic Data Types
  8. Pattern Matching
  9. Records
  10. Types and Annotations
  11. Debugging and CLI
  12. Prelude Tour

Getting Started

Small Rex programs can be written as one expression, optionally preceded by top-level declarations:

  • type — algebraic data types (ADTs)
  • class / instance — type classes and instances
  • fn — top-level functions

Note: This tutorial focuses on writing Rex code. If you want to embed Rex in Rust, see Embedding.

Running Rex

A runnable Rex file either defines main or ends with a final expression. The examples in this tutorial usually use final expressions because they keep small programs compact.

From this repository, you can run a Rex file:

cargo run -p rex-cli --bin rex -- rex-cli/examples/record_update.rex

Or evaluate a small snippet inline:

cargo run -p rex-cli --bin rex -- -c 'map ((*) 2) [1, 2, 3]'

What you should see

The CLI prints the evaluated value of the program entry point in JSON format. If something fails, you’ll get a parse/type/eval error (often with a span).

What “one expression” means

Even with declarations, a program without main uses the final expression as its result:

fn inc x: i32 -> i32 = x + 1;

let xs = [1, 2, 3] in
  map inc xs

The program above:

  1. Declares a top-level function inc.
  2. Creates a list xs.
  3. Evaluates map inc xs as the program’s result.

Comments

Comments use // ... for line comments and /* ... */ for block comments:

/* This is a comment */
1 + 2

Whitespace

Most whitespace is insignificant, and indentation has no syntactic meaning. Multi-line expressions are often easier to read:

let
  x = 1,
  y = 2
in
  x + y

Commas between let bindings are required. Top-level function declarations end with semicolons, so multi-line bodies do not depend on indentation. The parser also accepts many one-line forms, but multi-line formatting tends to be easier to debug.

Type-class and instance method blocks use explicit braces and semicolon-separated methods:

class Size a where {
  size : a -> i32;
}

An empty marker class or instance uses a semicolon:

class Marker a;
instance Marker i32;

Your first “real” Rex file

Create a file hello.rex:

let
  greet = \name -> "hello, " + name
in
  greet "world"

Run it:

cargo run -p rex-cli --bin rex -- hello.rex

Lambda and Arrow Spelling

Rex uses ASCII-only syntax for lambdas and arrows:

  • \ and ->

The Unicode lambda and right-arrow glyphs are not accepted.

Expressions: Values and Control Flow

Rex is expression-oriented: everything produces a value.

This page introduces the “everyday” expression forms you’ll use constantly.

Literals

( true
, false
, 123
, 3.14
, "hello"
)

Common primitive types are bool, i32, f32, string (plus uuid, datetime if enabled by the host).

Integers vs floats

123 is an integer literal. It can specialize to any Integral type from context, and defaults to i32 when ambiguous. 3.14 is a float literal and defaults to f32.

If you need to force a different numeric type, you can use an annotation (covered later).

( (4 is u8)
, (4 is i64)
, (-3 is i32)
)

Negative numbers

Rex supports negative integer literals:

-420

Negative literals require a signed numeric type. For example, (-3 is u8) is a type error, while (-3 is i16) is valid.

When you’re unsure about parsing, you can always write subtraction explicitly:

0 - 1

If / then / else

if is an expression and must have an else:

let x = 10 in
  if x < 0 then "neg" else "non-neg"

A common mistake

if requires both branches and they must have the same type:

// Not OK: the branches disagree ("string" vs "i32")
if true then "yes" else 0

Equality and comparisons

Comparisons are ordinary functions (usually from the prelude type classes):

( 1 == 2
, 1 != 2
, 1 < 2
, 2 >= 2
)

If you try to compare a type without an Eq / Ord instance, typechecking will fail.

Working with strings

String concatenation uses + (via AdditiveMonoid string):

"Rex " + "rocks"

Because + is type-class-based, the same syntax also works for numeric addition.

Grouping: parentheses are your friend

When in doubt, add parentheses—especially when mixing application and infix operators:

let f = \x -> x + 1 in
  f (1 + 2)

Let Bindings and Scope

let ... in ... introduces local bindings.

Think of let as: “name some sub-expressions so you can reuse them and make types clearer”.

One binding

let x = 1 + 2 in x * 10

Multiple bindings

Bindings can be written on separate lines (typically separated by commas):

let
  x = 1 + 2,
  y = x * 3
in
  (x, y)

Local helper functions

Because functions are values, let is the normal way to define local helpers:

let
  inc = \x -> x + 1,
  double = \x -> x * 2
in
  double (inc 10)

Scope

Bindings are visible only in the in body (and later bindings):

let
  x = 10,
  y = x + 1
in
  y

Recursive bindings

Rex supports writing recursive helpers via let rec. This is the easiest way to write loops:

let rec
  sum = \xs ->
    match xs with {
      case [] -> 0;
      case x::xs -> x + sum xs;
    }
in
  sum [1, 2, 3, 4]

Mutually-recursive helpers use comma-separated bindings:

let rec
  even = \n -> if n == 0 then true else odd (n - 1),
  odd = \n -> if n == 0 then false else even (n - 1)
in
  even 10

Tip: If you’re coming from languages with for loops, think “write a recursive function + match on a list” in Rex.

Let-polymorphism (preview)

Let bindings are generalized (HM let-polymorphism), so one binding can be used at multiple types:

let id = \x -> x in (id 1, id true, id "hi")

This is one of the core reasons to use let: it lets you build small reusable utilities without constantly writing type annotations.

Functions and Lambdas

Functions are values. The most common way to write one is a lambda.

Lambdas

\x -> x + 1

Lambdas can take multiple arguments:

\x y -> x + y

Rex only accepts the ASCII spellings \ and ->.

Annotating lambda parameters

You can annotate parameters when you need to force a specific type:

\(x: i32) -> x + 1

Application

Function application is left-associative:

f x y

is parsed as:

(f x) y

This is why parentheses are important when an argument is itself an application.

Functions returning functions (currying)

let add = \x -> (\y -> x + y) in
  (add 1) 2

Partial application

Because functions are curried, you can supply fewer arguments to get a new function back:

let add1 = (+) 1 in add1 41

Top-level functions (fn)

Top-level functions require parameter types, a return type, and a semicolon terminator. The recommended form puts each parameter name next to its type in the fn header:

fn add x: i32 -> y: i32 -> i32 = x + y;

This declares a function that takes an i32 and returns another function i32 -> i32. The semicolon terminates the top-level declaration, so multi-line bodies do not depend on indentation.

Top-level fn declarations are mutually recursive, so they can reference each other:

fn even n: i32 -> bool =
  if n == 0 then true else odd (n - 1);

fn odd n: i32 -> bool =
  if n == 0 then false else even (n - 1);

even 10

Alternative fn forms

Rex also accepts a parenthesized parameter in the header:

fn inc (x: i32) -> i32 = x + 1;

You can also write the full function type after the function name and provide a lambda body:

fn add : i32 -> i32 -> i32 = \x y -> x + y;

These are equivalent alternatives. The named-parameter header form is recommended because it keeps parameter names and types adjacent to each other.

fn constraints with where

Top-level functions can also have type-class constraints:

fn sum_list xs: List i32 -> i32 where Foldable List = foldl (+) 0 xs;

If you haven’t seen where constraints before, Section 2 covers them in detail.

Operators and Precedence

Operators like + and == are just functions with infix syntax.

Using an operator as a value

Parentheses turn an operator into a function value:

(+) 1 2

This enables partial application:

map ((*) 2) [1, 2, 3]

Operators come from type classes

Many operators are methods on prelude classes:

  • + / zero from AdditiveMonoid
  • * / one from MultiplicativeMonoid
  • == / != from Eq
  • ordering from Ord

This is why you can write + for both numbers and strings.

Precedence

Rex has a fixed precedence table (see Language Reference). A good habit is to use parentheses whenever you mix application with multiple infix operators.

(1 + 2) * 3

Record projection is not an operator

x.field is field projection syntax, not an operator you can partially apply:

type User = User { name: string };

let u: User = User { name = "Ada" } in u.name

Tuples, Lists, and Dictionaries

Rex supports several lightweight data shapes.

Tuples

Tuples group fixed-position values:

(1, "hi", true)

Rex supports tuple patterns in match and let. For indexing, use numeric projection like .0 and .1.

Indexing tuples with .

let t = (1, "hi", true) in t.1

Lists

List literals use square brackets:

[1, 2, 3]

Under the hood, lists are a prelude ADT List a with constructors Empty and Cons.

You can construct cons cells either as Cons h t (normal constructor call style) or with h::t sugar.

let xs = 1::2::3::[] in xs
match [1, 2, 3] with {
  case Empty -> 0;
  case Cons h t -> h;
}

List patterns (sugar)

Rex also supports list-pattern sugar:

match [1, 2, 3] with {
  case [] -> 0;
  case [x] -> x;
  case x::xs -> x;
}

Lists vs Arrays

Rex supports both List a and Array a. They are related, but intentionally different.

  • List a is a linked, recursive ADT (Cons / Empty) and is the default collection shape in user-written Rex code.
  • Array a is a contiguous, indexed runtime container that maps naturally to host memory layouts (for example Rust Vec<T>).

Why both:

  • Lists are ideal for language-level programming patterns (pattern matching, recursive decomposition, and list syntax sugar like [] and x::xs).
  • Arrays are ideal for host interop and performance-sensitive data transfer.

In embedding scenarios, host functions commonly return arrays rather than lists. For example, a Rust host function that returns Vec<i32> is exposed in Rex as returning Array i32.

Matching host results: use to_list

Because list patterns ([], x::xs, Cons) are list-only, convert array results before matching:

let
  /* We use to_array here to simulate a host function result of type Array i32. */
  data = to_array [1, 2, 3]
in
  match (to_list data) with {
    case x::xs -> x;
    case [] -> -1;
  }

The same shape without to_list fails with a type mismatch (array vs list):

let
  /* We use to_array here to simulate a host function result of type Array i32. */
  data = to_array [1, 2, 3]
in
  match data with {
    case x::xs -> x;
    case [] -> -1;
  }

Use the quick fix on the error and choose Convert expression to list with to_list; this rewrites the mismatched expression for you, which is usually all that is needed.

Why to_list is explicit (not implicit)

Rex keeps this conversion explicit for cost visibility. Converting Array a to List a allocates new list nodes and copies references, so it is not a zero-cost operation.

If to_list were implicit, those allocations and copies could be inserted automatically in hot paths (inside loops, repeated matches, pipelines, or nested helper calls) without being obvious in source code. That would increase allocation rate, add GC/heap pressure, and make performance regressions harder to find.

At host boundaries this matters even more: arrays are often used for efficient transfer and memory locality. Keeping to_list explicit ensures the representation change happens only where you choose to pay for it.

LSP and LLM workflow

Because Rex exposes semantic diagnostics and code actions through LSP, an LLM-assisted workflow can fix this in one pass:

  1. Run typecheck / request diagnostics.
  2. Detect the array/list mismatch at the match expression.
  3. Apply the to_list quick fix code action.
  4. Re-check and continue.

This is stronger than raw text editing because the fix is selected from compiler-semantic information (actual inferred/expected types and targeted edits), not guessed from surface syntax.

Dictionaries (records / dict values)

Dictionary literals use braces:

{ a = 1, b = 2 }

These are “record-like” values. Depending on context they may be treated as a record type ({ a: i32, b: i32 }) or as a dictionary-like value; either way, you can project fields when the field is known to exist:

type R = R { a: i32, b: i32 };

let r: R = R { a = 1, b = 2 } in r.a

Forcing a dictionary type

If you want a polymorphic “dictionary” (instead of a specific record type), use type ascription with is:

({ a = 1, b = 2 }) is Dict i32

Matching dictionaries

Dictionary patterns check for key presence and bind those keys to variables:

let d = ({ a = 1, b = 2 }) is Dict i32 in
match d with {
  case {a, b} -> a + b;
  case {a} -> a;
  case {} -> 0;
}

{} is useful as a fallback: it requires no keys, so it matches any dict.

Algebraic Data Types (ADTs)

ADTs let you define your own sum types. Top-level type declarations end with semicolons.

You’ll use ADTs to model “this or that” choices: optional values, tagged unions, trees, results, etc.

Simple ADT

type Maybe a = Just a | Nothing;

Constructors are values:

type Maybe a = Just a | Nothing;

let v = Just 1 in
  (v, Nothing)

Using ADTs is all about match

Defining an ADT is only half the story; consuming it is done with pattern matching:

type Maybe a = Just a | Nothing;

let
  fromMaybe = \d m ->
    match m with {
      case Just x -> x;
      case Nothing -> d;
    }
in
  fromMaybe 0 (Just 5)

Constructors with multiple fields

type Pair a b = Pair a b;

let v = Pair 1 "hi" in
  v

This is a single-constructor ADT (a “product type”). In many programs you’ll use record-carrying constructors instead because they self-document field names.

Record-carrying constructors

Variants can carry a record payload:

type User = User { name: string, age: i32 };

let u = User { name = "Ada", age = 36 } in
  u

This style works well with field projection and update (covered later).

Multi-variant and recursive ADTs

You can define sum types with multiple constructors, including recursive ones:

type Tree
  = Leaf { value: i32 }
  | Node { left: Tree, right: Tree };

Recursive ADTs are the foundation for ASTs, expression trees, and many structured data problems.

Pattern Matching with match

Use match to branch on the shape of values.

match is the “workhorse” control flow construct in Rex. You’ll use it for:

  • consuming ADTs (Option, Result, your own types),
  • splitting lists ([] vs x::xs),
  • checking key presence in dicts ({a, b}),
  • refining record-carrying variants so projection/update typecheck.

Matching ADTs

type Maybe a = Just a | Nothing;

let fromMaybe = \d m ->
  match m with {
    case Just x -> x;
    case Nothing -> d;
  }
in
  fromMaybe 0 (Just 5)

Rex checks matches for exhaustiveness on ADTs and reports missing constructors.

Inline match syntax

You’ll often see compact “inline” matches in examples:

match (Some 1) with { case Some x -> x; case None -> 0; }

Common patterns

Wildcards:

match [1, 2, 3] with {
  case Empty -> 0;
  case Cons _ _ -> 1;
}

List patterns:

match [1, 2] with {
  case [] -> 0;
  case [x] -> x;
  case [x, y] -> x + y;
  case _ -> 0;
}

Cons patterns:

match [1, 2, 3] with {
  case h::t -> h;
  case [] -> 0;
}

h::t is equivalent to Cons h t; both expression forms are valid.

Record patterns on record-carrying constructors:

type Point = Point { x: i32, y: i32 };

let p = Point { x = 1, y = 2 } in
match p with {
  case Point { x: x, y: y } -> x + y;
}

Dict key presence patterns:

let d = ({ a = 1, b = 2 }) is Dict i32 in
match d with {
  case {a, b} -> a + b;
  case {a} -> a;
  case {} -> 0;
}

Arrow spelling

Match arms use ->:

type Bit = T | F;

let v = T in
match v with {
  case T -> 1;
  case F -> 0;
}

Ordering and fallbacks

Match arms are tried top-to-bottom. Put specific patterns first and broad patterns (like _ or {}) last.

Records: Projection and Update

Records are key/value structures with named fields. Rex supports:

  • field projection: base.field
  • record update: { base with { field = expr } }

At the value level, “record” literals are written like dicts:

{ x = 1, y = 2 }

At the type level, record types are written with ::

let p: { x: i32, y: i32 } = { x = 1, y = 2 } in
  p

Projection

type Point = Point { x: i32, y: i32 };

let p: Point = Point { x = 1, y = 2 } in p.x

Projection is accepted when the field is definitely available on the type (see Specification).

Tip: If you get a “field not definitely available” type error, it usually means the typechecker can’t prove which ADT variant you have. A match often fixes it.

Update

type Point = Point { x: i32, y: i32 };

let p: Point = Point { x = 1, y = 2 } in
  { p with { x = p.x + 10 } }

Updates can set multiple fields at once:

type Point = Point { x: i32, y: i32 };

let p: Point = Point { x = 1, y = 2 } in
  { p with { x = 100, y = 200 } }

Updating record-carrying ADT variants

This is a common pattern:

type Sum = A { x: i32 } | B { x: i32 };

let s: Sum = A { x = 1 } in
match s with {
  case A {x} -> { s with { x = x + 1 } };
  case B {x} -> { s with { x = x + 2 } };
}

The match arms refine which constructor s has, allowing the update to typecheck.

Types and Annotations

Rex uses Hindley–Milner type inference, but you can (and often should) add annotations.

This page is about the “tools” you use to make types explicit when inference isn’t enough.

Type names

Examples of primitive and constructed types:

  • bool, i32, f32, string
  • (a, b) for tuples
  • List a, Option a, Promise a, Result a e (prelude/built-in constructors)

Lowercase names in type positions are type parameters only after a surrounding form declares them:

fn id<a> x: a -> a = x;

id 1

The same rule applies to let, declare fn, class methods, and instances:

let id<a>: a -> a = \x -> x in id "hello"

Function types are right-associative:

i32 -> i32 -> i32

means:

i32 -> (i32 -> i32)

Record types

Record types use ::

{ x: i32, y: i32 }

Record values use =:

{ x = 1, y = 2 }

Let annotations

let x: i32 = 1 in x

Lambda parameter annotations

\(x: i32) -> x + 1

Annotating expressions

You can also annotate via a let-binding when you want to force a particular type:

let xs: List i32 = [1, 2, 3] in xs

Type ascription with is

Rex also supports an expression-level “ascription” form:

({ a = 1, b = 2 }) is Dict i32

You’ll see is used in examples for two common reasons:

  1. To force a dictionary type (Dict a) instead of a specific record type.
  2. To disambiguate overloaded values (similar to adding a let-annotation).

Warning: Use is when it helps clarity, but don’t overuse it: most of the time, simple let annotations are easier to read.

Debugging: CLI Tips and Common Errors

Rex is prepared and evaluated in stages:

  1. Parsing
  2. Import/declaration preparation
  3. Type inference / checking
  4. Evaluation

Most debugging is about figuring out which stage is failing and adding just enough information to make the problem obvious.

Useful CLI flags

Run a Rex file:

cargo run -p rex-cli --bin rex -- path/to/file.rex

Run a file with JSON inputs for its entry point:

cargo run -p rex-cli --bin rex -- path/to/program.rex --inputs path/to/inputs.json

The inputs file is a top-level JSON object. Each field name must match a parameter of main; runnable files without main use their final expression and have the empty input shape {}.

Inspect the entry point type metadata:

cargo run -p rex-cli --bin rex -- path/to/program.rex --manifest

Run an inline snippet:

cargo run -p rex-cli --bin rex -- -c 'let x = 1 in x + 2'

Show the parsed AST and exit:

cargo run -p rex-cli --bin rex -- --emit-ast -c '1 + 2'

Show the entry point result type and exit:

cargo run -p rex-cli --bin rex -- --emit-type -c 'map ((*) 2) [1, 2, 3]'

Print a string result without JSON quotes:

cargo run -p rex-cli --bin rex -- --raw-output -c '"hello"'

“Parse error”: start small

If you hit a parse error:

  1. Reduce the program to the smallest failing snippet.
  2. Add parentheses to disambiguate application vs infix operators.
  3. Prefer multi-line let/match while debugging.

“Missing typeclass impl”

This usually means you called a type-class method at a type that has no instance.

Typical fixes:

  • use a different type (List vs Array, Option vs Result, …),
  • add an instance (Section 2),
  • add a type annotation so the intended instance is selected.

“Ambiguous overload”

This happens when an overloaded value doesn’t have enough information to pick an instance.

Typical fixes:

  • add a let-annotation: let z: i32 = zero in z
  • add is ascription: (zero) is i32 (if you prefer expression ascription style)
  • use the value in a context that forces a type (e.g. zero + 1).

The exact defaulting rules are described in Specification.

A Tour of the Prelude

Rex ships with a small “prelude” of standard types, type classes, and instances.

The source of truth in this repository is:

  • type classes + instances: rex-engine/src/prelude/typeclasses.rex
  • runtime builtins + helper wiring: rex-engine/src/prelude/mod.rs
  • standard type-system construction: rex-engine/src/prelude/type_system.rs

This page is a guided map so you know what to reach for while writing Rex.

Core data types

These are available by default:

  • List a (with constructors Empty and Cons)
  • Option a (constructors Some and None)
  • Result a e (constructors Err and Ok)
  • Array a
  • Dict a

Core classes (selected)

Numeric-like classes

  • AdditiveMonoid a (zero, +)
  • MultiplicativeMonoid a (one, *)
  • Ring a, Field a, Integral a (and friends)

Equality and ordering

  • Eq a (==, !=)
  • Ord a (cmp, <, <=, >, >=)
  • Default a (default)

Default gives you a value-level default for a type. It is separate from Rex’s defaulting pass, which resolves ambiguous type variables for defaultable classes.

Collections and effects

  • Functor f (map)
  • Applicative f (pure, ap)
  • Monad m (bind)
  • Foldable t (foldl, foldr, fold)
  • Filterable f (filter, filter_map)
  • Sequence f (take, skip, zip, unzip)
  • Indexable t a (get)

For tuples, use numeric projection like .0 and .1 instead of get.

A few useful helper functions

The prelude also exposes some generic helpers (type-class-based):

  • sum, mean, count, min, max
  • is_some, is_none (for Option)
  • is_ok, is_err (for Result)

How to learn what something is

When you see an unfamiliar function:

  1. Ask the CLI for its type: cargo run -p rex-cli --bin rex -- --emit-type -c 'the_name'
  2. If it’s a type-class method, find the class in rex-engine/src/prelude/typeclasses.rex
  3. If it’s a Rust-backed helper or primitive, find the runtime wiring in rex-engine/src/prelude/mod.rs

This workflow is especially helpful when you’re building your own abstractions.

Section 2 — Advanced Topics

This section covers advanced type system features, polymorphism, and functional programming patterns.

Chapters

  1. Type Inference
  2. Polymorphism
  3. Typeclasses
  4. Instances
  5. Constraints and Where
  6. Resolution and Coherence
  7. Functor
  8. Applicative
  9. Monad
  10. Writing Instances
  11. Defaulting
  12. Higher-Kinded Types

Type Inference (Hindley–Milner)

Rex infers types for most expressions. You get type errors when constraints can’t be satisfied or when the program would require ambiguous instance selection.

This section is intentionally practical: it’s about recognizing when the typechecker needs help, and what kinds of help work best.

A simple inference example

\x -> x

This is polymorphic: it can be used at any type (a -> a).

Try it

Ask the CLI for the type:

cargo run -p rex-cli --bin rex -- --emit-type -c '\\x -> x'

Inference plus operators

\x -> x + 1

This adds constraints (here, a numeric type class for +).

What changed?

The expression no longer works at “any type” because + only exists for types with an AdditiveMonoid instance (numbers and strings in the prelude).

When inference fails

You’ll see errors when:

  • branches of an if don’t match types,
  • you call a type-class method with no applicable instance,
  • you use an overloaded value without enough type information (ambiguity).

For details on ambiguity and defaulting, see Specification.

The most common “fixes”

  1. Add a type annotation to a let binding.
  2. Use expression ascription with is.
  3. Restructure code so an argument forces a type (e.g. apply a polymorphic function).

Polymorphism and Let-Generalization

The most visible “HM feature” in Rex is that let bindings can be reused at multiple types.

If you’re new to HM languages, this is the big shift from “everything has one type” to “some definitions are generic”.

A polymorphic helper

let id = \x -> x in
  (id 1, id true, id "hi")

Why lambdas aren’t generalized

Inside a lambda body, parameters are monomorphic unless you explicitly abstract:

\f ->
  let x = f 1 in
    f x

If f were required to work at multiple unrelated types, that would be rejected.

Practical implication

If you want something reusable, let-bind it at the outer level:

let
  id = \x -> x,
  use = \x -> (id x, id x)
in
  use 1

Practical tip

If a definition should be reusable, prefer let-binding it and giving it a clear name (and often a type annotation).

In practice, you’ll use:

  • let for reusable helpers,
  • lambdas for “inline glue” (callbacks passed to map, foldl, bind, …),
  • fn for API-like top-level functions with stable signatures.

Type Classes: Defining Overloads

Type classes define a set of operations that can be implemented for many types.

Rex type classes are similar to Haskell’s: they are compile-time constraints with runtime dictionary resolution.

Defining a class

class Size a where {
  size : a -> i32;
}

Method signatures can mention the class parameter a and any other types in scope.

Empty Classes

Classes with methods use where { ... }. Marker classes with no methods use a semicolon:

class Marker a;

Operators as methods

class Eq a where {
  == : a -> a -> bool;
  != : a -> a -> bool;
}

Superclasses

Superclasses use <= (read “requires”):

class Ord a <= Eq a where {
  < : a -> a -> bool;
}

If you have an Ord a, you also must have an Eq a instance.

Multi-parameter classes (tupled)

Some prelude classes logically take multiple type parameters, such as Indexable t a.

In Rex source you write:

class Indexable t a where {
  get : i32 -> t -> a;
}

In where constraints, multi-parameter classes are written using a tuple:

where Indexable (t, a) -> ...

This matches the implementation model described in Specification.

Instances: Implementing Type Classes

Instances attach method implementations to a concrete “head” type.

An instance has three parts:

  1. The class name (Show, Size, Functor, …)
  2. The instance head type (what you’re implementing it for)
  3. An optional instance context (<= ...) of required constraints

A monomorphic instance

class Show a where {
  show : a -> string;
}
instance Show i32 where {
  show = \_ -> "<i32>";
}

Class names in instance headers can be module-qualified when imported via alias:

import dep as D;

instance D.Show i32 where {
  show = \_ -> "<i32>";
}

A polymorphic instance with context

Instance contexts use <=:

instance<a> Show (List a) <= Show a where {
  show = \xs ->
    let
      step = \out x ->
        if out == "["
          then out + show x
          else out + ", " + show x,
      out = foldl step "[" xs
    in
      out + "]";
}

Read this as: “Show (List a) exists as long as Show a exists”.

Why the context matters

Inside show for lists, we call show x. That requires Show a, so we must list it in the instance context.

Non-overlap (coherence)

Rex rejects overlapping instance heads for the same class. This keeps method lookup deterministic.

In practical terms: you can’t have two different Show (List a) instances in scope at once.

Constraints and where

Sometimes a function is only valid when certain type-class constraints hold. In Rex you’ll see those constraints in type signatures (for fn) and in where clauses (commonly for lambdas).

Constrained lambdas

This example is from rex-cli/examples/type_classes.rex:

let
  use_classes<t,f,a> =
    \ (x: t) (y: f a) (z: a) where Indexable (t, a), Foldable f ->
    let
      first = get 0 x,
      total = foldl (\acc _ -> acc) z y
    in
      (first, total, z)
in
  let result: (i32, i32, i32) = use_classes [10, 20, 30] [1, 2, 3] 0 in result

Notes:

  • where ... -> attaches constraints to the lambda.
  • Multi-parameter classes like Indexable t a are written as Indexable (t, a) in the where list (internally they’re represented as tupled predicates).
  • Constraints can use module-qualified class names when imported via alias (for example where M.ClassName t -> ...).

Constrained top-level functions

Top-level functions can also have a where clause:

fn sum_list : List i32 -> i32 where Foldable List = \xs -> foldl (+) 0 xs;

Constraints appear after the type signature and before =.

Multiple constraints

Constraints are comma-separated:

fn demo : List i32 -> i32 where Foldable List, AdditiveMonoid i32 = \xs -> foldl (+) 0 xs;

Note: In many cases you don’t need to write constraints for concrete prelude types (List, Option, etc.) because the argument type already forces instance selection. where becomes more important when you want polymorphic constraints (e.g. “for any f with Foldable f”).

Resolution, Coherence, and Ambiguity

Type-class methods in Rex are resolved based on the inferred type at the call site.

This page answers “why did the typechecker complain?” when you’re using overloaded methods.

Coherence: why overlap is rejected

If two instances could match the same call, the runtime wouldn’t know which method to pick. Rex rejects such overlaps per class.

Deferred resolution for function values

Rex can keep an overloaded function value around and resolve it later when you apply it:

let f = map ((+) 1) in
  ( f [1, 2, 3]
  , f (Some 41)
  )

Here map is a Functor method. The engine picks the right map implementation when it sees the argument type (List i32 vs Option i32).

Why this works

map ((+) 1) is still a function, so Rex can defer selecting the Functor instance until the function is applied to a concrete container.

Ambiguity for non-function values

If you use an overloaded method as a non-function value and the type is not determined, resolution can be ambiguous and Rex will error.

For example, pure 1 is ambiguous by itself because it could be List i32, Option i32, Array i32, Result i32 e, etc.

Fix it by forcing a type:

let x: Option i32 = pure 1 in x

For the exact rules, see Specification (“Type Classes: Coherence, Resolution, and Ambiguity”).

Functors

The prelude defines:

class Functor f where {
  map<a,b> : (a -> b) -> f a -> f b;
}

map applies a pure function inside a container f.

If you can describe an operation as “change the values without changing the structure”, it’s a good fit for map.

Mapping over lists

map ((*) 2) [1, 2, 3]

Mental model

Each element is transformed independently; list length stays the same.

Mapping over Option

( map ((+) 1) (Some 41)
, map ((+) 1) None
)

None acts like “no value to transform”.

Mapping over Result

( map ((*) 2) (Ok 21)
, map ((*) 2) (Err "boom")
)

map transforms Ok values but leaves Err unchanged.

A useful pattern: composing transforms

Instead of branching on shapes early, keep your code “in the functor”:

let inc = \x -> x + 1 in
  map inc (Some 1)

Applicatives

An Applicative is a Functor that can inject values and apply wrapped functions:

class Applicative f <= Functor f where {
  pure<a> : a -> f a;
  ap<a,b> : f (a -> b) -> f a -> f b;
}

Applicatives are great when you want to combine independent computations that live “in a container”.

pure

let x: Option i32 = pure 1 in x

The type depends on context. For example, this forces Option:

let x: Option i32 = pure 1 in x

A common pattern: building up computations

Because functions are curried, you can apply step-by-step. For Option:

ap (ap (pure (\x y -> x + y)) (Some 1)) (Some 2)

ap with Option

ap (Some ((+) 1)) (Some 41)

If either side is “missing”, the result is missing:

( ap None (Some 1)
, ap (Some ((+) 1)) None
)

Applicative style

You can build up multi-argument computations by applying step-by-step:

ap (ap (pure (\x y -> x + y)) (Some 1)) (Some 2)

Monads

Monads are about sequencing computations where the next step depends on the previous result.

In Rex, the core monad operation is bind:

class Monad m <= Applicative m where {
  bind<a,b> : (a -> m b) -> m a -> m b;
}

Note the argument order: function first, then the monadic value.

If you come from Haskell: Rex’s bind corresponds to (>>=) but with the arguments flipped.

Option as a Monad

let
  safe_inc = \x -> Some (x + 1),
  step = \x -> bind safe_inc x
in
  step (Some 1)

More realistically, you inline the next step:

bind (\x -> Some (x + 1)) (Some 41)

Why monads matter

With Option, monadic sequencing means “stop early if something is missing” without deeply nested match expressions.

Result as a Monad

Result a e is useful for short-circuiting on the first Err:

let
  ok = Ok 1,
  boom = Err "boom"
in
  ( bind (\x -> Ok (x + 1)) ok
  , bind (\x -> Ok (x + 1)) boom
  )

“Do notation” without syntax

Rex doesn’t require special syntax. You can write sequencing explicitly with bind and lambdas:

bind (\x ->
  bind (\y ->
    pure (x + y)
  ) (Some 2)
) (Some 1)

Tip: When your bind chains get hard to read, consider extracting the steps into named let bindings.

For example, the same logic with named steps:

let
  add_x_y = \x y -> pure (x + y),
  step_y = \x -> bind (add_x_y x) (Some 2),
  run = \mx -> bind step_y mx
in
  run (Some 1)

Writing Your Own Instances (Including Functor/Applicative/Monad)

This page is a hands-on guide to defining your own instances for custom ADTs.

We’ll build a tiny container type and give it Functor, Applicative, and Monad instances.

Note: Functor, Applicative, and Monad are provided by the Rex prelude. The examples below assume those classes already exist (so we only write type/instance).

Step 1: define a container ADT

type Box a = Box a;

This is a single-variant ADT that “wraps” a value.

Step 2: make it a Functor

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}

Now you can:

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}
map ((+) 1) (Box 41)

Step 3: make it an Applicative

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}
instance Applicative Box <= Functor Box where {
  pure = \x -> Box x;
  ap = \bf bx ->
    match bf with {
      case Box f -> map f bx;
    };
}

Try:

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}
instance Applicative Box <= Functor Box where {
  pure = \x -> Box x;
  ap = \bf bx ->
    match bf with {
      case Box f -> map f bx;
    };
}
ap (Box ((*) 2)) (Box 21)

Step 4: make it a Monad

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}
instance Applicative Box <= Functor Box where {
  pure = \x -> Box x;
  ap = \bf bx ->
    match bf with {
      case Box f -> map f bx;
    };
}
instance Monad Box <= Applicative Box where {
  bind = \f bx ->
    match bx with {
      case Box x -> f x;
    };
}

Try:

type Box a = Box a;

instance Functor Box where {
  map = \f bx ->
    match bx with {
      case Box x -> Box (f x);
    };
}
instance Applicative Box <= Functor Box where {
  pure = \x -> Box x;
  ap = \bf bx ->
    match bf with {
      case Box f -> map f bx;
    };
}
instance Monad Box <= Applicative Box where {
  bind = \f bx ->
    match bx with {
      case Box x -> f x;
    };
}
bind (\x -> Box (x + 1)) (Box 41)

Common pitfalls

  • Overlapping instances: Rex rejects overlap for the same class; keep instance heads distinct.
  • Missing context constraints: if your method body calls another overloaded method, you often need to list the required class in the instance context.
  • Wrong argument order for bind: Rex’s bind is (a -> m b) first, then m a.

Default: Typeclass and Defaulting

In Rex, “default” can mean two different things:

  • The Default typeclass method default : a
  • The defaulting pass that resolves ambiguous type variables for defaultable classes

1) Default Typeclass (default : a)

The prelude provides Default and a set of built-in instances.

Built-in types with Default:

  • bool
  • u8, u16, u32, u64
  • i8, i16, i32, i64
  • f32, f64
  • string
  • List a
  • Array a
  • Option a
  • Result a e (when Default a is available)

Implementing Default for custom ADTs

You can implement Default for many ADT shapes.

Single constructor with unnamed fields:

type Pair = Pair i32 bool;

instance Default Pair where {
    default = Pair 42 true;
}

Single constructor with named fields:

type Config = Config { retries: i32, enabled: bool };

instance Default Config where {
    default = Config { retries = 3, enabled = false };
}

Multiple variants (enum) with no fields:

type Mode = Fast | Safe | Debug;

instance Default Mode where {
    default = Safe;
}

Multiple variants with mixed payload shapes:

type Token = Eof | IntLit i32 | Meta { line: i32, col: i32 };

instance Default Token where {
    default = Meta { line = 1, col = 1 };
}

Generic ADTs with constraints:

type Box a = Box a | Missing;

instance<a> Default (Box a) <= Default a where {
    default = Box default;
}

Ambiguous default calls and is

When multiple Default instances are in scope, default may be ambiguous until you pin the type. Record updates require a definitely known base type.

Failing example:

type A = A { x: i32, y: i32 };
type B = B { x: i32, y: i32 };

instance Default A where {
    default = A { x = 1, y = 2 };
}
instance Default B where {
    default = B { x = 10, y = 20 };
}
{ default with { x = 9 } }

In the editor/playground, use the quick fix on this error to insert is for the intended ADT. Try it on the example above.

Passing example (same setup, with explicit is):

type A = A { x: i32, y: i32 };
type B = B { x: i32, y: i32 };

instance Default A where {
    default = A { x = 1, y = 2 };
}
instance Default B where {
    default = B { x = 10, y = 20 };
}
{ (default is A) with { x = 9 } }

Another failing example (same ambiguity in a let binding):

type A = A { x: i32, y: i32 };
type B = B { x: i32, y: i32 };

instance Default A where {
    default = A { x = 1, y = 2 };
}
instance Default B where {
    default = B { x = 10, y = 20 };
}
let
    a = { default with { x = 9 } },
    b = { default with { y = 8 } }
in
    (a, b)

For this let-binding form, quick fixes offer two styles: add is to the default call, or add a type annotation on the binding (for example a: A = ...). These same quick fixes are also exposed through LSP code actions and can be used by LLM-driven tooling.

2) Type Defaulting (Ambiguous Types)

Some overloaded prelude operations (such as zero) only require class constraints:

zero

If nothing else forces a concrete type, Rex runs defaulting to pick a concrete type from the defaulting candidates that satisfy the required class constraints.

If you see an “ambiguous overload” error around numeric expressions, force a type:

let z: i32 = zero in z

Or use the value in a way that constrains it:

zero + 1

Integer literals are also overloaded (over Integral) and become concrete from context:

let
  x = 4,
  f: u16 -> u16 = \n -> n
in
  f x

Negative literals must resolve to a signed type:

let
  x: i32 = -3,
  f: i32 -> i32 = \n -> n
in
  f x

let x: u32 = -3 in x is a type error.

The defaulting algorithm is specified in Specification (“Defaulting”).

Higher-Kinded Types (and Partial Application)

This page explains the “advanced” type shape behind Functor, Applicative, and Monad.

What is a “type constructor”?

Some types take type parameters:

  • List a
  • Option a
  • Promise a
  • Result a e

The bare names List, Option, and Promise are type constructors (they still need an a).

In informal kind notation:

  • List : * -> *
  • Option : * -> *
  • Promise : * -> *
  • Result : * -> * -> *

Why Functor talks about f a

The class is defined as:

class Functor f where {
  map<a,b> : (a -> b) -> f a -> f b;
}

f here stands for a unary type constructor like List, Option, or Promise.

Result is binary — so how can it be a Functor?

The prelude has an instance:

instance<e> Functor (Result e) where {
  map = prim_map;
}

Result e means: “fix the error type to e, leaving one type parameter for the Ok value”. Written fully (with both parameters), that’s Result a e.

So Result e behaves like a unary type constructor:

  • Result a e is “a result with Ok type a and Err type e
  • map transforms the Ok value and leaves Err alone

Recognizing partial application in types

Whenever you see something like (Result e) or (Either e) in other languages, think:

“We pinned one type parameter to turn a multi-parameter type into a unary constructor.”

This idea shows up again for Applicative (Result e) and Monad (Result e).

Section 3 — Worked Examples

These examples are interactive in the docs: edit and run them directly on each page.

Tip: You can also run many examples inline with:

cargo run -p rex-cli --bin rex -- -c '<paste rex expression here>'

For larger multi-line experiments, saving to a .rex file is often easier.

Chapters

  1. Lists
  2. Folds
  3. Match and ADTs
  4. Records
  5. Functor Polymorphism
  6. Option Pipelines
  7. Result Workflows
  8. Custom Show Printing
  9. Custom Size
  10. Indexable
  11. Small Standard Module
  12. Mini Project

Example: List Basics

This page is a hand-held tour of the most common list workflow in Rex:

  • start with a list value
  • transform it with map
  • keep only what you want with filter
  • (optionally) reduce it with foldl (see the next page)

If you’re new to functional programming, think of map as “for each element, compute a new element”, and filter as “keep only elements where the predicate is true”.

Goal

Take a list of integers and produce new lists by applying simple rules (double, keep even, increment).

The simplest transform

Double everything

map ((*) 2) [1, 2, 3, 4]

What to notice

  • map comes from Functor List.
  • (*) is just a function; ((*) 2) is a partially applied function.

Step-by-step: naming intermediate values

The one-liner above is idiomatic, but while learning it helps to name each step:

let
  xs = [1, 2, 3, 4],
  doubled = map ((*) 2) xs
in
  doubled

This style also makes it easier to debug by temporarily returning an intermediate.

Filter then map

Filtering needs a predicate a -> bool. Let’s define one:

let
  is_even = \x -> (x % 2) == 0
in
  filter is_even [1, 2, 3, 4, 5, 6]

Now combine filter and map:

let
  xs = [1, 2, 3, 4, 5, 6],
  is_even = \x -> (x % 2) == 0
in
  map ((+) 1) (filter is_even xs)

Variations

Try changing the predicate to keep odd numbers instead:

let is_odd = \x -> (x % 2) != 0 in filter is_odd [1, 2, 3, 4, 5, 6]

Common beginner mistake: missing parentheses

Because application is left-associative, nesting calls without parentheses does not do what you want. Prefer:

let
  xs = [1, 2, 3, 4, 5, 6],
  is_even = \x -> (x % 2) == 0
in
  map ((+) 1) (filter is_even xs)

over trying to “read it as English” without grouping.

Worked examples

Example: triple_then_keep_big

Problem: triple each element, then keep only elements greater than 10.

let
  xs = [1, 2, 3, 4, 5],
  tripled = map ((*) 3) xs
in
  filter (\x -> x > 10) tripled

Why this works: map ((*) 3) transforms each element first, then filter keeps only values that pass the predicate.

Example: between lo hi x with filter

Problem: keep only values in an inclusive range.

let
  between = \lo hi x -> x >= lo && x <= hi
in
  filter (between 3 5) [1, 2, 3, 4, 5, 6]

Why this works: between 3 5 is a predicate function i32 -> bool, which is exactly what filter expects.

Example: naming inc in let

Problem: replace ((+) 1) with a named helper.

let
  inc = \x -> x + 1
in
  map inc [1, 2, 3, 4]

Why this works: inc has type i32 -> i32, so it can be passed directly to map.

Example: Folding

Foldable gives you foldl and foldr-style iteration.

If map changes values, folds reduce a collection down to a single result.

Goal

Learn to take a list and reduce it to:

  • a number (sum, product, count)
  • a string (joining)

A mental model: accumulator + step

foldl has the shape:

foldl : (b -> a -> b) -> b -> t a -> b

Read it as:

  1. Start with an accumulator of type b
  2. For each element of type a, update the accumulator
  3. Return the final accumulator

Sum a list

foldl (+) 0 [1, 2, 3, 4]

How to read it

  • Start with accumulator 0
  • For each element, add it to the accumulator
  • Return the final accumulator

The same thing, spelled out

let
  step = \acc x -> acc + x
in
  foldl step 0 [1, 2, 3, 4]

When debugging, spelling out step makes it easier to reason about types.

Build a string

let
  step = \out x ->
    if out == "" then x else out + ", " + x
in
  foldl step "" ["a", "b", "c"]

Worked example: bracketed join

Problem: join strings with commas and wrap the result in brackets.

let
  step = \out x ->
    if out == "" then x else out + ", " + x,
  joined = foldl step "" ["a", "b", "c"]
in
  "[" + joined + "]"

Why this works: the fold builds "a, b, c" from left to right, then the final expression adds the outer brackets.

Using folds to compute “length”

You can compute list length by ignoring elements and incrementing a counter:

foldl (\n _ -> n + 1) 0 [10, 20, 30, 40]

When to prefer match recursion vs foldl

Both are fine. Rules of thumb:

  • Use foldl when you’re “reducing” to a single value (sum, count, join).
  • Use explicit match recursion when you need more complex control flow.

Worked examples

Example: product with foldl

Problem: multiply all numbers in a list, starting from 1.

foldl (*) 1 [2, 3, 4]

Why this works: 1 is the multiplicative identity, so each element is accumulated by multiplication.

Example: all over booleans

Problem: check whether every boolean in a list is true.

let
  all = \xs -> foldl (\acc x -> acc && x) true xs
in
  (all [true, true, true], all [true, false, true])

Why this works: once acc becomes false, acc && x stays false for the rest of the fold.

Example: any over booleans

Problem: check whether at least one boolean in a list is true.

let
  any = \xs -> foldl (\acc x -> acc || x) false xs
in
  (any [false, false, true], any [false, false, false])

Why this works: the accumulator starts false and flips to true as soon as any element is true.

Example: ADTs + match

This example shows the usual pattern:

  1. define an ADT
  2. consume it with match

Goal

Build a tiny “Maybe” API:

  • fromMaybe (extract with default)
  • mapMaybe (transform inside Just)
  • isJust (check which constructor you have)

Define an ADT

type Maybe a = Just a | Nothing;

Use it

type Maybe a = Just a | Nothing;

let
  fromMaybe = \d m ->
    match m with {
      case Just x -> x;
      case Nothing -> d;
    }
in
  ( fromMaybe 0 (Just 5)
  , fromMaybe 0 Nothing
  )

Next steps

The next example implements mapMaybe, which applies a function to Just x and leaves Nothing unchanged.

A worked mapMaybe

type Maybe a = Just a | Nothing;

let
  mapMaybe = \f m ->
    match m with {
      case Just x -> Just (f x);
      case Nothing -> Nothing;
    }
in
  ( mapMaybe ((+) 1) (Just 41)
  , mapMaybe ((+) 1) Nothing
  )

Testing constructors with match

There’s no special “isJust” operator — you write it with match:

type Maybe a = Just a | Nothing;

let
  isJust = \m ->
    match m with {
      case Just _ -> true;
      case Nothing -> false;
    }
in
  (isJust (Just 1), isJust Nothing)

Common mistake: missing arms

When matching on an ADT, Rex checks exhaustiveness. If you forget an arm, you’ll get an error that names the missing constructors.

Worked examples

Example: orElse

Problem: return the first Just value, otherwise return the fallback Maybe.

type Maybe a = Just a | Nothing;

let
  orElse = \ma mb ->
    match ma with {
      case Just x -> Just x;
      case Nothing -> mb;
    }
in
  (orElse (Just 1) (Just 2), orElse Nothing (Just 2))

Why this works: match chooses ma when it is Just, and only uses mb when ma is Nothing.

Example: andThen (Maybe bind)

Problem: chain a function that returns Maybe, failing early on Nothing.

type Maybe a = Just a | Nothing;

let
  andThen = \f ma ->
    match ma with {
      case Just x -> f x;
      case Nothing -> Nothing;
    },
  step = \x -> if x > 0 then Just (x + 1) else Nothing
in
  (andThen step (Just 3), andThen step Nothing, andThen step (Just (0 - 1)))

Why this works: Just unwraps and continues with f; Nothing short-circuits immediately.

Example: adding Unknown and handling exhaustiveness

Problem: extend Maybe and still keep matches exhaustive.

type Maybe a = Just a | Nothing | Unknown;

let
  fromMaybe = \d m ->
    match m with {
      case Just x -> x;
      case Nothing -> d;
      case Unknown -> d;
    }
in
  (fromMaybe 0 (Just 5), fromMaybe 0 Unknown)

Why this works: the Unknown arm makes the match complete for all constructors.

Example: Records and Updates

This example focuses on record-carrying ADTs, because that’s where you most often use:

  • projection (x.field)
  • update ({ x with { field = ... } })

Goal

Model a User record, read its fields, and produce an updated copy.

Step 1: define and update

type User = User { name: string, age: i32 };

let
  u: User = User { name = "Ada", age = 36 },
  older = { u with { age = u.age + 1 } }
in
  (u.age, older.age)

What to notice

  • User { ... } constructs a record-carrying ADT value.
  • u.age is field projection.
  • { u with { age = ... } } updates the record payload and re-wraps the constructor.

Step 2: update multiple fields

type User = User { name: string, age: i32 };

let
  u: User = User { name = "Ada", age = 36 },
  updated =
    { u with
        { age = u.age + 1
        , name = u.name + "!"
        }
    }
in
  (u, updated)

Step 3: why match sometimes matters

Projection/update is only allowed when a field is definitely available on the type. With a multi-variant ADT, you often refine it with match first:

type Sum = A { x: i32 } | B { x: i32 };

let s: Sum = A { x = 1 } in
match s with {
  case A {x} -> { s with { x = x + 1 } };
  case B {x} -> { s with { x = x + 2 } };
}

Worked examples

Example: birthday applied twice

Problem: define birthday : User -> User and apply it two times.

type User = User { name: string, age: i32 };

let
  birthday = \u -> { u with { age = u.age + 1 } },
  u0: User = User { name = "Ada", age = 36 },
  u2 = birthday (birthday u0)
in
  (u0.age, u2.age)

Why this works: each birthday call returns a new User with age incremented by one.

Example: add admin and promote

Problem: add a boolean field and set it to true.

type User = User { name: string, age: i32, admin: bool };

let
  promote = \u -> { u with { admin = true } },
  u0: User = User { name = "Ada", age = 36, admin = false }
in
  promote u0

Why this works: record update changes only admin, preserving other fields.

Example: add constructor C and update the match

Problem: extend Sum with C { x: i32 } and keep updates valid.

type Sum = A { x: i32 } | B { x: i32 } | C { x: i32 };

let s: Sum = C { x = 1 } in
match s with {
  case A {x} -> { s with { x = x + 1 } };
  case B {x} -> { s with { x = x + 2 } };
  case C {x} -> { s with { x = x + 3 } };
}

Why this works: each arm refines s to a definite constructor, so the update is type-safe.

Example: One map, many containers

This demonstrates deferred resolution of a Functor method value.

Goal

Understand why one definition of f can work for lists, options, and results, and how to avoid ambiguity when working with overloaded methods.

let f = map ((+) 1) in
  ( f [1, 2, 3]
  , f (Some 41)
  , f (Ok 21)
  )

Why this is cool

f is a single definition that can be applied to different container types. Rex defers selecting the Functor instance until you apply f to a concrete container.

Step-by-step

Start by binding the method value:

let f = map ((+) 1) in f

At this point, f is still a function, so Rex can keep it “overloaded”.

Now apply it to a list:

let f = map ((+) 1) in f [1, 2, 3]

At this call site, f must be List i32 -> List i32, so Rex selects Functor List.

Contrast: ambiguous non-function values

Some overloaded values are ambiguous if you don’t force a type. For example, pure 1 could be a List i32, Option i32, Array i32, Result i32 e, etc.

Fix it by forcing a type:

let x: Option i32 = pure 1 in x

Worked examples

Example: mapping over Err

Problem: verify that map does not change the error branch.

map ((+) 1) (Err "boom")

Why this works: Functor (Result e) maps only the Ok value, leaving Err unchanged.

Example: one g, list and option

Problem: define g = map (\x -> x * x) once and apply it to multiple containers.

let g = map (\x -> x * x) in
  (g [1, 2, 3], g (Some 4))

Why this works: instance resolution for map is deferred until each concrete call site.

Example: fixing ambiguous pure 1

Problem: choose a concrete container for pure 1.

let x: Option i32 = pure 1 in x

Why this works: the annotation forces pure to use the Applicative Option instance.

Example: Option pipelines (Applicative + Monad)

Option a represents “a value that might not exist”.

Goal

Write a multi-step computation that:

  • fails early by producing None
  • otherwise returns a final value wrapped in Some

Then rewrite it in three styles:

  1. plain match
  2. bind chaining (monadic)
  3. ap application (applicative)

Applicative: apply a wrapped function

ap (Some ((*) 2)) (Some 21)

If either side is None, the result is None.

Monad: sequence steps with bind

let
  step1 = \x -> if x < 0 then None else Some (x + 1),
  step2 = \x -> Some (x * 2)
in
  bind step2 (bind step1 (Some 10))

Refactoring tip

If you have many steps, name them:

let
  step1 = \x -> if x < 0 then None else Some (x + 1),
  step2 = \x -> Some (x * 2),
  run = \x -> bind step2 (bind step1 x)
in
  run (Some 10)

The same logic using match

bind is convenience. Under the hood, it’s the same “if None, stop” flow you would write with match:

let
  step1 = \x -> if x < 0 then None else Some (x + 1),
  step2 = \x -> Some (x * 2)
in
  match (Some 10) with {
    case None -> None;
    case Some v1 ->
      match (step1 v1) with {
        case None -> None;
        case Some v2 -> step2 v2;
      };
  }

When to use ap vs bind

  • Use ap when you have independent optional pieces and want to apply a function if all exist.
  • Use bind when the next step depends on the previous result.

Worked examples

Example: fail step1 on x == 0 too

Problem: update step1 so non-positive input fails.

let
  step1 = \x ->
    if x < 0 then None else
    if x == 0 then None else
      Some (x + 1)
in
  (step1 10, step1 0, step1 (0 - 1))

Why this works: the additional guard handles zero before success.

Example: add2opt via ap and pure

Problem: add two optional integers when both are present.

let
  add2opt = \ox oy -> ap (ap (pure (\x y -> x + y)) ox) oy
in
  (add2opt (Some 1) (Some 2), add2opt None (Some 2))

Why this works: pure lifts the function, then each ap applies one argument inside Option.

Example: validate list values with filter_map

Problem: keep only non-negative values and increment them.

let
  validate = \x -> if x < 0 then None else Some (x + 1)
in
  filter_map validate [3, (0 - 1), 0, 5]

Why this works: filter_map drops None results and unwraps Some values into the output list.

Example: Result workflows

Result a e short-circuits on Err.

Goal

Model a computation that can fail with a useful error, while keeping “happy path” code easy to read.

let
  step1 = \x -> if x < 0 then Err "negative" else Ok (x + 1),
  step2 = \x -> Ok (x * 2)
in
  ( bind step2 (bind step1 (Ok 10))
  , bind step2 (bind step1 (Ok (0 - 1)))
  )

What to notice

  • When step1 returns Err, the second bind is skipped.
  • This lets you write “happy path” code without deeply nested match.

Step-by-step: name the pipeline

let
  step1 = \x -> if x < 0 then Err "negative" else Ok (x + 1),
  step2 = \x -> Ok (x * 2),
  run = \x -> bind step2 (bind step1 x)
in
  (run (Ok 10), run (Ok (0 - 1)))

map vs bind

Use map when your function does not fail and does not change the container:

map ((+) 1) (Ok 41)

Use bind when your function returns another Result (and might fail):

bind (\x -> if x < 0 then Err "negative" else Ok x) (Ok 1)

Worked examples

Example: fail step2 when value is too large

Problem: make the second step return Err above a threshold.

let
  step1 = \x -> if x < 0 then Err "negative" else Ok (x + 1),
  step2 = \x -> if x > 20 then Err "too-large" else Ok (x * 2),
  run = \x -> bind step2 (bind step1 x)
in
  (run (Ok 10), run (Ok 25))

Why this works: bind short-circuits on either error source, including the new step2 condition.

Example: custom error ADT

Problem: replace string errors with structured errors.

type Err = Negative | TooLarge;

let
  step1 = \x -> if x < 0 then Err Negative else Ok (x + 1),
  step2 = \x -> if x > 20 then Err TooLarge else Ok (x * 2),
  run = \x -> bind step2 (bind step1 x)
in
  (run (Ok 10), run (Ok 25), run (Ok (0 - 1)))

Why this works: error constructors carry precise machine-readable failure categories.

Example: and_then synonym

Problem: define a helper that reads like “then”.

let
  and_then = \mx f -> bind f mx,
  safe_inc = \x -> if x < 0 then Err "negative" else Ok (x + 1)
in
  and_then (Ok 1) safe_inc

Why this works: and_then is just argument-reordered bind, so behavior is identical.

Example: Custom Show type class

This mirrors rex-cli/examples/typeclasses_custom_show.rex.

Goal

Define your own show-printing API that turns values into string without baking formatting into every call site.

We’ll build it up in layers:

  1. define the class
  2. add a base instance (i32)
  3. add a structured type (Point)
  4. (optional) add a container instance (List a)
class DemoShow a where {
  demo_show : a -> string;
}
type Point = Point { x: i32, y: i32 };

instance DemoShow i32 where {
  demo_show = \_ -> "<i32>";
}
instance DemoShow Point where {
  demo_show = \p -> "Point(" + demo_show p.x + ", " + demo_show p.y + ")";
}
demo_show (Point { x = 1, y = 2 })

Extending it

Add an instance DemoShow (List a) <= DemoShow a (see rex-cli/examples/typeclasses_custom_show.rex) and call demo_show [Point { x = 1, y = 2 }].

A worked DemoShow (List a) instance

Here is the list instance from the repo example, with commentary:

class DemoShow a where {
  demo_show : a -> string;
}
instance DemoShow i32 where {
  demo_show = \_ -> "<i32>";
}
instance<a> DemoShow (List a) <= DemoShow a where {
  demo_show = \xs ->
    let
      step = \out x ->
        if out == "["
          then out + demo_show x
          else out + ", " + demo_show x,
      out = foldl step "[" xs
    in
      out + "]";
}

Why the <= DemoShow a constraint?

Because the implementation calls demo_show x for list elements, so it requires DemoShow a.

Worked examples

Example: use "; " as the list separator

Problem: format list output with semicolons.

class DemoShow a where {
  demo_show : a -> string;
}
instance DemoShow i32 where {
  demo_show = \_ -> "<i32>";
}
instance<a> DemoShow (List a) <= DemoShow a where {
  demo_show = \xs ->
    let
      step = \out x ->
        if out == "["
          then out + demo_show x
          else out + "; " + demo_show x,
      out = foldl step "[" xs
    in
      out + "]";
}
demo_show [1, 2, 3]

Why this works: only the separator string changed; the fold structure stays the same.

Example: DemoShow bool

Problem: add show-print support for booleans.

class DemoShow a where {
  demo_show : a -> string;
}
instance DemoShow bool where {
  demo_show = \b -> if b then "true!" else "false!";
}
(demo_show true, demo_show false)

Why this works: the instance defines one method body specialized to bool.

Example: DemoShow (Option a)

Problem: print Some(...) and None for options.

class DemoShow a where {
  demo_show : a -> string;
}
instance DemoShow i32 where {
  demo_show = \_ -> "<i32>";
}
instance<a> DemoShow (Option a) <= DemoShow a where {
  demo_show = \ox ->
    match ox with {
      case Some x -> "Some(" + demo_show x + ")";
      case None -> "None";
    };
}
(demo_show (Some 1), demo_show None)

Why this works: pattern matching distinguishes constructors and delegates formatting of payloads.

Example: Custom Size type class

This mirrors rex-cli/examples/typeclasses_custom_size.rex.

Goal

Use a type class to define a common “size” operation across different data types, without hard-coding the type at every call site.

class Size a where {
  size : a -> i32;
}
type Blob = Blob { bytes: List i32 };

instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ t -> 1 + size t;
    };
}
instance Size Blob where {
  size = \b -> size b.bytes;
}
size (Blob { bytes = [1, 2, 3, 4] })

What this demonstrates

  • defining a class with one method,
  • writing an instance for a prelude type (List),
  • writing an instance for your own ADT (Blob),
  • using match for recursion.

Calling size generically

Once you have a class, you can write functions that work for any type that has an instance:

class Size a where {
  size : a -> i32;
}
instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ t -> 1 + size t;
    };
}
let
  bigger<a>: a -> i32 = \(x: a) where Size a -> size x + 1
in
  bigger [1, 2, 3]

The where Size a constraint says: “this function is valid as long as Size a exists”.

Worked examples

Example: is_empty

Problem: write a generic emptiness check from size.

class Size a where {
  size : a -> i32;
}
instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ t -> 1 + size t;
    };
}
let
  is_empty<a>: a -> bool = \(x: a) where Size a -> size x == 0
in
  (is_empty ([] is List i32), is_empty [1, 2, 3])

Why this works: any type with a Size instance can reuse the same is_empty logic.

Example: Blob with name

Problem: add a name field and keep size based on bytes only.

class Size a where {
  size : a -> i32;
}
instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ t -> 1 + size t;
    };
}
type Blob = Blob { name: string, bytes: List i32 };

instance Size Blob where {
  size = \b -> size b.bytes;
}
size (Blob { name = "payload", bytes = [1, 2, 3, 4] })

Why this works: Size Blob delegates to the bytes list, so metadata does not affect size.

Example: total_size

Problem: sum sizes of a list of values.

class Size a where {
  size : a -> i32;
}
instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ t -> 1 + size t;
    };
}
let
  total_size = \(xs: List a) where Size a ->
    foldl (\acc x -> acc + size x) 0 xs
in
  total_size [[1, 2], [], [3]]

Why this works: foldl accumulates per-element sizes using the shared Size a method.

Example: Indexable

Indexable is a multi-parameter class in the prelude (so you can use get without defining the class yourself).

Goal

Learn how to pull elements out of common containers with a single API:

  • lists
  • arrays

Example uses:

( get 0 [10, 20, 30] , get 2 ["a", "b", "c"] )

How it works

  • Lists and arrays have Indexable (List a, a) / Indexable (Array a, a) instances.
  • Tuples use numeric projection like .0 and .1 instead of get.

A more guided example

let
  xs = [10, 20, 30],
  first = get 0 xs,
  third = get 2 xs,
  ys = [1, 2, 3],
  last = get 2 ys
in
  (first, third, last)

Note on out-of-bounds

get is generally expected to error if the index is out of bounds (depending on the host/runtime implementation). If you need safe indexing (returning Option/Result), write it with match on your container type (e.g. [] vs x::xs for lists).

Worked examples

Example: head : List a -> Option a

Problem: return the first list element safely.

let
  head = \xs ->
    match xs with {
      case [] -> None;
      case x::_ -> Some x;
    }
in
  (head [] is Option i32, head [10, 20, 30])

Why this works: pattern matching handles empty and non-empty shapes explicitly.

Example: get on a larger list

Problem: read specific indices from [100, 200, 300, 400].

let
  xs = [100, 200, 300, 400]
in
  (get 0 xs, get 2 xs, get 3 xs)

Why this works: Indexable (List a, a) provides get for list element access.

Example: Small Standard Module Helpers

It’s common to build small helpers with let and reuse them.

Goal

Practice building tiny “glue” functions that keep your code readable, especially when composing many operations.

let
  compose = \f g x -> f (g x),
  inc = \x -> x + 1,
  double = \x -> x * 2,
  inc_then_double = compose double inc
in
  inc_then_double 10

Worked example: double_then_inc

Problem: define double_then_inc and show it differs from inc_then_double.

let
  compose = \f g x -> f (g x),
  inc = \x -> x + 1,
  double = \x -> x * 2,
  inc_then_double = compose double inc,
  double_then_inc = compose inc double
in
  (inc_then_double 10, double_then_inc 10)

Why this works: function composition order changes the final result (22 vs 21).

A more “pipeline” style

Sometimes it’s clearer to read left-to-right:

let
  pipe = \x f -> f x,
  pipe2 = \x f g -> g (f x),
  inc = \x -> x + 1,
  double = \x -> x * 2
in
  pipe2 10 inc double

This is the same logic as double (inc 10), just easier to extend when you have many steps.

Worked examples

Example: pipe3

Problem: apply three transforms in left-to-right style.

let
  pipe3 = \x f g h -> h (g (f x)),
  inc = \x -> x + 1,
  double = \x -> x * 2,
  square = \x -> x * x
in
  pipe3 3 inc double square

Why this works: each function consumes the previous output, so the pipeline is explicit.

Example: compose square then add one

Problem: build a reusable function that squares and then increments.

let
  compose = \f g x -> f (g x),
  square = \x -> x * x,
  add1 = \x -> x + 1,
  square_then_add1 = compose add1 square
in
  square_then_add1 5

Why this works: compose add1 square creates \x -> add1 (square x).

Example: map a composed function

Problem: combine map with composition for list transforms.

let
  compose = \f g x -> f (g x),
  square = \x -> x * x,
  add1 = \x -> x + 1,
  square_then_add1 = compose add1 square
in
  map square_then_add1 [1, 2, 3, 4]

Why this works: one composed function encapsulates the per-element transform applied by map.

Mini Project: Validating and Transforming Records

This example combines records, match, and Result.

Goal

Build a small “workflow” in Rex:

  1. validate a User
  2. transform it (birthday)
  3. return either a useful error or the transformed user

This is a pattern you can scale up: each step is a function returning a Result, and you connect steps with bind.

type User = User { name: string, age: i32 };

let
  validate = \u ->
    if u.age < 0
      then Err "age must be non-negative"
      else Ok u,
  birthday = \u -> { u with { age = u.age + 1 } }
in
  bind (\u -> Ok (birthday u)) (validate (User { name = "Ada", age = 36 }))

Worked extensions

Example: update birthday to change name too

Problem: increment age and append "!" to the user name in one transform.

type User = User { name: string, age: i32 };

let
  birthday = \u ->
    { u with
        { age = u.age + 1
        , name = u.name + "!"
        }
    }
in
  birthday (User { name = "Ada", age = 36 })

Why this works: one record update can set multiple fields at once.

Example: reject empty names during validation

Problem: make validation fail when name == "".

type User = User { name: string, age: i32 };

let
  validate = \u ->
    if u.age < 0 then Err "age must be non-negative" else
    if u.name == "" then Err "name must be non-empty" else
      Ok u
in
  ( validate (User { name = "Ada", age = 36 })
  , validate (User { name = "", age = 36 })
  )

Why this works: the second guard introduces an additional failure branch before success.

Example: structured error ADT

Problem: replace free-form strings with typed error constructors.

type UserError = NegativeAge | EmptyName;
type User = User { name: string, age: i32 };

let
  validate = \u ->
    if u.age < 0 then Err NegativeAge else
    if u.name == "" then Err EmptyName else
      Ok u
in
  validate (User { name = "", age = 36 })

Why this works: callers can pattern-match on error constructors without string parsing.

A worked “structured error” version

Instead of strings, define an error ADT:

type UserError = NegativeAge | EmptyName;
type User = User { name: string, age: i32 };

let
  validate = \u ->
    if u.age < 0 then Err NegativeAge else
    if u.name == "" then Err EmptyName else
      Ok u,
  birthday = \u -> { u with { age = u.age + 1 } },
  run = \u -> bind (\ok -> Ok (birthday ok)) (validate u)
in
  ( run (User { name = "Ada", age = 36 })
  , run (User { name = "", age = 36 })
  , run (User { name = "Ada", age = (0 - 1) })
  )

What to notice

  • validate returns early with the first error it finds.
  • run uses bind to only call birthday when validation succeeded.

Worked examples

Example: add an upper-age validation rule

Problem: reject ages greater than 150.

type UserError = NegativeAge | EmptyName | TooOld;
type User = User { name: string, age: i32 };

let
  validate = \u ->
    if u.age < 0 then Err NegativeAge else
    if u.age > 150 then Err TooOld else
    if u.name == "" then Err EmptyName else
      Ok u
in
  ( validate (User { name = "Ada", age = 36 })
  , validate (User { name = "Ada", age = 200 })
  )

Why this works: the additional guard catches out-of-range ages before success.

Example: chain a second transform step with bind

Problem: run two transforms (birthday then normalize_name) after validation.

type User = User { name: string, age: i32 };

let
  validate = \u -> if u.age < 0 then Err "negative-age" else Ok u,
  birthday = \u -> Ok ({ u with { age = u.age + 1 } }),
  normalize_name = \u -> Ok ({ u with { name = u.name + "!" } }),
  run = \u ->
    bind normalize_name
      (bind birthday
        (validate u))
in
  run (User { name = "Ada", age = 36 })

Why this works: each bind feeds a successful result into the next transform.

Example: split validation into smaller validators

Problem: compose independent validators with bind.

type User = User { name: string, age: i32 };

let
  check_age = \u -> if u.age < 0 then Err "negative-age" else Ok u,
  check_name = \u -> if u.name == "" then Err "empty-name" else Ok u,
  validate = \u -> bind check_name (check_age u)
in
  ( validate (User { name = "Ada", age = 36 })
  , validate (User { name = "", age = 36 })
  )

Why this works: each validator has the same User -> Result User e shape, so they compose cleanly.

Interactive Demos

These demos are meant to be edited and run directly in the docs.

Demo: Factorial

This demo computes n! using direct recursion: it multiplies n by the factorial of n - 1 until it reaches the base case 0, which returns 1. It is a minimal example of structural recursion over integers and shows how a simple mathematical definition maps directly to Rex function syntax.

Related reading: Factorial.

The implementation is centered on fact, which uses an if expression to separate the base case from the recursive case. The final line evaluates fact 6, so the output is a single integer result; this keeps the demo focused on call structure and termination rather than data modeling.

fn fact : i32 -> i32 = \n ->
  if n == 0
  then 1
  else n * fact (n - 1);

fact 6

Demo: Fibonacci

This demo generates Fibonacci numbers with the classic recursive recurrence: each value is the sum of the previous two, with base cases at 0 and 1. It illustrates branching recursion and builds a small prefix of the sequence so you can see the growth pattern directly in the output.

Related reading: Fibonacci number.

The fib function mirrors the mathematical recurrence directly: when n is 0 or 1 it returns immediately, otherwise it performs two recursive calls and adds their results. Instead of evaluating just one input, the demo computes a list from fib 0 through fib 10, which makes it easy to confirm correctness across multiple cases in one run.

fn fib : i32 -> i32 = \n ->
  if n <= 1
  then n
  else fib (n - 1) + fib (n - 2);

[fib 0, fib 1, fib 2, fib 3, fib 4, fib 5, fib 6, fib 7, fib 8, fib 9, fib 10]

Demo: Merge Sort

This demo implements merge sort, a divide-and-conquer algorithm that splits a list into halves, recursively sorts each half, and then merges the two sorted results. The implementation highlights a full pipeline of helper functions (split, merge, compare) and demonstrates how recursive decomposition can produce deterministic, stable ordering over immutable lists.

Related reading: Merge sort.

compare_i32 converts primitive comparisons into an Order ADT, and split_alt peels off pairs to partition input into two sublists without mutation. mergesort handles the empty and singleton base cases, then recursively sorts both halves and combines them with merge, which pattern-matches on two lists and always emits the smaller head first.

type Order = Lt | Eq | Gt;

fn compare_i32 : i32 -> i32 -> Order = \a b ->
  if a < b then Lt else if a == b then Eq else Gt;

fn split_alt : List i32 -> (List i32, List i32) = \xs ->
  match xs with {
    case [] -> ([], []);
    case [x] -> ([x], []);
    case x::y::rest ->
      let (xs1, ys1) = split_alt rest in (Cons x xs1, Cons y ys1);
  };

fn merge : List i32 -> List i32 -> List i32 = \xs ys ->
  match (xs, ys) with {
    case ([], _) -> ys;
    case (_, []) -> xs;
    case (x::xt, y::yt) ->
      match (compare_i32 x y) with {
        case Lt -> Cons x (merge xt ys);
        case Eq -> Cons x (Cons y (merge xt yt));
        case Gt -> Cons y (merge xs yt);
      };
  };

fn mergesort : List i32 -> List i32 = \xs ->
  match xs with {
    case [] -> [];
    case [x] -> [x];
    case _ ->
      let (left, right) = split_alt xs in
      merge (mergesort left) (mergesort right);
  };

let
  input = [9, 1, 7, 3, 2, 8, 6, 4, 5]
in
  mergesort input

Demo: Binary Search Tree

This demo builds and queries a binary search tree, where values smaller than a node go left and larger values go right. It shows insertion, membership testing, and size calculation over a custom recursive ADT, illustrating how ordered data structures can be expressed with pure pattern-matching functions.

Related reading: Binary search tree.

The Tree type has Empty and Node constructors, and each operation recursively follows tree structure. insert descends left or right based on key order and rebuilds the path back up, contains follows the same branching logic to test membership, and size traverses both subtrees to count nodes; the final let block builds an example tree and returns a tuple of summary queries.

type Tree = Empty | Node { key: i32, left: Tree, right: Tree };

fn insert : i32 -> Tree -> Tree = \k t ->
  match t with {
    case Empty -> Node { key = k, left = Empty, right = Empty };
    case Node {key, left, right} ->
      if k < key then
        Node { key = key, left = insert k left, right = right }
      else if k > key then
        Node { key = key, left = left, right = insert k right }
      else
        t;
  };

fn contains : i32 -> Tree -> bool = \k t ->
  match t with {
    case Empty -> false;
    case Node {key, left, right} ->
      if k == key then true
      else if k < key then contains k left
      else contains k right;
  };

fn size : Tree -> i32 = \t ->
  match t with {
    case Empty -> 0;
    case Node {left, right} -> 1 + size left + size right;
  };

let
  t0: Tree = Empty
in
  let
    t1 = insert 7 (insert 2 (insert 9 (insert 1 (insert 5 t0)))),
    t2 = insert 8 t1
  in
    (size t2, contains 5 t2, contains 4 t2)

Demo: Expression Evaluator

This demo evaluates arithmetic expressions represented as an AST with constructors for literals, addition, multiplication, and negation. Alongside evaluation, it computes expression depth and performs a small simplification pass, showing how one tree structure can support multiple independent recursive analyses and transformations.

Related reading: Abstract syntax tree.

The code defines one ADT (Expr) and then reuses it across three traversals: eval computes numeric meaning, depth computes structural height, and simplify_once applies a local rewrite rule for double negation. In the final expression block, two sample trees are built, one is simplified once, and the output tuple shows evaluation and depth results side-by-side.

type Expr = Lit i32 | Add Expr Expr | Mul Expr Expr | Neg Expr;

fn eval : Expr -> i32 = \e ->
  match e with {
    case Lit n -> n;
    case Add a b -> eval a + eval b;
    case Mul a b -> eval a * eval b;
    case Neg x -> 0 - eval x;
  };

fn depth : Expr -> i32 = \e ->
  match e with {
    case Lit _ -> 1;
    case Add a b ->
      if depth a > depth b then 1 + depth a else 1 + depth b;
    case Mul a b ->
      if depth a > depth b then 1 + depth a else 1 + depth b;
    case Neg x -> 1 + depth x;
  };

fn simplify_once : Expr -> Expr = \e ->
  match e with {
    case Neg (Neg x) -> x;
    case _ -> e;
  };

let
  expr1 = Add (Lit 2) (Mul (Lit 3) (Lit 4)),
  expr2 = Neg (Neg (Add (Lit 5) (Mul (Lit 1) (Lit 9))))
in
  let simplified = simplify_once expr2 in
  (eval expr1, depth expr1, eval simplified)

Demo: Dijkstra Lite

This demo models a minimal shortest-path problem and applies the core relaxation idea behind Dijkstra-style algorithms: compare a direct edge with an indirect path through an intermediate node and keep the smaller distance. It uses a small Dist ADT (Inf or Finite) to make unreachable and reachable cases explicit and type-safe.

Related reading: Dijkstra’s algorithm.

add_weight and min_dist isolate the distance algebra, so shortest_a_to_b can read clearly as “direct path versus via-C path, then pick minimum.” The sample graphs in the final let block exercise both outcomes: one where routing through C wins and one where the direct edge is best, with as_i32 converting the ADT into plain output numbers for display.

type Dist = Inf | Finite i32;
type Graph = Graph { ab: i32, ac: i32, cb: i32 };

fn add_weight : Dist -> i32 -> Dist = (\d w ->
  match d with {
    case Inf -> Inf;
    case Finite x -> Finite (x + w);
  }
);

fn min_dist : Dist -> Dist -> Dist = (\a b ->
  match (a, b) with {
    case (Inf, x) -> x;
    case (x, Inf) -> x;
    case (Finite x, Finite y) ->
      if x <= y then Finite x else Finite y;
  }
);

fn shortest_a_to_b : Graph -> Dist = (\g ->
  let
    direct = Finite g.ab,
    via_c = add_weight (Finite g.ac) g.cb
  in
    min_dist direct via_c
);

fn as_i32 : Dist -> i32 = (\d ->
  match d with {
    case Inf -> -1;
    case Finite x -> x;
  }
);

let
  g1 = Graph { ab = 10, ac = 3, cb = 4 },
  g2 = Graph { ab = 5, ac = 9, cb = 9 },
  d1 = shortest_a_to_b g1,
  d2 = shortest_a_to_b g2
in
  (as_i32 d1, as_i32 d2)

Demo: 0/1 Knapsack

This demo solves the 0/1 knapsack optimization problem with dynamic programming: each item can be taken at most once, and the algorithm computes the best achievable value for every capacity from 0 to max_cap. The table is represented as immutable rows, and each new row is derived from the previous one by choosing between “take” and “skip” for the current item.

Related reading: Knapsack problem.

zeros initializes the base DP row, build_row computes one new row for a single item, and go folds this process across the full item list. For each capacity, build_row compares without (skip item) and with_item (take item plus best compatible remainder), then stores the maximum; solve returns the final cell at max_cap.

type Item = Item { w: i32, v: i32 };

fn nth : List i32 -> i32 -> i32 = \xs i ->
  match xs with {
    case [] -> 0;
    case x::rest ->
      if i == 0 then x else nth rest (i - 1);
  };

fn zeros : i32 -> i32 -> List i32 = \i max_cap ->
  if i > max_cap then [] else Cons 0 (zeros (i + 1) max_cap);

fn build_row : Item -> List i32 -> i32 -> i32 -> List i32 = \item prev cap max_cap ->
  if cap > max_cap then
    []
  else
    let
      without = nth prev cap,
      with_item =
        if item.w <= cap then
          item.v + nth prev (cap - item.w)
        else
          0,
      best = if without >= with_item then without else with_item
    in
      Cons best (build_row item prev (cap + 1) max_cap);

fn go : List Item -> List i32 -> i32 -> List i32 = \remaining row max_cap ->
  match remaining with {
    case [] -> row;
    case item::rest ->
      let next = build_row item row 0 max_cap in
      go rest next max_cap;
  };

fn solve : List Item -> i32 -> i32 = \items max_cap ->
  nth (go items (zeros 0 max_cap) max_cap) max_cap;

let
  items = [
    Item { w = 2, v = 3 },
    Item { w = 3, v = 4 },
    Item { w = 4, v = 5 },
    Item { w = 5, v = 8 }
  ],
  cap_5 = solve items 5,
  cap_8 = solve items 8
in
  (cap_5, cap_8)

Demo: Union-Find

This demo implements core union-find operations for tracking connected components in a small graph. It maintains parent links, finds set representatives, and merges sets with union, then checks connectivity; together these operations demonstrate how incremental edge additions can be answered with near-constant-time component queries.

Related reading: Disjoint-set data structure.

get_parent and set_parent provide indexed access over a fixed-size parent record, while find follows parent pointers recursively until it reaches a representative. union links one representative to another when sets differ, and connected compares representatives; the final block performs a few unions and returns both connectivity checks and representatives to show resulting components.

type UF = UF { p0: i32, p1: i32, p2: i32, p3: i32, p4: i32 };

fn get_parent : UF -> i32 -> i32 = \uf x ->
  if x == 0 then uf.p0
  else if x == 1 then uf.p1
  else if x == 2 then uf.p2
  else if x == 3 then uf.p3
  else uf.p4;

fn set_parent : UF -> i32 -> i32 -> UF = \uf x p ->
  if x == 0 then { uf with { p0 = p } }
  else if x == 1 then { uf with { p1 = p } }
  else if x == 2 then { uf with { p2 = p } }
  else if x == 3 then { uf with { p3 = p } }
  else { uf with { p4 = p } };

fn find : UF -> i32 -> i32 = \uf x ->
  let px = get_parent uf x in
  if px == x then x else find uf px;

fn union : UF -> i32 -> i32 -> UF = \uf a b ->
  let
    ra = find uf a,
    rb = find uf b
  in
    if ra == rb then uf else set_parent uf rb ra;

fn connected : UF -> i32 -> i32 -> bool = \uf a b -> find uf a == find uf b;

let
  uf0 = UF { p0 = 0, p1 = 1, p2 = 2, p3 = 3, p4 = 4 },
  uf1 = union uf0 0 1,
  uf2 = union uf1 1 2,
  uf3 = union uf2 3 4
in
  (
    connected uf3 0 2,
    connected uf3 0 4,
    find uf3 2,
    find uf3 4
  )

Demo: Prefix Parser + Evaluator

This demo performs recursive-descent parsing over a prefix token stream to build an expression tree, then evaluates that tree. It separates syntax (Tok) from semantics (Expr) and returns both the parsed expression and unconsumed tokens, which is a common parser design for composing larger grammars.

Related reading: Polish notation and Recursive descent parser.

parse_expr is the parser entrypoint and consumes tokens according to constructor shape: numbers produce leaf nodes, while operators recursively parse the required subexpressions. eval then interprets the produced AST, and is_empty checks whether parsing consumed all tokens; the two sample token streams demonstrate both parsing and evaluation in one result tuple.

type Tok = TNum i32 | TPlus | TMul | TNeg;
type Expr = Num i32 | Add Expr Expr | Mul Expr Expr | Neg Expr;

fn parse_expr : List Tok -> (Expr, List Tok) = \toks ->
  match toks with {
    case [] -> (Num 0, []);
    case TNum n::rest -> (Num n, rest);
    case TPlus::rest ->
      let
        (lhs, rest1) = parse_expr rest,
        (rhs, rest2) = parse_expr rest1
      in
        (Add lhs rhs, rest2);
    case TMul::rest ->
      let
        (lhs, rest1) = parse_expr rest,
        (rhs, rest2) = parse_expr rest1
      in
        (Mul lhs rhs, rest2);
    case TNeg::rest ->
      let (inner, rest1) = parse_expr rest in
      (Neg inner, rest1);
  };

fn eval : Expr -> i32 = \expr ->
  match expr with {
    case Num n -> n;
    case Add a b -> eval a + eval b;
    case Mul a b -> eval a * eval b;
    case Neg x -> 0 - eval x;
  };

fn is_empty<a> : List a -> bool = \xs ->
  match xs with {
    case [] -> true;
    case _::_ -> false;
  };

let
  toks1 = [TPlus, TNum 2, TMul, TNum 3, TNum 4],
  toks2 = [TPlus, TNeg, TNum 3, TNum 10],
  (ast1, rest1) = parse_expr toks1,
  (ast2, rest2) = parse_expr toks2
in
  (eval ast1, is_empty rest1, eval ast2, is_empty rest2)

Demo: Topological Sort (Kahn Style)

This demo computes a topological ordering of a directed acyclic graph using a Kahn-style process: repeatedly select nodes with zero in-degree, output them, and remove their outgoing edges. It demonstrates dependency resolution in graph form and returns an empty list when edges remain but no valid next node exists.

Related reading: Topological sorting.

The helpers break the algorithm into pure list operations: in_degree counts incoming edges, remove_outgoing deletes edges from a chosen node, and enqueue_zeros updates the processing queue with newly unlocked nodes. kahn drives the main loop by consuming the queue and accumulating output order, with a final reversal because nodes are prepended during recursion.

type Node = A | B | C | D;
type Edge = Edge Node Node;

fn node_eq : Node -> Node -> bool = \a b ->
  match (a, b) with {
    case (A, A) -> true;
    case (B, B) -> true;
    case (C, C) -> true;
    case (D, D) -> true;
    case _ -> false;
  };

fn contains : List Node -> Node -> bool = \xs x ->
  match xs with {
    case [] -> false;
    case y::ys -> if node_eq y x then true else contains ys x;
  };

fn append : List Node -> List Node -> List Node = \xs ys ->
  match xs with {
    case [] -> ys;
    case h::t -> Cons h (append t ys);
  };

fn reverse_go : List Node -> List Node -> List Node = \rest acc ->
  match rest with {
    case [] -> acc;
    case h::t -> reverse_go t (Cons h acc);
  };

fn reverse : List Node -> List Node = \xs ->
  reverse_go xs [];

fn is_empty<a> : List a -> bool = \xs ->
  match xs with {
    case [] -> true;
    case _::_ -> false;
  };

fn remove_outgoing : List Edge -> Node -> List Edge = \edges n ->
  match edges with {
    case [] -> [];
    case Edge from to::rest ->
      if node_eq from n then remove_outgoing rest n
      else Cons (Edge from to) (remove_outgoing rest n);
  };

fn in_degree : List Edge -> Node -> i32 = \edges n ->
  match edges with {
    case [] -> 0;
    case Edge from to::rest ->
      let tail = in_degree rest n in
      if node_eq to n then 1 + tail else tail;
  };

fn push_unique : List Node -> Node -> List Node = \queue n ->
  if contains queue n then queue else append queue [n];

fn enqueue_zeros : List Node -> List Node -> List Node -> List Edge -> List Node = \nodes queue seen edges ->
  match nodes with {
    case [] -> queue;
    case n::rest ->
      let queue1 =
        if contains seen n then
          queue
        else if in_degree edges n == 0 then
          push_unique queue n
        else
          queue
      in
        enqueue_zeros rest queue1 seen edges;
  };

fn kahn : List Node -> List Node -> List Node -> List Edge -> List Node -> List Node = \queue seen order edges nodes ->
  match queue with {
    case [] ->
      if is_empty edges then
        reverse order
      else
        [];
    case n::rest ->
      let
        edges1 = remove_outgoing edges n,
        seen1 = Cons n seen,
        queue1 = enqueue_zeros nodes rest seen1 edges1
      in
        kahn queue1 seen1 (Cons n order) edges1 nodes;
  };

let
  nodes = [A, B, C, D],
  edges = [Edge A B, Edge A C, Edge B D, Edge C D],
  initial = enqueue_zeros nodes [] [] edges
in
  kahn initial [] [] edges nodes

Demo: N-Queens Backtracking

This demo counts valid placements of queens on an N x N chessboard using backtracking with pruning. It places one queen per row, rejects positions that share a column or diagonal with prior queens, and recursively explores only safe continuations, which makes it a compact example of constraint search.

Related reading: N-queens problem.

is_safe checks a candidate column against previously placed queens, carrying a diagonal distance counter so both diagonal directions can be tested with abs_i32. try_cols iterates candidate columns within a row and accumulates solution counts, while count_from advances to the next row after each safe placement; solve just seeds the recursion with row 0 and an empty placement list.

fn abs_i32 : i32 -> i32 = \x ->
  if x < 0 then 0 - x else x;

fn is_safe : i32 -> List i32 -> i32 -> bool = \col placed dist ->
  match placed with {
    case [] -> true;
    case c::rest ->
      if col == c then
        false
      else if abs_i32 (col - c) == dist then
        false
      else
        is_safe col rest (dist + 1);
  };

fn count_from : i32 -> i32 -> List i32 -> i32 = \row n placed ->
  if row == n then
    1
  else
    try_cols row n placed 0;

fn try_cols : i32 -> i32 -> List i32 -> i32 -> i32 = \row n placed col ->
  if col == n then
    0
  else
    let rest = try_cols row n placed (col + 1) in
    if is_safe col placed 1 then
      count_from (row + 1) n (Cons col placed) + rest
    else
      rest;

fn solve : i32 -> i32 = \n ->
  count_from 0 n [];

(solve 4, solve 5)

Built-in types & functions

This page is auto-generated from the prelude source. Run cargo run -p rex --bin gen_prelude_docs to refresh it.

Built-in Types

TypeDescription
Array aFixed-size indexed sequence.
Dict aDictionary/record-like mapping from field labels to values.
List aImmutable singly linked list. Constructors: Empty, Cons.
Option aOptional value (Some or None). Constructors: Some, None.
Result a bResult value (Ok or Err) for success/failure flows. Constructors: Err, Ok.
boolBoolean truth value.
datetimeUTC timestamp value.
f3232-bit floating-point number.
f6464-bit floating-point number.
i1616-bit signed integer.
i3232-bit signed integer.
i6464-bit signed integer.
i88-bit signed integer.
stringUTF-8 string value.
u1616-bit unsigned integer.
u3232-bit unsigned integer.
u6464-bit unsigned integer.
u88-bit unsigned integer.
uuidUUID value.

Built-in Type Classes

AdditiveGroup

Types supporting additive inverse.

Superclasses: Subtractive

Methods:

  • negate: AdditiveGroup 'a => ('a -> 'a). Additive inverse.

AdditiveMonoid

Types with additive identity and associative addition.

Superclasses: none

Methods:

  • zero: AdditiveMonoid 'a => 'a. Additive identity.
  • +: AdditiveMonoid 'a => ('a -> ('a -> 'a)). Addition (or concatenation for strings).

Alternative

Applicative types with a fallback choice operation.

Superclasses: Applicative

Methods:

  • or_else: Alternative 'f => ((('f 'a) -> ('f 'a)) -> (('f 'a) -> ('f 'a))). Provide an alternative container value.

Applicative

Functors that can lift values and apply wrapped functions.

Superclasses: Functor

Methods:

  • pure: Applicative 'f => ('a -> ('f 'a)). Lift a plain value into an applicative context.
  • ap: Applicative 'f => (('f ('a -> 'b)) -> (('f 'a) -> ('f 'b))). Apply wrapped functions to wrapped values.

Default

Types with a canonical default value.

Superclasses: none

Methods:

  • default: Default 'a => 'a. Canonical default value for a type. For Result a e, this requires Default a.

Divisive

Types supporting division.

Superclasses: MultiplicativeMonoid

Methods:

  • /: Divisive 'a => ('a -> ('a -> 'a)). Division.

Eq

Types supporting equality/inequality comparison.

Superclasses: none

Methods:

  • ==: Eq 'a => ('a -> ('a -> bool)). Equality comparison.
  • !=: Eq 'a => ('a -> ('a -> bool)). Inequality comparison.

Field

Types supporting division in addition to ring operations.

Superclasses: Ring, Divisive

Methods:

Filterable

Functors supporting filtering and partial mapping.

Superclasses: Functor

Methods:

  • filter: Filterable 'f => (('a -> bool) -> (('f 'a) -> ('f 'a))). Keep elements that satisfy a predicate.
  • filter_map: Filterable 'f => (('a -> (Option 'b)) -> (('f 'a) -> ('f 'b))). Map and drop missing results in one pass.

Foldable

Containers that can be reduced with folds.

Superclasses: none

Methods:

  • foldl: Foldable 't => (('b -> ('a -> 'b)) -> ('b -> (('t 'a) -> 'b))). Strict left fold.
  • foldr: Foldable 't => (('a -> ('b -> 'b)) -> ('b -> (('t 'a) -> 'b))). Right fold.
  • fold: Foldable 't => (('b -> ('a -> 'b)) -> ('b -> (('t 'a) -> 'b))). Left-style fold over a container.

Functor

Type constructors that support structure-preserving mapping.

Superclasses: none

Methods:

  • map: Functor 'f => (('a -> 'b) -> (('f 'a) -> ('f 'b))). Apply a function to each value inside a functor.

Indexable

Containers that support indexed element access.

Superclasses: none

Methods:

  • get: Indexable ('t, 'a) => (i32 -> ('t -> 'a)). Get an element by index.

Integral

Integral numeric types supporting modulo.

Superclasses: none

Methods:

  • %: Integral 'a => ('a -> ('a -> 'a)). Remainder/modulo operation.

Monad

Applicatives supporting dependent sequencing (bind).

Superclasses: Applicative

Methods:

  • bind: Monad 'm => (('a -> ('m 'b)) -> (('m 'a) -> ('m 'b))). Monadic flat-map/sequencing operation.

MultiplicativeMonoid

Types with multiplicative identity and associative multiplication.

Superclasses: none

Methods:

  • one: MultiplicativeMonoid 'a => 'a. Multiplicative identity.
  • *: MultiplicativeMonoid 'a => ('a -> ('a -> 'a)). Multiplication.

Ord

Types with total ordering comparisons.

Superclasses: Eq

Methods:

  • cmp: Ord 'a => ('a -> ('a -> i32)). Three-way comparison returning negative/zero/positive i32.
  • <: Ord 'a => ('a -> ('a -> bool)). Less-than comparison.
  • <=: Ord 'a => ('a -> ('a -> bool)). Less-than-or-equal comparison.
  • >: Ord 'a => ('a -> ('a -> bool)). Greater-than comparison.
  • >=: Ord 'a => ('a -> ('a -> bool)). Greater-than-or-equal comparison.

Ring

Types supporting additive group plus multiplication.

Superclasses: AdditiveGroup, MultiplicativeMonoid

Methods:

Semiring

Types supporting additive and multiplicative monoid operations.

Superclasses: AdditiveMonoid, MultiplicativeMonoid

Methods:

Sequence

Ordered containers with slicing/zipping operations.

Superclasses: Functor, Foldable

Methods:

  • take: Sequence 'f => (i32 -> (('f 'a) -> ('f 'a))). Keep only the first n elements.
  • skip: Sequence 'f => (i32 -> (('f 'a) -> ('f 'a))). Drop the first n elements.
  • zip: Sequence 'f => (('f 'a) -> (('f 'b) -> ('f ('a, 'b)))). Pair elements from two containers by position.
  • unzip: Sequence 'f => (('f ('a, 'b)) -> (('f 'a), ('f 'b))). Split a container of pairs into a pair of containers.

Show

Types that can be converted to user-facing strings (Haskell-style naming).

Superclasses: none

Methods:

  • show: Show 'a => ('a -> string). Render a value as a human-readable string.

Subtractive

Types supporting binary subtraction.

Superclasses: Semiring

Methods:

  • -: Subtractive 'a => ('a -> ('a -> 'a)). Subtraction.

Built-in Functions

Overloaded (Type Class Methods)

FunctionSignatureImplemented OnDescription
negate('a -> 'a)i8
i16
i32
i64
f32
f64
Additive inverse.
zero'astring
u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Additive identity.
+('a -> ('a -> 'a))string
u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Addition (or concatenation for strings).
or_else((('f 'a) -> ('f 'a)) -> (('f
'a) -> ('f 'a)))
List
Option
Array
(Result 'e)
Provide an alternative container value.
pure('a -> ('f 'a))List
Option
Array
(Result 'e)
Lift a plain value into an applicative context.
ap(('f ('a -> 'b)) -> (('f 'a)
-> ('f 'b)))
List
Option
Array
(Result 'e)
Apply wrapped functions to wrapped values.
default'abool
u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
(List 'a)
(Array 'a)
(Option 'a)
(Result 'a 'e)
Canonical default value for a type. For Result a e, this requires Default a.
/('a -> ('a -> 'a))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Division.
==('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
bool
string
uuid
datetime
(List 'a)
(Option 'a)
(Array 'a)
(Result 'a 'e)
Equality comparison.
!=('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
bool
string
uuid
datetime
(List 'a)
(Option 'a)
(Array 'a)
(Result 'a 'e)
Inequality comparison.
filter(('a -> bool) -> (('f 'a) ->
('f 'a)))
List
Option
Array
Keep elements that satisfy a predicate.
filter_map(('a -> (Option 'b)) -> (('f
'a) -> ('f 'b)))
List
Option
Array
Map and drop missing results in one pass.
foldl(('b -> ('a -> 'b)) -> ('b ->
(('t 'a) -> 'b)))
List
Option
Array
Strict left fold.
foldr(('a -> ('b -> 'b)) -> ('b ->
(('t 'a) -> 'b)))
List
Option
Array
Right fold.
fold(('b -> ('a -> 'b)) -> ('b ->
(('t 'a) -> 'b)))
List
Option
Array
Left-style fold over a container.
map(('a -> 'b) -> (('f 'a) -> ('f
'b)))
List
Option
Array
(Result 'e)
Apply a function to each value inside a functor.
get(i32 -> ('t -> 'a))((List 'a), 'a)
((Array 'a), 'a)
Get an element by index.
%('a -> ('a -> 'a))u8
u16
u32
u64
i8
i16
i32
i64
Remainder/modulo operation.
bind(('a -> ('m 'b)) -> (('m 'a)
-> ('m 'b)))
List
Option
Array
(Result 'e)
Monadic flat-map/sequencing operation.
one'au8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Multiplicative identity.
*('a -> ('a -> 'a))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Multiplication.
cmp('a -> ('a -> i32))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
Three-way comparison returning negative/zero/positive i32.
<('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
Less-than comparison.
<=('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
Less-than-or-equal comparison.
>('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
Greater-than comparison.
>=('a -> ('a -> bool))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
Greater-than-or-equal comparison.
take(i32 -> (('f 'a) -> ('f 'a)))List
Array
Keep only the first n elements.
skip(i32 -> (('f 'a) -> ('f 'a)))List
Array
Drop the first n elements.
zip(('f 'a) -> (('f 'b) -> ('f
('a, 'b))))
List
Array
Pair elements from two containers by position.
unzip(('f ('a, 'b)) -> (('f 'a),
('f 'b)))
List
Array
Split a container of pairs into a pair of containers.
show('a -> string)bool
u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
string
uuid
datetime
(List 'a)
(Array 'a)
(Option 'a)
(Result 'a 'e)
Render a value as a human-readable string.
-('a -> ('a -> 'a))u8
u16
u32
u64
i8
i16
i32
i64
f32
f64
Subtraction.

Other Built-ins

FunctionSignatureDescription
&&(bool -> (bool -> bool))Boolean conjunction.
Cons('a -> ((List 'a) -> (List
'a)))
Construct a non-empty list from head and tail.
Empty(List 'a)The empty list constructor.
Err('e -> (Result 't 'e))Construct a failed Result.
None(Option 't)The empty Option constructor.
Ok('t -> (Result 't 'e))Construct a successful Result.
Some('t -> (Option 't))Construct a present Option value.
countFoldable 'f => (('f 'a) ->
i32)
Count elements in a foldable container.
is_err((Result 't 'e) -> bool)Check whether a Result is Err.
is_none((Option 'a) -> bool)Check whether an Option is None.
is_ok((Result 't 'e) -> bool)Check whether a Result is Ok.
is_some((Option 'a) -> bool)Check whether an Option is Some.
maxFoldable 'f, Ord 'a => (('f
'a) -> 'a)
Maximum element by ordering.
meanFoldable 'f, Field 'a => (('f
'a) -> 'a)
Arithmetic mean over numeric foldables.
minFoldable 'f, Ord 'a => (('f
'a) -> 'a)
Minimum element by ordering.
sumFoldable 'f, AdditiveMonoid 'a
=> (('f 'a) -> 'a)
Sum all elements in a foldable container.
to_array((List 'a) -> (Array 'a))Convert a list to an array.
to_list((Array 'a) -> (List 'a))Convert an array to a list.
unwrap((Option 'a) -> 'a)

((Result 't 'e) -> 't)
Extract the inner value from Some/Ok, or raise an error for None/Err.
``

Rex Language Guide

Rex is a small, strongly-typed functional DSL with:

  • Hindley–Milner type inference (let-polymorphism)
  • algebraic data types (ADTs), including record-carrying constructors
  • Haskell-style type classes (including higher-kinded classes like Functor)

This guide is meant for users and embedders. For locked/production-facing semantics and edge cases, see SPEC.md.

Source Forms

A Rex source is parsed as a compilation unit containing:

  • zero or more declarations (type, class, instance, fn, import)
  • optionally followed by a single expression

Sources with a final expression are snippets or program entry points. Declaration-only sources are modules.

Example snippet:

fn inc : i32 -> i32 = \x -> x + 1;

let
  xs = [1, 2, 3]
in
  map inc xs

Program Entry Points

When a source is run as a program, Rex uses one entry point:

  • If the source defines fn main, main is the entry point. The same source must not also contain a final expression.
  • If the source does not define main, the final expression is treated as an implicit zero-argument entry point.
  • If there is no main and no final expression, running the source as a program is an error.

The CLI passes arguments to main from a JSON file supplied with --inputs. The JSON file is a top-level object whose fields match the parameter names:

fn main scale: i32 -> offset: i32 -> i32 =
  scale + offset;
{
  "scale": 3,
  "offset": 4
}

The values are converted to Rex values using the parameter types. Runnable files without main use their final expression as the entry point, so their input shape is {}.

Modules and Imports

Rex modules are .rex files. Imports are semicolon-terminated top-level declarations. Module files are declaration-only: they do not have a top-level expression result. To evaluate an expression, run a source as a program entry point.

Supported forms:

import foo.bar as Bar;
import foo.bar (*);
import foo.bar (x, y as z);

Semantics:

  • import foo.bar as Bar imports a module alias; use qualified access (Bar.name).
  • Alias-qualified lookup is namespace-aware:
    • expression/pattern positions use exported values and constructors (Bar.value).
    • type positions use exported types (Bar.Type).
    • class-constraint positions use exported classes (Bar.Class).
  • import foo.bar (*) imports every exported name into local unqualified scope.
  • import foo.bar (x, y as z) imports selected exported names; y is bound locally as z.
  • Unqualified imports are context-sensitive:
    • expression/pattern positions use the imported value facet
    • type positions use the imported type facet
    • class-constraint positions use the imported class facet
  • Importing a name does not invent missing facets. For example, importing a type name does not make it usable as a value unless the module also exports a value with that same spelling.
  • A single exported name may carry multiple facets at once. ADTs commonly do this: Boxed can be both a type name and a constructor value.
  • Module alias imports and clause imports are mutually exclusive in one import declaration.
  • Only pub names are importable.
  • If two imports introduce the same unqualified name (including via (*)), resolution fails with a module error.
  • Importing a name that conflicts with a local top-level declaration is a module error.
  • Lexical bindings (let, lambda params, pattern bindings) can shadow imported names.
  • For binder forms with annotations, the annotation is resolved before the new binder name enters expression scope.

Examples:

import sample (Boxed);

let id: Boxed -> Boxed = \x -> x in
id (Boxed 1)

Here Boxed is imported once, but it can be used in both type position and expression position.

import sample (Status, Ready);

let id: Status -> Status = \x -> x in
id Ready

This only works if sample exports Status as a type and Ready as a value. Importing Status alone does not make Status available as an expression unless the module also exports a value named Status.

Path resolution:

  • foo.bar resolves to foo/bar.rex.
  • Local module paths resolve relative to the importing file.
  • Leading super path segments walk up directories (for example super.core.calc).

Lexical Structure

Whitespace and Comments

  • Whitespace, including newlines, is generally insignificant and indentation has no syntactic meaning. Top-level type, fn, and declare fn declarations, marker classes/instances, and class/instance items use explicit semicolon terminators.
  • Comments use // ... for line comments and /* ... */ for block comments. They are stripped before parsing.
  • Nested block comments are not supported in current Rex builds.

Identifiers and Operators

  • Identifiers start with a letter or _, followed by letters/digits/underscores.
  • Operators are non-alphanumeric symbol sequences (+, *, ==, <, …).
  • Operators can be used as values by parenthesizing: (+), (==), (<).

Lambdas

The lambda syntax is \x -> expr. Rex only accepts the ASCII spellings \ and ->.

Expressions

Literals

  • true, false
  • integers and floats (integer literals are overloaded over Integral and default to i32 when ambiguous)
  • strings: "hello"
  • UUID and datetime literals, when enabled by the parser

Examples:

( (4 is u8)
, (4 is u64)
, (4 is i16)
, (-3 is i16)
)

Negative literals only specialize to signed types. For example, (-3 is u8) is a type error.

Function Application

Application is left-associative: f x y parses as (f x) y.

let add = \x y -> x + y in add 1 2

Let-In

Let binds one or more definitions and then evaluates a body:

let
  x = 1 + 2,
  y = 3
in
  x * y

Let bindings are polymorphic (HM “let-generalization”):

let id = \x -> x in (id 1, id true, id "hi")

Integer-literal bindings are a special case: unannotated let x = 4 is kept monomorphic so use sites can specialize it through context.

let
  x = 4,
  f: u8 -> u8 = \y -> y
in
  f x

Recursive Let (let rec)

Use let rec for self-recursive and mutually-recursive bindings.

let rec
  even = \n -> if n == 0 then true else odd (n - 1),
  odd = \n -> if n == 0 then false else even (n - 1)
in
  (even 10, odd 11)

Notes:

  • Bindings in let rec are separated by commas.

If-Then-Else

if 1 < 2 then "ok" else "no"

Tuples, Lists, Dictionaries

(1, "hi", true)
[1, 2, 3]
{ a = 1, b = 2 }

Notes:

  • Lists are implemented as a List a ADT (Empty/Cons) in the prelude.
  • Cons expressions use :: (for example x::xs), equivalent to Cons x xs.
  • Cons is used with normal constructor-call syntax (Cons head tail), while :: is infix sugar.
  • Dictionary literals { k = v, ... } build record/dict values. They become records when used as the payload of an ADT record constructor, or when their type is inferred/annotated as a record.

:: is right-associative, so 1::2::[] means 1::(2::[]).

let
  xs = 1::2::3::[]
in
  xs

Pattern Matching

match performs structural matching. The scrutinee is followed by with, then one or more semicolon-terminated case arms inside a braced arm block:

match xs with {
  case Empty -> 0;
  case Cons h t -> h;
}

Patterns include:

  • wildcards: _
  • variables: x
  • constructors: Ok x, Cons h t, Pair a b
  • qualified constructors via module alias: Sample.Right x
  • list patterns: [], [x], [x, y]
  • cons patterns: h::t (equivalent to Cons h t)
  • dict key presence: {foo, bar} (keys are identifiers)
  • record patterns on record-carrying constructors: Bar {x, y}
match [1, 2, 3] with {
  case h::t -> h;
  case [] -> 0;
}

Rex checks ADT matches for exhaustiveness and reports missing constructors.

Types

Primitive Types

Common built-in types include:

  • bool
  • i32 (default integer-literal fallback type)
  • f32 (float literal type)
  • string
  • uuid
  • datetime

Function Types

Functions are right-associative: a -> b -> c means a -> (b -> c).

Tuples, Lists, Arrays, Dicts

  • Tuple type: (a, b, c)
  • List type: List a (prelude)
  • Array type: Array a (prelude)
  • Dict type: Dict a (prelude; key type is a symbol/field label at runtime)
  • Promise type: Promise a (built-in unary type constructor; embedders may attach their own operations)

ADTs

Define an ADT with type. Each top-level type declaration is terminated by a semicolon:

type Maybe a = Just a | Nothing;

Constructors are values (functions) in the prelude environment:

Just 1
Nothing

Record-Carrying Constructors

ADT variants can carry a record payload:

type User = User { name: string, age: i32 };

let u: User = User { name = "Ada", age = 36 } in u

Type Annotations

Annotate let bindings, lambda parameters, and function declarations:

let x: i32 = 1 in x

Annotations can mention ADTs and prelude types:

let xs: List i32 = [1, 2, 3] in xs

They can also use module-qualified type names:

import dep as D;
fn id x: D.Boxed -> D.Boxed = x;

Records: Projection and Update

Rex supports:

  • projection: x.field
  • record update: { base with { field = expr } }

Projection and update are valid when the field is definitely available on the base:

  • on plain record types { field: Ty, ... }
  • on single-variant ADTs whose payload is a record
  • on multi-variant ADTs only after the constructor has been proven (typically by match)

Example (multi-variant refinement via match):

type Sum = A { x: i32 } | B { x: i32 };

let s: Sum = A { x = 1 } in
match s with {
  case A {x} -> { s with { x = x + 1 } };
  case B {x} -> { s with { x = x + 2 } };
}

Declarations

Functions (fn)

Top-level functions are declared with an explicit type signature and a value (typically a lambda). Each top-level fn declaration is terminated by a semicolon:

fn add x: i32 -> y: i32 -> i32 = x + y;

Top-level fn declarations are mutually recursive, so they can refer to each other in the same module:

fn even n: i32 -> bool =
  if n == 0 then true else odd (n - 1);

fn odd n: i32 -> bool =
  if n == 0 then false else even (n - 1);

even 10

Type Classes (class)

Type classes declare overloaded operations. Method signatures live in the class:

class Size a where {
  size : a -> i32;
}

Classes with no methods are terminated with a semicolon:

class Marker a;

Methods can be operators (use parentheses to refer to them as values if needed):

class Eq a where {
  == : a -> a -> bool;
}

Superclasses use <= (read “requires”):

class Ord a <= Eq a where {
  < : a -> a -> bool;
}

Instances (instance)

Instances attach method implementations to a concrete head type, optionally with constraints:

class Size a where {
  size : a -> i32;
}
instance<t> Size (List t) where {
  size = \xs ->
    match xs with {
      case Empty -> 0;
      case Cons _ rest -> 1 + size rest;
    };
}

Instances with no method implementations are also terminated with a semicolon:

instance Marker i32;

The class in an instance header may be module-qualified:

import dep as D;

instance D.Pick i32 where {
  pick = 7;
}

Instance contexts use <=:

class Show a where {
  show : a -> string;
}
instance Show i32 where {
  show = \_ -> "<i32>";
}
instance<a> Show (List a) <= Show a where {
  show = \xs ->
    let
      step = \out x ->
        if out == "["
          then out + show x
          else out + ", " + show x,
      out = foldl step "[" xs
    in
      out + "]";
}

Notes:

  • Instance heads are non-overlapping per class (overlap is rejected).
  • Inside instance method bodies, the instance context is the only source of “given” constraints.

Prelude Type Classes (Selected)

Rex ships a prelude with common abstractions and instances. Highlights:

  • numeric hierarchy: AdditiveMonoid, Semiring, Ring, Field, …
  • Default (default) for common scalar and container types
  • Eq / Ord
  • Functor / Applicative / Monad for List, Array, Option, Result
  • Foldable, Filterable, Sequence
  • multi-parameter Indexable t a with instances for lists/arrays

Example: Functor across different container types:

( map ((*) 2) [1, 2, 3]
, map ((+) 1) (Some 41)
, map ((*) 2) (Ok 21)
)

Example: Indexable:

get 0 [10, 20, 30]

Defaulting (Ambiguous Types)

Rex supports defaulting for variables constrained by defaultable classes (for example AdditiveMonoid). This matters for expressions like zero where no concrete type is otherwise forced.

This defaulting pass is separate from the Default type class method default.

Example:

zero

With no other constraints, zero defaults to a concrete candidate type. See SPEC.md for the exact algorithm and candidate order.

Rex Spec (Locked Semantics)

This document records the intended, production-facing semantics of the current Rex implementation. When behavior changes, this file and the corresponding regression tests should be updated together.

Regression tests live in:

  • rex/tests/spec_semantics.rs
  • rex/tests/record_update.rs
  • rex/tests/typeclasses_system.rs
  • rex/tests/negative.rs

Notation

  • Γ ⊢ e : τ means “under type environment Γ, expression e has type τ”.
  • C τ means a typeclass predicate (constraint) for class C at type τ.
  • “Ground” means “contains no free type variables” (ftv(τ) = ∅).
  • Rex’s multi-parameter classes are represented internally by packing the parameters into tuples:
    • unary C a is Predicate { class: C, typ: a }
    • binary C t a is Predicate { class: C, typ: (t, a) }
    • etc.

Lexical Comments

Rex comments are lexical trivia and are removed before parsing:

  • // starts a line comment that runs to the next newline or end of file.
  • /* ... */ starts a block comment. Block comments may span lines.
  • Nested block comments are not supported.
  • The legacy {- ... -} spelling is ordinary syntax, not a comment.

String Literals

String literals are decoded during lexing.

  • Double-quoted ("...") and single-quoted ('...') literals both produce string values.
  • C-style simple escapes are supported: \a, \b, \f, \n, \r, \t, \v, \\, \", \', and \?.
  • Octal escapes use one to three octal digits (\0 through \777).
  • Hex escapes use \x followed by one or more hexadecimal digits.
  • Unicode escapes use \u followed by exactly four hexadecimal digits, or \U followed by exactly eight hexadecimal digits.
  • Backslash-newline is a line continuation and produces no character.
  • Unsupported or malformed escape sequences are lexical errors.

Program Entry Points

A Rex source is a compilation unit with zero or more declarations and an optional final expression. Entry-point execution uses a single program entry point:

  • If the source defines a top-level fn main, that function is the entry point. It is an error for the same source to also contain a final expression.
  • If the source does not define main, the final expression is treated as an implicit zero-argument entry point.
  • If the source does not define main and has no final expression, entry-point execution is an error.

The CLI supplies arguments to an explicit main from a JSON object passed with --inputs. The object keys must exactly match the main parameter names, and each value is converted with json_to_rex using the corresponding parameter type. JSON inputs require concrete parameter types. A runnable source without main uses its final expression as an implicit entry point and conceptually has the empty input object {}.

Module Imports

Rex distinguishes between:

  • program entry-point execution, and
  • module files used by the import system (declaration-only).

When a .rex file is loaded as a module via the module system, it must not contain a top-level expression result.

Syntax

Top-level imports support three forms:

import foo.bar as Bar;
import foo.bar (*);
import foo.bar (x, y, z as q);

Rules:

  • Import declarations are terminated by explicit semicolons.
  • import <module> as <Alias> imports the module namespace and requires qualified access (Alias.member).
  • import <module> (*) imports all exported values, types, and classes into unqualified scope.
  • import <module> (x, y as z) imports selected exported values, types, and classes into unqualified scope.
  • as <Alias> on the module and (...) import clauses are mutually exclusive.

Visibility and Exports

Only exported (pub) values, types, and classes are importable through (*) and item clauses.

Module aliases expose all export namespaces for qualified lookup:

  • Alias.value resolves against exported values (including constructors).

  • Alias.Type resolves against exported type names in type positions.

  • Alias.Class resolves against exported class names in class-constraint positions.

  • Missing requested exports are module errors.

  • Private (non-pub) values are not importable.

Name Binding and Conflicts

  • Imported unqualified names participate in lexical shadowing.
  • Lexically bound names (lambda params, let vars, pattern bindings) shadow imported names.
  • Importing a name that conflicts with a local top-level declaration is a module error.
  • Importing the same unqualified name more than once (including via aliasing) is a module error.

Type/class rewrites run with declaration ordering semantics:

  • In binder forms that carry type syntax (\ (x : T) -> ..., let rec f : T = ...), the binder being introduced does not suppress alias resolution inside its own annotation.
  • Missing alias members used in type/class positions (function signatures, annotations, where constraints, instance headers, and superclass clauses) are reported as module errors.

Module Initialization

  • Importing a module does not execute arbitrary top-level expressions.
  • Module initialization is declaration-driven: exported values/types/classes are registered from declarations, and import resolution rewrites references to canonical internal symbols.
  • Cyclic imports are supported via strongly connected component (SCC) loading of module interfaces.

Let Rec Bindings

Syntax

Recursive bindings use let rec with comma-separated entries:

let rec
  a = ...,
  b = ...
in
  body

Rules:

  • let rec entries are separated by commas.
  • let rec bindings must bind variables (not arbitrary patterns).

Top-Level Declaration Terminators

Top-level type, fn, declare fn, and import declarations are terminated by explicit semicolons:

import math.core as Math;
type Box a = Box a;
fn inc x: i32 -> i32 = x + 1;
declare fn host_value : i32;

Rules:

  • The semicolon terminates the declaration, not a nested type or expression itself.
  • The terminating semicolon is found at top-level expression/type depth; semicolons nested inside parentheses, brackets, braces, or blocks do not terminate the declaration.
  • Indentation and newlines do not delimit declarations.

Explicit Type Parameters

Type variables used in annotations, constraints, class heads, or instance heads must be declared by the syntactic form that binds them.

Examples:

type Box a = Box a;
fn id<a> x: a -> a = x;
declare fn host_id<a> x: a -> a;
let id<a>: a -> a = \x -> x in id 1
class Size a where { size : a -> i32; }
instance<a> Show (List a) <= Show a where { show = prim_show; }

Rules:

  • A bare unknown type name is an error, even when it starts with a lowercase letter.
  • Top-level fn, declare fn, named let, class methods, and instance methods bind type parameters with <...> after the value name.
  • type and class declarations bind type parameters with whitespace after the declaration head.
  • instance declarations bind type parameters with <...> immediately after instance.

Top-Level fn Recursion

Top-level fn declarations are mutually recursive within a module.

This means:

  • A top-level fn may reference itself.
  • A top-level fn may reference other top-level fn declarations in the same module, regardless of declaration order.

Operationally, top-level fn recursion follows the same fixed-point semantics as recursive bindings in let rec, but at declaration scope.

Record Projection

Syntax

Field projection is an expression:

base.field

Typing (Definite Fields)

Let Γ ⊢ base : T. Projection is well-typed iff the field is definitely available on T:

  1. If T is a record type { ..., field : τ, ... }, then Γ ⊢ base.field : τ.
  2. If T is a single-variant ADT whose payload is a record containing field : τ, then Γ ⊢ base.field : τ.
  3. If T is a multi-variant ADT, projection is accepted only if the typechecker can prove the current constructor is a specific record-carrying variant (typically via match refinement or by tracking known constructors through let-bound variables).

If the typechecker cannot prove the constructor for a multi-variant ADT, the field is considered “not definitely available”, and projection is rejected.

Evaluation

Evaluation is strict in base. At runtime, projection reads the field out of the record payload:

  • for plain records/dicts, it indexes the map by the field symbol.
  • for record-carrying ADT values, it indexes the payload record/dict.

Missing fields are a runtime error (EngineError::UnknownField) when projection is attempted on a non-record-like value.

Record Update

Syntax

Record update is an expression:

{ base with { field1 = e1, field2 = e2 } }

Typing (Definite Fields)

Let Γ ⊢ base : T. Record update is well-typed iff:

  1. Each updated field exists on the definite record shape of T.
  2. T is one of:
    • a record type { field: Ty, ... }, OR
    • a single-variant ADT whose payload is a record, OR
    • a multi-variant ADT after the expression has been refined to a specific record-carrying constructor (the typechecker tracks this refinement).
  3. For each update fieldᵢ = eᵢ, the update expression unifies with the declared field type.

If the base type is a multi-variant ADT and the typechecker cannot prove the current constructor, record update is rejected (the field is “not definitely available”).

Typing: Known-Constructor Refinement

The typechecker refines “which constructor is known” via two mechanisms:

  1. Pattern matching: within a case K { ... } -> ... arm, the scrutinee is known to be K.
  2. Let-bound known constructors: when a variable is bound to a value constructed with a record-carrying constructor, the variable may carry “known variant” information forward.

This enables the common pattern:

type Sum = A { x: i32 } | B { x: i32 };

let s: Sum = A { x = 1 } in
match s with {
  case A {x} -> { s with { x = x + 1 } };
  case B {x} -> { s with { x = x + 2 } };
}

Evaluation

Evaluation is strict:

  1. Evaluate base to a value.
  2. Evaluate all update expressions (left-to-right in the implementation’s map iteration order).
  3. Apply updates:
    • If base is a plain record/dict value, updates replace existing fields.
    • If base is an ADT whose payload is a record/dict, updates replace fields in the payload and re-wrap the constructor tag.

Runtime errors:

  • Updating a non-record-like runtime value is EngineError::UnsupportedExpr.

Type Classes: Coherence, Resolution, and Ambiguity

Instance Coherence (No Overlap)

For each class C, instance heads are non-overlapping:

  • When injecting a new instance head H, it is rejected if it unifies with any existing head for the same class C.

This forbids overlap and preserves deterministic method resolution.

Regression: spec_typeclass_instance_overlap_is_rejected (rex/tests/spec_semantics.rs).

Qualified Class Names in instance Headers

The class name in an instance header may be qualified through a module alias:

import dep as D;

instance D.Pick i32 where {
  pick = 7;
}

The alias member must be an exported class from the referenced module; otherwise import-use validation fails before typechecking/evaluation.

Method Resolution (Runtime)

At runtime, class methods are resolved by unification against the inferred call type.

Let m be a class method, and let its call site be typed with monomorphic call type τ_call.

Resolution:

  1. Determine the “instance parameter type” for the method by unifying τ_call with the method’s scheme and extracting the predicate corresponding to the method’s defining class.
  2. If the instance parameter type is still headed by a type variable (not ground enough to pick an instance), the use is ambiguous:
    • If m is used as a function value (i.e. τ_call is a function type), the engine returns an overloaded function value and defers resolution until the function is applied with concrete arguments.
    • If m is used as a value (non-function), the engine errors (EngineError::AmbiguousOverload).
  3. If exactly one instance head unifies with the instance parameter type, its method body is specialized and evaluated.
  4. If none match, the engine errors (EngineError::MissingTypeclassImpl).
  5. If more than one match (should not occur given non-overlap), the engine errors (EngineError::AmbiguousTypeclassImpl).

Regression: spec_typeclass_method_value_without_type_is_ambiguous (rex/tests/spec_semantics.rs).

Overloaded Method Values (Deferred Resolution)

If a class method is used as a function value, the engine may defer instance selection until the function is applied with concrete argument types. This supports idioms like:

let f = map ((+) 1) in
  ( f [1, 2, 3]
  , f (Some 41)
  )

Here f is polymorphic over the Functor dictionary; at each call site, the engine resolves map using the argument type (List i32 vs Option i32) and dispatches to the corresponding instance method body.

Instance-Method Checking (Static)

Inside an instance method body, only the instance context is available as “given” constraints:

  • Given predicates start with the instance’s explicit context.
  • The superclass closure of that context is added (repeat until fixed point).
  • The instance head itself is also considered given (dictionary recursion).

Rules:

  • Ground predicates required by the method body must be entailed by the given set (via instance search).
  • Non-ground predicates are not resolved by instance search (that would be unsound); they must appear explicitly in the instance context.

This is what makes instance methods predictable and prevents “magical” selection based on unifying type variables with arbitrary instance heads.

Integer Literals

Integer literals are overloaded over integral types.

  • A literal like 4 introduces a fresh type variable α with predicate Integral α.
  • A negative literal like -3 introduces α with predicates Integral α and AdditiveGroup α (so it can only specialize to signed numeric types).
  • Binary subtraction uses Subtractive, which includes unsigned integer types. Unary negation still requires AdditiveGroup.
  • Division uses Divisive, which includes primitive integer and floating-point types. Integer division follows Rust’s integer division semantics.
  • Integer +, -, *, /, and % are checked at runtime for primitive integer types. Arithmetic overflow raises integer overflow (T) and arithmetic underflow raises integer underflow (T), where T is the concrete integer type.
  • Context can specialize α (for example, let x: u64 = 4 in x).
  • Unannotated let bindings whose definition is an integer literal are kept monomorphic. This lets use sites specialize the binding consistently in that scope (for example, let x = 4 in (x + 1, x + 2)).
  • If α remains ambiguous, normal defaulting rules apply.

Examples:

let x: u8 = 4 in x
let f: i64 -> i64 = \x -> x in f 4
let x = 4 in (x is u16)
let x: i16 = -3 in x

Attempting to use a negative literal at an unsigned type is a type error (for example let x: u8 = -3 in x).

Float Literals

Float literals are overloaded over primitive floating-point types.

  • A literal like 3.0 introduces a fresh type variable α with predicate Field α.
  • Context can specialize α to f32 or f64 (for example, let x: f64 = 3.0 in x).
  • If α remains ambiguous, normal defaulting rules choose f32.
  • Unannotated let bindings whose definition is a float literal are kept monomorphic, matching integer literal bindings.
  • Float literals do not imply integer-to-float coercions. A mixed expression such as 1 + 2.0 is still a type error unless the values are explicitly converted by user code.

Examples:

let x: f64 = 3.0 in x
let f: f64 -> f64 = \x -> x in f 3.0
let x = 3.0 in (x is f32)

Defaulting

Defaulting runs after type inference and before evaluation.

Eligible Variables

A type variable α is eligible for defaulting iff:

  • α appears only in simple predicates of the form C α (not in compound types), and
  • at least one such C is in the numeric defaultable set: AdditiveMonoid, MultiplicativeMonoid, Subtractive, AdditiveGroup, Ring, Divisive, Field, Integral.

Eq and Ord are allowed as companion predicates when a numeric defaultable predicate is also present. They do not make a type variable defaultable on their own. This lets expressions like if x == 0.0 then ... default through the float literal’s Field predicate without making unconstrained equality default to an arbitrary numeric type.

If α appears in any non-simple predicate or any non-defaultable class predicate, it is not defaulted.

Candidate Types (Order Matters)

The candidate list is constructed in this order:

  1. Traverse the typed expression (depth-first) and collect every concrete (ground) 0-arity type constructor that appears as the type of a subexpression (unique, in first-seen order).
  2. Append (if not already present): f32, i32, string.

Choosing a Default

For an eligible variable α with required predicates { C₁ α, ..., Cₙ α }, choose the first candidate type T such that all predicates are satisfied in the empty context:

entails([], Cᵢ T) for all i

If no candidate satisfies all predicates, α remains ambiguous.

Example: zero (type α with AdditiveMonoid α) defaults to f32 when no other concrete type is present:

zero

Regression: spec_defaulting_picks_a_concrete_type_for_numeric_classes (rex/tests/spec_semantics.rs).

Architecture

Rex is implemented as a small set of focused crates that form a pipeline:

  1. Parsing (rex-parser): converts source text into a rex_ast::CompilationUnit { decls, body }.
  2. Typing (rex-typesystem): Hindley–Milner inference + ADTs + type classes; produces a rex_typesystem::TypedExpr.
  3. Execution (rex-engine): builds the host environment, prepares typed code into a CompiledProgram, and evaluates it to a runtime rex_engine::Handle.

The crates are designed so you can use them independently (e.g. parser-only tooling, typechecking-only checks, or embedding the full evaluator).

Crates

  • rex-ast: shared AST types (Expr, Pattern, Decl, TypeExpr, CompilationUnit, symbols, spans).
  • rex-parser: source parser. Entry point: rex_parser::parse.
    • Parsing enforces a fixed cap on AST nesting.
  • rex-typesystem: type system. Entry points:
    • TypeSystem::new() to create an explicit typing environment.
    • infer_typed(&mut ts, expr) / infer(&mut ts, expr) for type inference.
    • The inference implementation itself lives in rex-typesystem/src/inference.rs; typesystem.rs now holds the shared core types, environments, and registration logic.
    • For untrusted code, set rex_typesystem::TypeSystemLimits::safe_defaults() before inference.
  • rex-engine: host environment builder, compiler, and runtime evaluator. Entry points:
    • Engine::with_prelude(state)? to inject runtime constructors and builtin implementations (state can be ()).
    • standard_type_system()? to create a typing environment with the engine-owned standard prelude.
    • Engine::into_compiler() to consume the prepared engine into a compilation view.
    • Engine::into_evaluator() / Compiler::into_evaluator() to consume preparation state into an evaluator.
    • Compiler::compile_program to prepare a parsed program entry point into CompiledProgram; Compiler::infer_* for type-only checks.
    • Evaluator::run(compiled, inputs).await to execute one prepared program. inputs is a BTreeMap<String, Handle> for the program’s external main interface; run consumes the evaluator, compiled program, and input map.
    • Engine carries host state as Engine<State> (State: Clone + Send + Sync + 'static); typed export callbacks receive &State and return Result<T, EngineError>, typed export_async callbacks receive &State and return Future<Output = Result<T, EngineError>>, while handle-based native APIs (export_native*) receive Context<State>.
    • compile and evaluation APIs return EngineError; convenience entry points that cross phases return ExecutionError.
    • Host module injection API: Module + Export + Engine::inject_module.
  • rex-proc-macro: #[derive(Rex)] bridge for Rust types ↔ Rex ADTs/values.
  • rex: CLI front-end around the pipeline.
  • rex-lsp / rex-vscode: editor tooling.

rex-engine is organized internally around the same phases:

  • builder/ owns engine construction, module injection, import qualification/rewrite, host export registration, and registry markdown.
  • compiler/ owns typechecking and CompiledProgram construction.
  • evaluator/ owns execution, scheduling, native dispatch, Context, and the runtime core.
  • modules/, value.rs, and config.rs hold shared module identities, heap values/GC roots, and runtime options.

Design Notes

  • Typed preparation: rex-engine prepares code into a typed form before execution. The current CompiledProgram stores a typed AST plus the environment snapshot needed to run it.
  • Single-shot execution: evaluation is intentionally one-shot. CompiledProgram is moved into Evaluator::run with its runtime input map, consuming the evaluator as well. Prepare all required declarations/modules before constructing or consuming the evaluator.
  • Same-lineage runtime model: a CompiledProgram is intended to run on the evaluator produced from the same compiler. Rex programs are supplied as source and compiled per run, so the engine does not expose a portable compiled-artifact or cross-runtime linking model.
  • Prelude ownership: rex-engine owns the standard prelude source, standard typing environment, and runtime contract. The split is:
    • typeclass and instance declarations written in Rex at rex-engine/src/prelude/typeclasses.rex
    • rex-engine/src/prelude/type_system.rs builds the prelude-enabled TypeSystem, including ADTs, parsed declarations, and primop schemes
    • rex-engine/src/prelude/mod.rs parses the Rex source and injects runtime method bodies/native implementations for Engine::with_prelude(state)?
    • rex-typesystem exposes generic registration/inference APIs and does not own the standard prelude
  • Depth bounding: Some parts of the pipeline are naturally recursive (parsing deeply nested parentheses, matching deeply nested terms). The parser enforces a fixed AST-depth cap, and the typechecker-limit API provides bounded recursion for production/untrusted workloads.
  • Import-use rewrite/validation: module processing resolves import aliases across expression vars, constructor patterns, type references, and class references; unresolved qualified alias members are rejected as module errors before runtime.

Intentional String Boundaries

Rex now prefers structured internal representations (for example NameRef, BuiltinTypeId, CanonicalSymbol, and module/type/class maps) across parser, type system, evaluator, and LSP rewrite paths. Remaining string usage is intentional in these boundary layers:

  • Source text and parsing: the parser accepts source strings by definition.
  • Human-facing diagnostics and display: error messages, hover text, CLI rendering, and debug output stringify symbols/types for readability.
  • Protocol/serialization boundaries: JSON/LSP payloads are string-based and convert structured internal symbols/types at the edge.
  • Filesystem/module specifiers: import specifiers and path labels are textual before being resolved into structured module identities.

Non-goal for this pass:

  • Eliminating all .to_string() calls globally. The design target is to avoid stringly-typed core semantics, not to remove string conversion at UI/protocol boundaries.

Memory Management

rex-engine uses a heap-based runtime: evaluated values live in a central heap, and the internal evaluator passes lightweight pointers to those heap entries. The heap now includes a copying collector, so internal pointers can move during allocation.

This gives the engine a clear separation between identity and storage without exposing raw heap pointers to embedders. Public API code works with rooted Handle values, while Pointer remains an internal representation detail.

Design goals and rationale

  • Support graph-shaped runtime data, including cycles.
  • Keep allocation and dereference rules explicit and centralized.
  • Make host integration predictable by using stable handles rather than implicit deep copies.
  • Preserve strong runtime safety checks for pointer validity and heap ownership.
  • Keep diagnostics (type names, debug/display output, equality) correct for heap graphs.
  • Allow unreachable runtime objects to be reclaimed without exposing raw moving pointers to embedders.

Core runtime model

Pointer is an internal stable pointer

A Pointer identifies a slot in a heap using:

  • heap_id
  • index
  • generation

Conceptually:

  • index selects a slot.
  • generation distinguishes different occupants of the same slot over time.
  • heap_id prevents accidental cross-heap usage.

Pointer is intentionally crate-private. The engine validates it on access, so stale pointers and cross-heap usage fail deterministically inside the runtime. Because collection is copying, any raw pointer from before a collection is stale unless it has been rewritten through a traced runtime structure.

Handle is the public rooted value reference

A Handle owns a temporary external heap root for one value. Cloning the handle clones that root handle, and dropping the final clone unregisters it.

Host code can:

  • inspect a value with Handle::value(), which returns a Value.
  • convert to Rust with Handle::to_rust() or FromRex::from_rex(...).
  • display/debug/compare values through handle methods.

Host code cannot extract or store a raw runtime pointer.

Heap stores all runtime values

Heap owns an internal HeapState with object slots, external root slots, root-slot reuse state, and GC scheduling metadata.

  • object slots store runtime cells
  • root slots store public Handle roots and temporary roots
  • GC metadata tracks the next collection threshold and collection count

Each HeapSlot stores:

  • generation: u64
  • cell: Option<Cell>

Internal runtime reads/writes go through heap methods. Public construction uses Heap::alloc_*, which returns Handle values rather than raw pointers.

Runtime heap lifecycle

Engine constructs the initial Heap during preparation (Engine::new, Engine::with_prelude). When an engine is converted into a Compiler and then an Evaluator, the evaluator runtime core and compiler state share the same heap handle.

  • Evaluation returns Handle, not Value.
  • Callers can inspect via the returned handle or allocate more values from native callbacks through Context::heap().

This keeps allocation authority clear: the preparation phase creates the heap, and execution uses the evaluator runtime core’s shared heap store.

Copying collection and roots

Every public Heap::alloc_* call may run collection before allocating the requested object. Collection starts from registered roots, copies reachable objects into a new slot vector, rewrites roots and traced child pointers, and increments each moved object’s generation. Old raw pointers are intentionally invalid after collection.

Roots come from:

  • public Handle values returned to host code
  • temporary roots used while constructing composite heap cells
  • evaluator frames and scheduler tasks that trace and rewrite their internal pointers
  • runtime environments, closures, native functions, and overloaded-function records stored in live heap cells

This is why public APIs return handles. A Handle owns an external heap root, remains valid across later allocations and await points, and resolves to the current post-GC pointer when the runtime needs to dereference it.

Read/write semantics

Public reads return Value

Handle::value() returns Value, a safe public value of the runtime value. Composite values contain child Handle values rather than raw pointers.

Why:

  • Avoid accidental deep clones in hot paths.
  • Keep internal runtime values and heap pointers out of the public API.
  • Root child values discovered during inspection.

Writes are controlled

Public values are created through Heap::alloc_* methods, which return Handle.

There is also an internal overwrite operation used for recursive initialization patterns (placeholder first, then finalized value). Runtime code that holds crate-private pointers across allocation must protect them with handles, temporary roots, or traced frame/task state.

Equality, debug, and display are heap-aware

Structural operations are provided as heap-aware helpers:

  • Handle::debug()
  • Handle::display() / Handle::display_with(...)
  • Handle::value_eq(...)

These functions dereference through the heap and are cycle-safe (visited-set based), so recursive graphs can be inspected and compared without infinite recursion. They operate through handles, so they stay valid even if allocation has moved the underlying objects since the handle was created.

Handle-first host/native boundary

Runtime conversion traits are handle-centric:

  • IntoRex
  • FromRex

Public native injection paths pass handles, including module runtime exports (export_native / export_native_async). These callbacks receive Context<State>, so they can allocate public handles through engine.heap() and inspect host state via engine.state(). Value is used where direct payload inspection is required.

This keeps ownership/allocation behavior centralized in the heap while making it impossible for host code to store unrooted raw pointers.

Safety and invariants

At runtime, the heap enforces:

  • Wrong-heap pointer rejection (heap_id mismatch).
  • Invalid/stale pointer rejection (index/generation mismatch).
  • Type-aware errors via heap-driven type_name.
  • Root validation for public handles and temporary roots.
  • Debug-build verification that copied objects are rooted and all traced child pointers are valid after collection.

No unsafe code is used for this memory model.

Scope and limitations

  • This is a moving, copying heap with automatic collection; embedders should treat object location as completely opaque.
  • There is no public manual GC or heap-tuning API. Test-only hooks can force collection, but production callers only observe stable Handle behavior.
  • Pointer, Cell, temporary roots, and trace/rewrite plumbing remain crate-private runtime machinery.

In short, memory management is centered on explicit heap ownership, rooted public handles, validated moving pointers, and cycle-safe graph traversal.

Embedding Rex in Rust

Rex is designed as a small pipeline you can embed at whatever stage you need:

  1. rex-parser: source → CompilationUnit { decls, body }
  2. rex-typesystem: HM inference + type classes → TypedExpr (plus predicates/type)
  3. rex-engine: build host modules, compile typed code into CompiledProgram, then run it → rex_engine::Handle

This document focuses on common embedding patterns.

Running Untrusted Rex Code (Production Checklist)

This repo provides language-level parsing limits and a pure evaluator suitable for embedding. Your production server is responsible for enforcing hard resource limits (process isolation, wall-clock timeouts, memory limits).

Recommended defaults for untrusted input:

  • Parsing enforces a fixed AST-depth cap.
  • Run evaluation in an isolation boundary you can hard-kill (separate process/container), with CPU/RSS/time limits.

Evaluation API:

  • Evaluation is async via Evaluator.

Compile Then Run

rex-engine now has an explicit preparation boundary:

  • Engine builds the host environment.
  • Compiler prepares user code into a CompiledProgram.
  • Evaluator owns the runtime core and runs one prepared program with runtime inputs for main.

Evaluator is single-shot: Evaluator::run consumes the evaluator, the compiled program, and a BTreeMap<String, Handle> of inputs. Programs are compiled with Rex’s singular external interface semantics: an explicit fn main ... defines named runtime inputs, while a final expression without main is treated as an implicit zero-input main.

use rex::{
    engine::{CompileOptions, Engine},
    parser::parse,
};

let engine = Engine::with_prelude(())?;
let mut compiler = engine.into_compiler();

let parsed = parse("let x = 1 + 2 in x * 3").map_err(|errs| format!("{errs:?}"))?;
let program = compiler
    .compile_program(&parsed, CompileOptions::default())
    .await?;
assert_eq!(program.result_type().to_string(), "i32");
let evaluator = compiler.into_evaluator();
let value = evaluator.run(program, Default::default()).await?;

What “compiled” means in the current design:

  • parsing, import rewriting, declaration injection, and typechecking have already happened
  • CompiledProgram carries a typed expression plus the environment snapshot needed to run it
  • CompiledProgram::main_signature() reports input names/types and the external result type
  • Evaluator owns the runtime core needed for execution
  • Evaluator::run consumes the evaluator, compiled program, and runtime input map; use a new engine/compiler/evaluator for another generated workflow

What is captured:

  • Rex declarations that are part of the prepared program are captured into the compiled env snapshot
  • host-provided exports registered through export, export_async, export_native, export_native_async, or export_value are carried by the evaluator produced from the same compiler
  • typeclass method bindings are carried by that same evaluator runtime

That means a CompiledProgram is intended to be run by the evaluator created from the same compiler. Rex does not currently expose a portable compiled artifact or cross-runtime linking model.

Phase-specific errors:

  • Compiler APIs return EngineError
  • Evaluator::run returns EngineError
  • APIs that parse, compile, and run in one call return ExecutionError because they cross phase boundaries

Compile parsed Rex sources with Compiler::compile_program and pass the resulting CompiledProgram to Evaluator::run.

Evaluate Rex Code Directly

use rex::{
    engine::Engine,
    parser::parse,
};

let program = parse("let x = 1 + 2 in x * 3").map_err(|errs| format!("{errs:?}"))?;

let engine = Engine::with_prelude(())?;
let mut compiler = engine.into_compiler();
let program = compiler.compile_program(&program, Default::default()).await?;
let evaluator = compiler.into_evaluator();
let value = evaluator.run(program, Default::default()).await?;
println!("{value}");

Module sources loaded via importers must be declaration-only. To run an expression, use snippet or program entry points. Qualified alias members used in type/class positions (annotations, where constraints, instance headers, superclass clauses) are validated against module exports during module processing; missing exports fail early with module errors.

Engine Initialization and Default Imports

Engine::with_prelude(state) is shorthand for Engine::with_options(state, EngineOptions::default()).

  • Prelude is enabled by default.
  • Prelude is default-imported.
  • Default imports are weak: they fill missing names, but never override local declarations or explicit imports.

If you want full control:

use rex::engine::{Engine, EngineOptions, PreludeMode};

let mut engine = Engine::with_options(
    (),
    EngineOptions {
        prelude: PreludeMode::Disabled,
        default_imports: vec![],
    },
)?;

Inject Modules (Embedder Patterns)

This is fully supported in rex-engine. You can compose module loading from:

  • bundled stdlib imports (std.*)
  • modules injected with Engine::inject_module
  • custom async importers (for DB/object-store/in-memory modules)

1) Use an Explicit Importer

rex-engine does not read module files from disk by default. File-backed loading is a host policy decision; the CLI installs its own filesystem importer, while embedded applications should provide an importer that matches their trust boundary. Use DenyImporter when you need an explicit importer implementation that rejects every module request.

Notes:

  • importers receive an ImportRequest with the requested module name and the importing module id.
  • snippets and parsed programs load declaration-only modules through the compiler’s import rewriting path; module source itself remains declaration-only.
  • import clauses ((*) / item lists) import exported names into unqualified scope.
  • unqualified imports are context-sensitive: expression positions use values, type positions use types, and class/constraint positions use classes.
  • module aliases (import x as M) provide qualified access to exported values, types, and classes.
  • importing a name only brings in the facets that actually exist under that name.

2) Inject In-Memory Rex Modules

For host-managed modules, either call Engine::inject_module or add an importer that maps module_name to source text.

use futures::future::BoxFuture;
use rex::{
    engine::{
        CompileOptions, Engine, ImportRequest, Importer, ModuleId, ResolvedModule,
        ResolvedModuleContent,
    },
    parser::parse,
};
use std::collections::HashMap;
use std::sync::Arc;

let mut engine = Engine::with_prelude(())?;

let modules = Arc::new(HashMap::from([
    (
        "acme.math".to_string(),
        "pub fn inc : i32 -> i32 = \\x -> x + 1;".to_string(),
    ),
    (
        "acme.main".to_string(),
        "import acme.math (inc);\npub fn main : i32 = inc 41;".to_string(),
    ),
]));

struct MapImporter {
    modules: Arc<HashMap<String, String>>,
}

impl Importer for MapImporter {
    fn import<'a>(
        &'a self,
        req: ImportRequest,
    ) -> BoxFuture<'a, Result<Option<ResolvedModule>, rex::engine::EngineError>> {
        Box::pin(async move {
            let Some(source) = self.modules.get(&req.module_name) else {
                return Ok(None);
            };
            Ok(Some(ResolvedModule {
                id: ModuleId::Virtual(format!("host:{}", req.module_name)),
                content: ResolvedModuleContent::Source(source.clone()),
            }))
        })
    }
}

engine.add_importer("host-map", Arc::new(MapImporter { modules }));
let mut compiler = engine.into_compiler();
let parsed = parse("import acme.main (main);\nmain").map_err(|errs| format!("{errs:?}"))?;
let program = compiler
    .compile_program(&parsed, CompileOptions::default())
    .await?;
let value = compiler.into_evaluator().run(program, Default::default()).await?;
println!("{value}");

3) Host-Provided Rust Functions, Exposed as Modules

This is the common embedder case.

Use Module + Engine::inject_module(...):

  1. Create a Module.
  2. Add exports:
    • typed exports with export / export_async
    • runtime/native exports with export_native / export_native_async
    • optional structured declarations with add_rex_adt / add_adt_decl
  3. Inject it into the engine.

Module::add_rex_adt::<T>() now stages the full acyclic ADT family reachable from T. This is driven by RexType::collect_rex_family(...): ADT types contribute declarations there, while leaf Rex types inherit a no-op default. For example, if Label contains a Side, staging Label is enough; you do not need to stage Side separately. Cyclic ADT families are still rejected.

Module also exposes its staged decls, adts, and exports vectors directly. That is useful if you want to inspect, transform, or assemble a module in multiple passes before calling Engine::inject_module.

export handlers are fallible and must return Result<T, EngineError>. If a handler returns Err(...), evaluation fails with that engine error. export_async handlers follow the same rule, but return Future<Output = Result<T, EngineError>>.

use rex::{
    engine::{CompileOptions, Engine, Module},
    parser::parse,
};

let mut engine = Engine::with_prelude(())?;

let mut math = Module::new("acme.math");
math.export("inc", |_state: &(), x: i32| { Ok(x + 1) })?;
math.export_async("double_async", |_state: &(), x: i32| async move { Ok(x * 2) })?;
engine.inject_module(math)?;
let mut compiler = engine.into_compiler();
let parsed = parse("import acme.math (inc, double_async as d);\ninc (d 20)")
    .map_err(|errs| format!("{errs:?}"))?;
let program = compiler
    .compile_program(&parsed, CompileOptions::default())
    .await?;
let value = compiler.into_evaluator().run(program, Default::default()).await?;
println!("{value}");

You can declare ADTs directly inside an injected host module:

use rex_ast::Symbol;
use rex_engine::{Engine, Module};
use rex_typesystem::types::{BuiltinTypeId, Type};

let mut engine = Engine::with_prelude(())?;

let mut m = Module::new("acme.status");
let mut status = engine.adt_decl("Status", &[]);
status.add_variant(Symbol::intern("Ready"), vec![]);
status.add_variant(
    Symbol::intern("Failed"),
    vec![Type::builtin(BuiltinTypeId::String)],
);
m.add_adt_decl(status)?;
engine.inject_module(m)?;

Then Rex code can import and use those names from the module:

import acme.status (Status, Failed);

let fail: string -> Status = \msg -> Failed msg in
match (fail "boom") with {
  case Failed msg -> length msg;
  case _ -> 0;
}

Status is used here in type position, while Failed is used in expression/pattern positions. They are imported through the same name-based mechanism.

Internally this generates module declarations and injects host implementations under qualified module export symbols.

If you need to construct exports separately (for example to build a module from plugin metadata), you can use:

  • Export::from_handler / Export::from_async_handler (typed handlers)
  • Export::from_native / Export::from_native_async (handle-based native handlers)

Then add them via Module::add_export, or push them into Module::exports directly if you are assembling the module programmatically.

This example shows how to use Rust enums and structs as Rex-facing types with ADTs declared inside the module itself. The host function accepts a Rust Label (containing a Rust Side enum), and Rex code calls it through sample.render_label.

Example:

use rex::{
    Rex,
    engine::{CompileOptions, Engine, EngineError, Module},
    parser::parse,
};

#[derive(Clone, Debug, PartialEq, Rex)]
enum Side {
    Left,
    Right,
}

#[derive(Clone, Debug, PartialEq, Rex)]
struct Label {
    text: String,
    side: Side,
}

fn render_label(label: Label) -> String {
    match label.side {
        Side::Left => format!("{:<12}", label.text),
        Side::Right => format!("{:>12}", label.text),
    }
}

let mut engine = Engine::with_prelude(())?;

let mut m = Module::new("sample");
m.add_rex_adt::<Label>()?;
m.export("render_label", |_state: &(), label: Label| {
    Ok::<String, EngineError>(render_label(label))
})?;
engine.inject_module(m)?;
let mut compiler = engine.into_compiler();
let parsed = parse(
    r#"
    import sample (Label, Left, Right, render_label);
    (
        render_label (Label { text = "left", side = Left }),
        render_label (Label { text = "right", side = Right })
    )
    "#,
)
.map_err(|errs| format!("{errs:?}"))?;
let program = compiler
    .compile_program(&parsed, CompileOptions::default())
    .await?;
let value = compiler.into_evaluator().run(program, Default::default()).await?;
println!("{value}"); // ("left        ", "       right")

In that example:

  • Label is imported once and then used as both a type name and a constructor value.
  • Left and Right are imported as constructor values.
  • render_label is imported as a value.

3a) Runtime-Defined Signatures (Handle APIs)

If your host determines function signatures/behavior at runtime, use the native module export APIs and provide an explicit Scheme + arity:

  • Module::export_native
  • Module::export_native_async

These callbacks receive Context<State> (not just &State), so they can:

  • read state via engine.state()
  • allocate new values via engine.heap()
  • inspect typed call information via the explicit &Type / Type callback parameter

Async native callbacks receive owned argument vectors and return Send + 'static futures so the runtime can suspend them as explicit pending evaluation frames.

use futures::FutureExt;
use rex_engine::{Engine, Context, Handle, Module};
use rex::typesystem::{BuiltinTypeId, Scheme, Type};

let mut engine = Engine::with_prelude(())?;

let mut m = Module::new("acme.dynamic");
let scheme = Scheme::new(vec![], vec![], Type::fun(Type::builtin(BuiltinTypeId::I32), Type::builtin(BuiltinTypeId::I32)));

m.export_native("id_handle", scheme.clone(), 1, |_ctx: Context<()>, _typ: &Type, args: &[Handle]| {
    Ok(args[0].clone())
})?;

m.export_native_async("answer_async", Scheme::new(vec![], vec![], Type::builtin(BuiltinTypeId::I32)), 0, |ctx: Context<()>, _typ: Type, _args: Vec<Handle>| {
    async move { ctx.heap().alloc_i32(42) }.boxed()
})?;

engine.inject_module(m)?;

Scheme and arity must agree. Registration returns an error if the type does not accept the provided number of arguments.

4) Custom Importer Contract (Advanced)

If you need dynamic/nonstandard module loading behavior, implement Importer.

Importer contract:

  • return Ok(Some(ResolvedModule { ... })) when you can satisfy the module.
  • return Ok(None) to let the next importer try.
  • return Err(...) for hard failures (invalid module payload, policy violations, etc.).

ResolvedModule can carry either ResolvedModuleContent::Source(...) for real Rex source or ResolvedModuleContent::CompilationUnit(...) for preconstructed structured modules.

5) Snippets That Import Relative Modules

If you evaluate ad-hoc Rex snippets that contain imports, parse the snippet and pass an importer path in CompileOptions for Compiler::compile_program. For type-only checks through Compiler::infer_snippet, pass the same importer path argument there:

use rex::{
    engine::CompileOptions,
    parser::parse,
};

let mut compiler = engine.into_compiler();
let parsed = parse("import foo.bar as Bar;\nBar.add 1 2")
    .map_err(|errs| format!("{errs:?}"))?;
let program = compiler
    .compile_program(
        &parsed,
        CompileOptions::default()
            .with_importer_path(std::path::Path::new("/tmp/workflow/_snippet.rex")),
    )
    .await?;
let value = compiler.into_evaluator().run(program, Default::default()).await?;

Engine State

Engine is generic over host state: Engine<State>, where State: Clone + Send + Sync + 'static. The state is stored as engine.state: Arc<State> and is shared across all injected functions.

  • Use Engine::with_prelude(())? if you do not need host state.
  • If you do, pass your state struct into Engine::new(state) or Engine::with_prelude(state).
  • export / export_async callbacks receive &State as their first parameter.
  • Handle-based native APIs (export_native*) receive Context<State> so they can allocate public handles through the heap and read engine.state().
use rex_engine::Engine;

#[derive(Clone)]
struct HostState {
    user_id: String,
    roles: Vec<String>,
}

let mut engine: Engine<HostState> = Engine::with_prelude(HostState {
    user_id: "u-123".into(),
    roles: vec!["admin".into(), "editor".into()],
})?;

let mut globals = Module::global();
globals.export("have_role", |state, role: String| {
    Ok(state.roles.iter().any(|r| r == &role))
})?;
engine.inject_module(globals)?;

Array/List Interop at Host Boundaries

Rex keeps both List a and Array a because they serve different goals:

  • List a is ergonomic for user-authored functional code and pattern matching.
  • Array a is the host-facing contiguous representation (for example Vec<u8> from filesystem reads).

At host function call sites, Rex performs a narrow implicit coercion from List a to Array a in argument position. This means users can pass list literals to host functions that accept Vec<T> without writing conversions.

accept_bytes [1, 2, 3]

where accept_bytes is exported from Rust with a Vec<u8> parameter.

For the opposite direction, Rex exposes explicit helpers:

  • to_list : Array a -> List a
  • to_array : List a -> Array a

Why to_list Is Explicit (Not Implicit)

Array -> List conversion is intentionally explicit to keep runtime costs predictable in user code. Converting an array into a list allocates a new linked structure and changes performance characteristics for downstream operations.

If this conversion were implicit everywhere, the compiler could silently insert it in places where users do not expect allocation or complexity changes (for example inside control-flow joins, nested expressions, or polymorphic code). That would make performance harder to reason about and make type errors less transparent.

By requiring to_list explicitly, we keep intent and cost visible at the exact program point where representation changes. This preserves ergonomics while avoiding hidden work:

match (to_list bytes) with {
    case Cons head _ -> head;
    case Empty -> 0;
}

Typecheck Without Evaluating

use rex::{
    parser::parse,
    typesystem::{infer, standard_type_system},
};

let program = parse("map (\\x -> x) [1, 2, 3]").map_err(|errs| format!("{errs:?}"))?;

let mut ts = standard_type_system()?;
for decl in &program.decls {
    match decl {
        rex_ast::Decl::Type(d) => ts.register_type_decl(d)?,
        rex_ast::Decl::Class(d) => ts.register_class_decl(d)?,
        rex_ast::Decl::Instance(d) => {
            ts.register_instance_decl(d)?;
        }
        rex_ast::Decl::Fn(d) => ts.register_fn_decls(std::slice::from_ref(d))?,
    }
}

let body = program
    .body
    .as_ref()
    .expect("snippet must contain a final expression");
let (preds, ty) = infer(&mut ts, body.as_ref())?;
println!("type: {ty}");
if !preds.is_empty() {
    println!(
        "constraints: {}",
        preds.iter()
            .map(|p| format!("{} {}", p.class, p.typ))
            .collect::<Vec<_>>()
            .join(", ")
    );
}

Type Classes and Instances

Users can declare new type classes and instances directly in Rex source. As the host, you:

  1. Parse Rex source into CompilationUnit { decls, body }.
  2. Inject Decl::Class / Decl::Instance into the type system (if you’re typechecking without running).
  3. Inject all decls into the engine (if you’re running), so instance method bodies are available at runtime.

Typecheck: Inject Class/Instance Decls into TypeSystem

use rex::{
    parser::parse,
    typesystem::{infer, standard_type_system},
};

let code = r#"
class Size a where {
    size : a -> i32;
}
instance<t> Size (List t) where {
    size = \xs ->
        match xs {
            case Empty -> 0;
            case Cons _ rest -> 1 + size rest;
        };
}
size [1, 2, 3]
"#;

let program = parse(code).map_err(|errs| format!("{errs:?}"))?;

let mut ts = standard_type_system()?;
for decl in &program.decls {
    match decl {
        rex_ast::Decl::Type(d) => ts.register_type_decl(d)?,
        rex_ast::Decl::Class(d) => ts.register_class_decl(d)?,
        rex_ast::Decl::Instance(d) => {
            ts.register_instance_decl(d)?;
        }
        rex_ast::Decl::Fn(d) => ts.register_fn_decls(std::slice::from_ref(d))?,
    }
}

let body = program
    .body
    .as_ref()
    .expect("snippet must contain a final expression");
let (_preds, ty) = infer(&mut ts, body.as_ref())?;
assert_eq!(ty.to_string(), "i32");

Evaluate: Inject Decls into Engine

use rex_engine::{Engine, EngineError, Module};
use rex::parser::parse;

let code = r#"
class Size a where {
    size : a -> i32;
}
instance<t> Size (List t) where {
    size = \xs ->
        match xs {
            case Empty -> 0;
            case Cons _ rest -> 1 + size rest;
        };
}
(size [1, 2, 3], size [])
"#;

let program = parse(code).map_err(|errs| format!("{errs:?}"))?;

let engine = Engine::with_prelude(())?;
let mut compiler = engine.into_compiler();
let compiled = compiler.compile_program(&program, Default::default()).await?;
let _ty = compiled.result_type().clone();
let value = compiler.into_evaluator().run(compiled, Default::default()).await?;
println!("{value}");

Inject Native Values and Functions

rex-engine is the boundary where Rust provides implementations for Rex values.

For host-provided modules, prefer Module + inject_module (above). For root-scope values or functions, use Module::global() and inject that staged module into the engine.

use rex_engine::{Engine, Module};

let mut engine = Engine::with_prelude(())?;
let mut globals = Module::global();
globals.export_value("answer", 42i32)?;
globals.export("inc", |_state, x: i32| { Ok(x + 1) })?;
engine.inject_module(globals)?;

Integer Literal Overloading with Host Natives

Integer literals are overloaded (Integral a) and can specialize at call sites. This works for direct calls, let bindings, and lambda wrappers:

use rex::parser::parse;
use rex_engine::{Engine, Module};

for code in [
    "num_u8 4",
    "let x = 4 in num_u8 x",
    "let f = \\x -> num_i64 x in f 4",
] {
    let mut engine = Engine::with_prelude(())?;
    let mut globals = Module::global();
    globals.export("num_u8", |_state: &(), x: u8| Ok(format!("{x}:u8")))?;
    globals.export("num_i64", |_state: &(), x: i64| Ok(format!("{x}:i64")))?;
    engine.inject_module(globals)?;

    let program = parse(code).map_err(|errs| format!("parse error: {errs:?}"))?;
    let mut compiler = engine.into_compiler();
    let compiled = compiler.compile_program(&program, Default::default()).await?;
    let _ty = compiled.result_type().clone();
    let value = compiler.into_evaluator().run(compiled, Default::default()).await?;
    println!("{value}");
}

Negative literals specialize only to signed numeric types. For example, num_i32 (-3) is valid, while num_u32 (-3) is a type error.

Float literals are similarly context-sensitive for primitive float widths. A literal such as 3.0 defaults to f32 when unconstrained, but specializes to f64 when passed to a native or Rex function whose argument type is f64.

Async Natives

If your host functions are async, stage them in a module with export_async and run the compiled program with Evaluator::run.

use rex::parser::parse;
use rex_engine::{Engine, Module};

let mut engine = Engine::with_prelude(())?;
let mut globals = Module::global();
globals.export_async("inc", |_state, x: i32| async move { Ok(x + 1) })?;
engine.inject_module(globals)?;

let program = parse("inc 1").map_err(|errs| format!("parse error: {errs:?}"))?;
let mut compiler = engine.into_compiler();
let compiled = compiler.compile_program(&program, Default::default()).await?;
let _ty = compiled.result_type().clone();
let v = compiler.into_evaluator().run(compiled, Default::default()).await?;
println!("{v}");

By default, admitted async host futures are polled inline by the evaluator. This keeps the engine portable and avoids assuming a particular runtime, which is important for wasm embedders. Inline polling is fine for futures that are naturally non-blocking, but CPU-heavy or blocking work should be moved onto an executor supplied by the embedding application.

Use set_parallelism_controller to decide when async host callbacks may be invoked. A ParallelismController grants a NativeAsyncPermit for each admitted async native call; the permit is held until that call completes. Controllers can therefore enforce process-local limits, shared limits across several evaluators, or externally coordinated limits backed by a cluster scheduler.

ExecutionBounds remains available as a fixed controller. Its max_ready_work value is only an internal evaluator queue-pressure guard: it limits how many already-created Rex frames sit in the active ready queue, but it does not reserve external compute capacity. Native async permits are the backpressure mechanism for host jobs.

Use set_async_call_policy to wrap futures after they have been admitted. The policy decides where an admitted future runs; the parallelism controller decides whether the host callback is allowed to start yet.

use futures::FutureExt;
use rex_engine::{AsyncCallPolicy, Engine, EngineError, Module};

let mut engine = Engine::with_prelude(())?;
engine.set_async_call_policy(AsyncCallPolicy::executor_fn(|future| {
    async move {
        tokio::spawn(future)
            .await
            .map_err(|err| EngineError::Internal(format!("async host task failed: {err}")))?
    }
    .boxed()
}));

let mut globals = Module::global();
globals.export_async("inc", |_state, x: i32| async move { Ok(x + 1) })?;
engine.inject_module(globals)?;

The executor hook is intentionally generic rather than Tokio-specific. Native applications can use Tokio or any other Rust executor; wasm applications can keep the inline policy or adapt to browser task primitives in the host crate.

Parsing Limits

Parsing enforces a fixed AST-depth cap:

use rex::parser::parse;

let program = parse("(((1)))")
    .map_err(|errs| format!("parse error: {errs:?}"))?;

Bridge Rust Types with #[derive(Rex)]

The derive:

  • implements RexType
  • implements RexAdt
  • implements IntoRex
  • implements FromRex
  • adds inherent helper methods such as inject_rex, rex_adt_decl, and rex_adt_family
  • declares an ADT in the Rex type system
  • injects runtime constructors (so Rex can build values)
  • discovers and registers the full acyclic ADT family needed by the root type

The derive does not implement RexDefault; inject_rex_with_default is available only when the type already provides that trait.

Fields of type Vec<T> are exposed as Array T and convert to/from Rex runtime arrays. When constructing or updating derived records from Rex code, use to_array [...] for these fields.

That means MyType::inject_rex(&mut engine)? is enough for acyclic graphs of derived ADTs. You do not need to manually register dependencies in topological order. Cyclic ADT families are still not supported by this registration path.

If a field uses a Rust type that participates in Rex value conversion but is not itself a Rex ADT (for example a leaf type with manual RexType / IntoRex / FromRex impls), no extra field annotation is required. Such leaf types inherit the default no-op family collection from RexType, so derived ADTs can contain them without trying to register them as ADTs.

use rex::{
    Rex,
    engine::{Engine, EngineError, FromRex, Handle, Heap, IntoRex},
    typesystem::{RexType, Type},
};

#[derive(Debug, PartialEq)]
struct AtomRef(i32);

impl RexType for AtomRef {
    fn rex_type() -> Type {
        i32::rex_type()
    }
}

impl IntoRex for AtomRef {
    fn into_rex(self, heap: &Heap) -> Result<Handle, EngineError> {
        self.0.into_rex(heap)
    }
}

impl FromRex for AtomRef {
    fn from_rex(handle: &Handle) -> Result<Self, EngineError> {
        Ok(Self(i32::from_rex(handle)?))
    }
}

#[derive(Rex, Debug, PartialEq)]
struct Fragment(Vec<AtomRef>);

let mut engine = Engine::with_prelude(())?;
Fragment::inject_rex(&mut engine)?;
use rex::{
    Rex,
    engine::{Engine, FromRex},
    parser::parse,
};

#[derive(Rex, Debug, PartialEq)]
enum Maybe<T> {
    Just(T),
    Nothing,
}

let mut engine = Engine::with_prelude(())?;
Maybe::<i32>::inject_rex(&mut engine)?;

let program = parse("Just 1").map_err(|errs| format!("parse error: {errs:?}"))?;
let mut compiler = engine.into_compiler();
let compiled = compiler.compile_program(&program, Default::default()).await?;
let _ty = compiled.result_type().clone();
let v = compiler.into_evaluator().run(compiled, Default::default()).await?;
assert_eq!(Maybe::<i32>::from_rex(&v)?, Maybe::Just(1));

Register ADTs Without Derive

If your type metadata is data-driven (for example loaded from JSON), you can build ADTs without #[derive(Rex)].

  • Use Engine::adt_decl_from_type(...) to seed an ADT declaration from a Rex type head.
  • Add variants with AdtDecl::add_variant(...).
  • Stage it with Module::add_adt_decl(...), then inject that module with Engine::inject_module(...).

Module::add_adt_decl(...) is the low-level single-ADT staging primitive. If you are building several ADTs manually, prefer batching them in one module with add_adt_family(...).

use rex::{
    ast::Symbol,
    engine::{Engine, Module},
    typesystem::{RexType, Type},
};

let mut engine = Engine::with_prelude(())?;
let mut globals = Module::global();

let mut adt = engine.adt_decl_from_type(&Type::con("PrimitiveEither", 0))?;
adt.add_variant(Symbol::intern("Flag"), vec![bool::rex_type()]);
adt.add_variant(Symbol::intern("Count"), vec![i32::rex_type()]);
globals.add_adt_decl(adt)?;
engine.inject_module(globals)?;

If you have a Rust type with manual RexType/IntoRex/FromRex impls, implement RexAdt and provide rex_adt_decl(). Then Engine::inject_rex_adt::<T>() gives manual types the same registration workflow that #[derive(Rex)] exposes as T::inject_rex(...).

If the manual Rust type is itself an ADT, override RexType::collect_rex_family(...) and add its AdtDecl there. Leaf types can inherit the default no-op implementation.

use rex::{
    ast::Symbol,
    engine::Engine,
    typesystem::{AdtDecl, RexAdt, RexType, Type, TypeError, TypeVarSupply},
};

struct PrimitiveEither;

impl RexType for PrimitiveEither {
    fn rex_type() -> Type {
        Type::con("PrimitiveEither", 0)
    }

    fn collect_rex_family(out: &mut Vec<AdtDecl>) -> Result<(), TypeError> {
        out.push(<Self as RexAdt>::rex_adt_decl()?);
        Ok(())
    }
}

impl RexAdt for PrimitiveEither {
    fn rex_adt_decl() -> Result<AdtDecl, TypeError> {
        let mut supply = TypeVarSupply::new();
        let mut adt = AdtDecl::new(&Symbol::intern("PrimitiveEither"), &[], &mut supply);
        adt.add_variant(Symbol::intern("Flag"), vec![bool::rex_type()]);
        adt.add_variant(Symbol::intern("Count"), vec![i32::rex_type()]);
        Ok(adt)
    }
}

let mut engine = Engine::with_prelude(())?;
engine.inject_rex_adt::<PrimitiveEither>()?;

Depth Limits

Some workloads (very deep nesting) can exhaust parser/typechecker recursion depth. Prefer bounded limits for untrusted code:

  • parser AST depth
  • rex_typesystem::TypeSystemLimits::safe_defaults

Contributing

Workspace Layout

Rex is a Cargo workspace. The most important crates are:

  • rex-parser: source parsing into a CompilationUnit { decls, body }
  • rex-ast: AST nodes, symbols, and spans
  • rex-typesystem: Hindley–Milner inference + type classes + ADTs
  • rex-engine: host environment building, compilation, evaluation, and native injection
  • rex-proc-macro: #[derive(Rex)] bridge for Rust types ↔ Rex types/values
  • rex: CLI binary

Architecture overview: ARCHITECTURE.md.

Development

Run the full test suite:

cargo test

There is also a lightweight “fuzz smoke” test that runs a deterministic parse→infer→eval loop. You can scale iterations with REX_FUZZ_ITERS:

REX_FUZZ_ITERS=2000 cargo test -p rex --test fuzz_smoke

Fuzz Harnesses

For end-to-end fuzzing with external fuzzers (AFL++, honggfuzz, custom mutational drivers), the workspace includes rex-fuzz, a set of stdin-driven harness binaries:

cargo build -p rex-fuzz --bins
printf '1 + 2' | cargo run -q -p rex-fuzz --bin e2e
printf '(' | cargo run -q -p rex-fuzz --bin parse

Tuning knobs (environment variables):

  • REX_FUZZ_STACK_MB: stack size (MiB) for the harness thread

If you edit Rust code, also run:

cargo fmt
cargo clippy

Lockfiles

This repo commits:

  • Cargo.lock (workspace lockfile)
  • rex-vscode/package-lock.json (VS Code extension)

Other lock-like files (for example under target/ or node_modules/) are build artifacts and should not be committed.

LLMs

Introduction and Rationale

Rex includes a semantic assistance layer designed first for machine clients that generate code, especially LLM agents, and second for humans using an editor. This ordering is deliberate. LLMs are fast at proposing code but weak at maintaining a precise internal model of a language’s static semantics over many edits. A practical system therefore externalizes semantic reasoning into stable, tool-facing interfaces that can be queried repeatedly. Human users still benefit from the same machinery, but the core design target is iterative machine control: propose code, observe structured feedback, apply a constrained repair, and repeat.

A key design decision is to prioritize structured outputs over prose. Natural-language diagnostics are useful for people, but brittle for agents. Rex exposes semantic information and quick-fix data through explicit command contracts so that an LLM can operate as a controller over the typechecker and editor transformations rather than as a parser of unstructured text.

Typed Holes as a Control Primitive

The center of the workflow is the typed hole, written as ?. A hole allows partial programs to be represented directly in source code. Instead of treating incompleteness as a syntax error, Rex keeps the program parseable and infers constraints around the missing expression.

This shifts generation from “write final code in one pass” to “write a scaffold, then solve local obligations.” For LLMs, this is a better fit: the model can produce a coarse structure, ask for the expected type at the hole, retrieve candidate repairs, and select one.

fn parse_ph : string -> Result f32 string = \raw ->
  if raw == "7.3" then Ok 7.3 else Err "bad reading";

fn classify_ph : f32 -> string = \ph ->
  if ph < 6.8 then "acidic"
  else if ph > 7.8 then "alkaline"
  else "stable";

fn qc_label_from_sensor : string -> Result string string = \raw ->
  match (parse_ph raw) with {
    case Ok ph -> Ok (classify_ph ph);
    case Err e -> Err e;
  };

let sensor_reading = "7.3" in
let qc_label : Result string string = ? in
qc_label

In an LSP-enabled editor (including the browser playground), placing the cursor on ? exposes hole-filling actions and semantic candidates such as qc_label_from_sensor sensor_reading. The expected type at the hole is Result string string, so the model can fill a semantically meaningful real-world step without guessing. The same machinery is consumed by VS Code and by external LLM tooling.

Semantic Loop Endpoints

Rex provides semantic commands that return JSON-shaped data for program state at a position. The most important operation is a single semantic loop step, which reports expected and inferred types, in-scope values, candidate functions and adapters, local diagnostics, quick-fixes, and hole metadata.

From a control-systems viewpoint, this is an observation function over the current text. Separate commands apply a selected quick-fix by identifier, or repeatedly apply best-ranked quick-fixes in bulk mode. Bulk mode also supports a dry-run option so agents can preview predicted text without committing edits.

The intended loop is simple: observe, choose, apply, re-observe. This structure is robust because it avoids fragile prompt-only planning and continuously re-anchors decisions in the compiler’s current state.

Candidate Narrowing and Adapter-Aware Repair

Candidate generation is hole-targeted and type-directed. Rex prefers functions whose result type can satisfy the local expected type and attempts to satisfy function arguments from in-scope values. When no direct value exists for an argument, Rex can propose single-step adapter expressions derived from in-scope functions.

This does not prove semantic correctness. It proves local type plausibility and improves search efficiency. The mechanism narrows the action space; it does not replace domain reasoning.

fn mk : i32 -> string = \n -> "value";
let x = 1 in
let y : string = ? in
y

In the editor, the hole can be filled with a candidate such as mk x, generated from local type compatibility and in-scope bindings.

Bulk Repair, Dry Runs, and Contracts

Rex supports multi-step quick-fix application around a cursor location. Bulk repair is useful for agents because it can reduce several local errors in one command while returning telemetry about what changed at each step. Dry-run mode computes the same sequence but reports predicted output without mutating source text.

The semantic endpoints use a stable JSON contract with regression tests. This matters operationally: agents are software clients, and software clients break when response schemas drift. Contract tests convert “it usually works” into “it remains parseable across refactors.”

Resource Bounds and Adversarial Inputs

Semantic assistance can become expensive when scope size is large. To keep the system usable under load and safer for embedded deployments, Rex enforces explicit limits in semantic candidate pipelines, including caps on scanned environment schemes, in-scope values, candidate list sizes, and hole-report counts. This is a pragmatic defense against unbounded CPU and output growth in LSP-side analysis.

These bounds are not a complete security model. They should be combined with host-level timeouts, concurrency limits, memory limits, and request-rate controls in production embeddings.

Trying the Workflow in the Browser Playground

The interactive playground has full LSP support, so this chapter can be exercised directly in the browser. Paste a snippet with a hole, place the cursor on the hole, and inspect available quick-fixes and semantic suggestions.

fn parse_i32 : string -> Result string i32 = \s ->
  if s == "42" then Ok 42 else Err "bad-int";

fn plus1 : i32 -> i32 = \n -> n + 1;

let input = "42" in
let out : Result string i32 = ? in
out

A useful exercise is to fill out in multiple ways, observe type errors, then invoke semantic quick-fixes and compare outcomes.

The ideas used here are mostly established. Typed holes and goal-directed development are prominent in systems such as GHC (Haskell) and dependently typed environments like Agda and Idris. Live, structure-aware editor semantics have been explored in research systems such as Hazel. Type-directed code search and synthesis has a long line of work, including tools like InSynth and later synthesis frameworks.

Rex does not claim conceptual novelty in these foundations. Its contribution is engineering integration: one semantics pipeline serving both human editor workflows and LLM control loops, with contract-stable machine interfaces, regression coverage, and bounded candidate generation.

Reference: Semantic Assists

Rex exposes the following assists through LSP execute commands. Each assist is intended to be used in a short observe-then-act loop rather than as a one-shot oracle.

The argument forms below use JSON types and a 0-based Position.

Common types:

type UriArg =
  | { uri: string }
  | [uri: string];

type PosArg =
  | { uri: string; line: u32; character: u32 }
  | [uri: string, line: u32, character: u32];

type DiagnosticLite = {
  message: string;
  line: u32;
  character: u32;
};

type QuickFix = {
  id: string;
  title: string;
  kind: string | null;
  edit: WorkspaceEdit | null;
};

type HoleInfo = {
  name: string;
  line: u32;
  character: u32;
  expectedType: string;
};

rex.expectedTypeAt

args: PosArg
returns: null | { expectedType: string }

rex.functionsProducingExpectedTypeAt

args: PosArg
returns: { items: string[] } // each item rendered as "name : type"

rex.functionsAcceptingInferredTypeAt

args: PosArg
returns: {
  inferredType: string | null;
  items: string[];
}

rex.adaptersFromInferredToExpectedAt

args: PosArg
returns: {
  inferredType: string | null;
  expectedType: string | null;
  items: string[];
}

rex.functionsCompatibleWithInScopeValuesAt

args: PosArg
returns: { items: string[] } // concrete call-style suggestions

rex.holesExpectedTypes

args: UriArg
returns: { holes: HoleInfo[] }

rex.semanticLoopStep

args: PosArg
returns: {
  expectedType: string | null;
  inferredType: string | null;
  inScopeValues: string[];
  functionCandidates: string[];
  holeFillCandidates: Array<{ name: string; replacement: string }>;
  functionsAcceptingInferredType: string[];
  adaptersFromInferredToExpectedType: string[];
  functionsCompatibleWithInScopeValues: string[];
  localDiagnostics: DiagnosticLite[];
  quickFixes: QuickFix[];
  quickFixTitles: string[];
  holes: HoleInfo[];
}

rex.semanticLoopApplyQuickFixAt

args:
  | { uri: string; line: u32; character: u32; id: string }
  | [uri: string, line: u32, character: u32, id: string]
returns: null | { quickFix: QuickFix }

rex.semanticLoopApplyBestQuickFixesAt

args:
  | {
      uri: string;
      line: u32;
      character: u32;
      maxSteps?: u64;
      strategy?: "conservative" | "aggressive";
      dryRun?: bool;
    }
  | [
      uri: string,
      line: u32,
      character: u32,
      maxSteps?: u64,
      strategy?: string,
      dryRun?: bool
    ]
// maxSteps is clamped to [1, 20]

returns: {
  strategy: "conservative" | "aggressive";
  dryRun: bool;
  appliedQuickFixes: QuickFix[];
  appliedCount: u64;
  steps: Array<{
    index: u64;
    quickFix: QuickFix;
    diagnosticsBefore: DiagnosticLite[];
    diagnosticsAfter: DiagnosticLite[];
    diagnosticsBeforeCount: u64;
    diagnosticsAfterCount: u64;
    diagnosticsDelta: i64;
    noImprovementStreak: u64;
  }>;
  updatedText: string;
  localDiagnosticsAfter: DiagnosticLite[];
  stoppedReason: string;
  stoppedReasonDetail: string;
  lastDiagnosticsDelta: i64;
  noImprovementStreak: u64;
  seenStatesCount: u64;
}

Practical Generation Guidance (Legacy Checklist)

The remainder of this chapter preserves the practical generation checklist that was previously a standalone LLM guidance page. It remains useful when an LLM is emitting Rex directly rather than running a semantic loop command at each step.

When building or revising Rex code, read docs in this order:

  1. This chapter (LLMS.md) for semantic-loop workflow and generation pitfalls.
  2. LANGUAGE.md for syntax and everyday feature usage.
  3. SPEC.md for locked behavior when edge cases matter.

High-Value Rules

  1. Use fn for top-level reusable functions; use let and let rec for local helpers.
  2. For local mutual recursion, use comma-separated let rec bindings.
  3. Use x::xs for list cons in both patterns and expressions (x::xs is equivalent to Cons x xs).
  4. Validate snippets with the Rex CLI before shipping docs.

Quick Generation Checklist

Before returning generated Rex code:

  1. Put top-level reusable functions in fn declarations (they are mutually recursive).
  2. Use let rec only for local recursive helpers inside expressions.
  3. Add annotations where constructor or numeric ambiguity is likely (Empty, zero, overloaded methods).
  4. Ensure the final expression returns a visible result (often a tuple for demos).
  5. Run cargo run -p rex-cli --bin rex -- /tmp/snippet.rex and fix all parse and type errors.

Syntax Pitfalls

1) Recursion model

  • Top-level fn declarations are mutually recursive.
  • Top-level type and fn declarations end with ;; indentation and newlines do not terminate them.
  • Single recursive local helper: let rec
  • Mutually recursive local helpers: let rec with commas between bindings.

Top-level mutual recursion:

fn even : i32 -> bool = \n ->
  if n == 0 then true else odd (n - 1);

fn odd : i32 -> bool = \n ->
  if n == 0 then false else even (n - 1);

even 10
let rec
  even = \n -> if n == 0 then true else odd (n - 1),
  odd = \n -> if n == 0 then false else even (n - 1)
in
  even 10

If you define local helpers in plain let and reference each other, you will get unbound-variable errors. Use let rec for local recursion.

2) List construction and list patterns

  • Pattern matching: x::xs is valid in case patterns.
  • Expression construction: x::xs and Cons x xs are equivalent (list literals are also valid). Cons uses normal constructor and function call style (Cons head tail).

Equivalent:

x::xs
Cons x xs

3) ADT equality is not implicit

Do not assume custom ADTs automatically implement Eq. For example, comparing Node values with == can fail with a missing-instance type error.

For small enums and ADTs, write an explicit equality helper:

node_eq = \a b ->
  match (a, b) with {
    case (A, A) -> true;
    case (B, B) -> true;
    case _ -> false;
  }

Related: avoid checking list emptiness with direct equality like xs == [] in generic code. Prefer an explicit matcher helper.

4) Ambiguous constructors (for example Empty)

Constructors like Empty can be ambiguous when multiple ADTs define the same constructor name (for example List.Empty and Tree.Empty).

Disambiguate with an annotation at the binding site:

type Tree = Empty | Node { key: i32, left: Tree, right: Tree };

let
  t0: Tree = Empty
in
  match t0 with {
    case Empty -> 0;
    case Node {key, left, right} -> key;
  }

5) Reserved identifiers

Avoid bindings that collide with keywords (for example as). Use alternatives like xs1, lefts, rest1, and similar.

6) Constructor patterns with literals

Some forms like Lit 1 inside nested patterns can fail to parse. Prefer simpler constructor patterns and do literal checks in expression logic if needed.

Also avoid relying on tuple and list patterns that include numeric literals in one branch (for example (x::_, 0)); match structurally first, then use an if guard in expression code.

Validation Workflow

Before emitting generated Rex snippets in docs:

  1. Save the snippet to a temporary .rex file.
  2. Run cargo run -p rex-cli --bin rex -- /tmp/snippet.rex.
  3. If parse or type errors appear, fix and re-run until clean.

For mdBook interactive demos, also run:

cd docs
mdbook build