Iwf Guide

Database and Migrations

Iwf is PostgreSQL-first. You write the schema in SQL, Iwf generates Idris metadata and model types, and runtime queries go through the PostgreSQL runtime adapter.

1. Schema.sql

The schema source of truth is:

Application/Schema.sql

Start with normal PostgreSQL DDL:

CREATE TABLE users (
  id BIGSERIAL PRIMARY KEY,
  email TEXT NOT NULL UNIQUE,
  username TEXT NOT NULL UNIQUE,
  password_hash TEXT NOT NULL,
  created_at TIMESTAMP NOT NULL DEFAULT now()
);

CREATE TABLE articles (
  id BIGSERIAL PRIMARY KEY,
  author_id BIGINT NOT NULL REFERENCES users(id),
  slug TEXT NOT NULL UNIQUE,
  title TEXT NOT NULL,
  body TEXT NOT NULL,
  created_at TIMESTAMP NOT NULL DEFAULT now()
);

Application/Fixtures.sql contains development and test data.

2. Generated Idris Types

The app build runs typegen before Idris compilation. In the canonical app:

cd examples/canonical
iwf build --server

Typegen emits Generated.Schema under build/generated/.

Generated modules include:

model records such as Article.
typed primary and foreign key IDs such as Id "articles".
enum types.
JSON, schema, and form decoding support for full model rows.
table and column metadata.
nullability and constraint metadata.
model decoders used by TypedSQL.
schemaMetadata for PostgreSQL-to-Idris type mapping.
databaseMetadata for runtime/schema features.

SQL names are rendered as Idris names:

audit_logs -> AuditLog
user_id    -> userId

Nullable columns become Maybe. Primary keys become Id "table". Foreign keys become IDs of the referenced table.

The parser supports the canonical app style plus a growing PostgreSQL subset: tables, enums, extensions, schemas, indexes, RLS policies, comments, domains, arrays, generated columns, column comments, composite primary keys, richer defaults/checks, and common ALTER TABLE ... ADD ... constraints.

It is not a full PostgreSQL parser. Cover unusual DDL with typegen tests before depending on generated metadata from it.

3. Migrations

Migration files live in:

Application/Migrations/

Use migrations to evolve existing databases. Keep Application/Schema.sql as the desired final state.

The check workflow can load Application/Schema.sql, replay migrations into a clean database, and compare schema-only dumps when migration files are present.

4. Handler Database Access

In controllers, handlers already receive a ControllerContext. Iwf uses that context as an auto implicit database source, so ordinary controller queries do not need an explicit db context wrapper:

listTags : ControllerContext -> ControllerApp (List String)
listTags context =
  sqlQuery "select name from tags order by name"

Runtime execution uses the canonical PostgreSQL runtime library under:

libs/idris-postgres-runtime

The current backend is a long-lived Python/libpq helper hidden behind that library boundary. App code should call Iwf database APIs. It should not build psql -c commands for runtime queries.

For scripts or framework maintenance code outside a controller, create a pool and borrow a connection explicitly:

runMaintenance : AppConfig -> IO (Either String ())
runMaintenance config = do
  pool <- poolFromConfig config
  result <-
    withConnection pool $ \connection =>
      withTransaction connection $
        transactionExec
          "update iwf_jobs set locked_at = null where locked_at is not null;"
  shutdownDatabasePool pool
  pure result

5. Prepared Queries

Use sqlQuery and sqlExec in controllers. They combine compile-time TypedSQL checking with the controller error boundary:

findUser : String -> ControllerContext -> ControllerApp (Maybe User)
findUser email context =
  sqlQuery "select users.* from users where email = ${email}"

saveEmail : User -> String -> ControllerContext -> ControllerApp ()
saveEmail user email context =
  sqlExec "update users set email = ${email} where id = ${user.id}"

Prepared query parameters are captured from local names or field projections in ${...} placeholders. Parameter values are sent separately from SQL text. Query-failure logs include operation, SQL text, parameter count, and adapter error, but not parameter values.

For checked query definitions, use TypedSQL.

6. Transactions

Use transactionOrFail when several prepared statements must commit or roll back together. The transaction provides the database source for nested queries:

renameArticle :
  Id "articles" ->
  String ->
  ControllerContext ->
  ControllerApp ()
renameArticle articleId title context =
  transactionOrFail $
    sqlExec "update articles set title = ${title} where id = ${articleId}"

Adapter errors roll the transaction back and become controller failures.

Use withTransactionWithAutoRefresh when writes should invalidate live fragments:

withTransactionWithAutoRefresh runtime connection $
  transactionExecInvalidating
    "update articles set title = 'Updated' where id = 1;"
    ["articles"]

7. Typed Exception Cleanup

The helpers above are the normal app interface. Plain withConnection is an IO convenience helper for scripts. Use withConnectionApp when framework or advanced code can throw typed Control.App exceptions and the pool slot must still be released:

import Control.App

data MaintenanceAbort = MkMaintenanceAbort

runCheckedMaintenance :
  DatabasePool ->
  Control.App.App Control.App.Init (Either String ())
runCheckedMaintenance pool =
  Control.App.handle {err = MaintenanceAbort}
    (withConnectionApp {err = MaintenanceAbort} pool $ \connection => do
      result <- Control.App.primIO (executeSql connection "select 1")
      case result of
        Left _ => Control.App.throw MkMaintenanceAbort
        Right _ => pure ())
    (\_ => pure (Right ()))
    (\_ => pure (Left "maintenance aborted"))

Use withTransactionApp when advanced typed user code can throw inside a runtime transaction. It rolls the transaction back, releases runtime state, and rethrows the same typed exception.

8. Row-Level Security Metadata

Define RLS in SQL:

ALTER TABLE articles ENABLE ROW LEVEL SECURITY;

CREATE POLICY articles_author_policy ON articles
  USING (author_id = current_setting('app.current_user_id')::bigint);

Generated schema metadata records protected tables and policies. Use:

authenticatedRlsContext
authUserRlsContext
anonymousRlsContext
rlsTransaction
withRlsTransaction

These helpers prepend request-local role/user settings before application SQL runs.

9. Useful Runtime Helpers

sqlQuery
sqlExec
transactionOrFail

Advanced and script-facing helpers:

transaction
query
queryMaybe
exec
queryOrFail
queryMaybeOrFail
execOrFail
poolFromConfig
databasePool
withConnection
withConnectionApp
shutdownDatabasePool
checkDatabasePool
databasePoolMetrics
executeSql
executeSqlParams
executeSqlDetailed
executeSqlParamsDetailed
withTransaction
withTransactionApp
transactionExec
transactionExecParams
transactionExecTracked
transactionExecInvalidating
executePrepared
queryPreparedRows
queryPrepared

Deliberate Non-Features

Iwf does not add a relationship DSL or generated model validation metadata. Keep relationship loading as explicit SQL and explicit Idris functions.

Read TypedSQL.