Lambdas & Iteration¶

Prove has no loops. All iteration is expressed through higher-order functions.

Lambdas¶

Lambdas are single-expression anonymous functions, used exclusively as arguments to higher-order functions like map, filter, and reduce. They cannot capture mutable state and must be pure.

Syntax: |params| expression

// Filtering with a lambda
active_users as List<User> = filter(users, |u| u.active)

// Mapping with a lambda
names as List<String> = map(users, |u| u.name)

// Reducing with a lambda
total as Decimal = reduce(prices, 0, |acc, p| acc + p.price)

// Using `valid` to pass a validates function as predicate (no lambda needed)
verified_emails as List<String> = filter(emails, valid email)

Constraints: - Single expression only — no multi-line bodies, no statements. If you need more, write a named function. - Should be pure — IO effects inside a lambda are not recommended and may cause undefined behavior in parallel contexts. Side effects require a named function. - Closure capture — lambdas can capture immutable variables from the enclosing scope. Captured values are passed via a compiler-generated context struct. - Only as arguments — lambdas cannot be assigned to variables or returned from functions. They exist only at the call site of a higher-order function or a Verb parameter.

Lambdas work with any function parameter typed as Verb<P1, ..., R>:

// Store merge with a lambda resolver
result as MergeResult = Store.merge(base, local, remote, |c| KeepRemote)

Builtin Functions¶

The following functions are builtins — always available, no import needed. They work on any iterable type (List, Array, and future iterable types like cursors).

Higher-Order Functions¶

Index parameter: map, filter, each, all, and any support an optional second lambda parameter for the element index (typed as Integer):

// With index
numbered as List<String> = map(users, |u, idx| f"{idx}: {u.name}")
evens as List<Item> = filter(items, |item, idx| idx % 2 == 0)

Other Builtins¶

These are not part of any stdlib module — they are compiler builtins with generic type inference. The compiler dispatches to the appropriate C runtime function based on the collection type.

Note: The builtin clamp handles Integer arguments only. For Float and Decimal arguments, use Math.clamp — see Math.

Iteration — No Loops¶

Prove has no for, while, or loop constructs. Iteration is expressed through the builtin HOFs (map, filter, reduce) and recursion. This keeps all data transformations as expressions (they produce values) rather than statements.

// Instead of: for each user, get their name
names as List<String> = map(users, |u| u.name)

// Instead of: for each item, keep valid ones
valid_items as List<Item> = filter(items, |i| i.quantity > 0)

// Instead of: accumulate a total with a loop
total as Decimal = reduce(order.items, 0, |acc, item| acc + item.price * item.quantity)

// Chaining with pipe operator
result as List<String> = users
    |> filter(|u| u.active)
    |> map(|u| u.email)
    |> filter(valid email)

// Check if all items are in stock
all_available as Boolean = all(items, |i| i.quantity > 0)

// Check if any user is an admin
has_admin as Boolean = any(users, |u| u.role == "admin")

For complex iteration that doesn't fit map/filter/reduce, use recursion with a transforms function and a terminates annotation.

Parallel Iteration¶

par_map, par_filter, and par_reduce are parallel variants of the standard higher-order functions. They use a pthreads thread pool with automatic core detection — no worker count needed.

// Parallel map — transform each element concurrently
scores as List<Integer> = par_map(documents, compute_score)

// Parallel filter — keep matching elements concurrently
valid as List<Order> = par_filter(orders, valid order)

// Parallel reduce — combine elements concurrently
total as Integer = par_reduce(values, 0, add)

Purity requirement: for par_map, par_filter, and par_reduce, the callback must be a named pure function (transforms, validates, derives, creates, or matches). IO and async verbs are rejected at compile time. par_each is less restrictive — it allows IO callbacks but rejects async verbs. When using a named function reference, the compiler verifies purity; lambdas passed to parallel HOFs are not currently checked.

Closures: lambdas with captured variables are supported. The compiler generates a context struct for captured values and passes it through the parallel runtime.

Ordering: result ordering is not guaranteed — elements may be placed in any order depending on thread scheduling. Use map if ordering must be preserved.

Why No Loops?¶

1. Expressions, not statements — map, filter, reduce return values; loops are statements that require mutable state
2. Composable — chain operations: users |> filter(...) |> map(...)
3. Parallelizable — the compiler can parallelize par_map automatically
4. Total functions — no chance of infinite loops when combined with terminates

Complete Example: RESTful Server¶

module Rest
  type Port is Integer:[16 Unsigned] where 1 .. 65535
  type Route is Get(path String) | Post(path String) | Delete(path String)

  type User is
    id Integer
    name String
    email String

/// Checks whether a string is a valid email address.
validates email(address String)
from
    contains(address, "@") && contains(address, ".")

/// Retrieves all users from the store.
inputs users(db Store) List<User>!
from
    query(db, "SELECT * FROM users")!

/// Creates a new user from a request body.
outputs create(db Store, body String) User!
  ensures email(result.email)
from
    user as User = decode(body)!
    insert(db, "users", user)!
    user

/// Routes incoming HTTP requests.
dispatches request(route Route, body String, db Store) Response!
from
    Get("/health") => ok("healthy")
    Get("/users")  => users(db)! |> encode |> ok
    Post("/users") => create(db, body)! |> encode |> created
    _              => not_found()

/// Application entry point — no verb, main is special.
main()!
from
    port as Port = 8080
    db as Store = connect()!
    server as Server = new_server()
    route(server, "/", request)
    listen(server, port)!