Iwf Guide

First CRUD Feature

This guide builds one small article feature in the order users usually need it: page, route, form, table, query, validation, auth, live refresh, and final check. It uses the app-facing Iwf surface only.

1. Create The App

Start from a generated project:

iwf new my-app
cd my-app
iwf build

Keep the starter shape:

module Main

import Iwf

%language ElabReflection
%default partial

The normal app path starts from import Iwf. Add feature imports only when the feature needs generated app code, such as Generated.Schema for database rows.

2. Add A Page

Write the page directly. The view returns ordinary .idrx HTML; render adds the default shell for full browser requests:

articleIndexView : Html
articleIndexView =
  fragment
    [ <title>Articles</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <header class="flex items-center justify-between">
          <h1>Articles</h1>
          <a class="btn-primary" href="/articles/new">New article</a>
        </header>
        <p>No articles yet.</p>
      </main>
    ]

render serves the full shell for normal browser requests and the #main-content fragment for boosted requests.

3. Add A Route With A Path Parameter

Path captures live in a normal record:

record ArticlePath where
  constructor MkArticlePath
  slug : String

The route spec tells Iwf which path fields to decode, and handledBy checks the handler implements that spec:

showArticle : ArticlePath -> ControllerContext -> ControllerApp Response
showArticle input context = do
  maybeArticle <-
    sqlQuery
      "select articles.* from articles where slug = ${input.slug}"
  article <- requireFound maybeArticle
  pure (render context (articleShowView article))

showArticleRoute : RouteSpec ArticlePath NoInput Response
showArticleRoute =
  get "/articles/{slug}" |> params ArticlePath |> html

showArticleBinding : BoundRoute
showArticleBinding =
  handledBy showArticleRoute showArticle

There is no separate body declaration for this route because the route has no body. For routes that do have a body, declare the body type on the route spec and bind the handler with handledBy.

4. Add A Form

Define the submitted fields:

record ArticleForm where
  constructor MkArticleForm
  title : String
  slug : String
  body : String

%runElab derive "ArticleForm" [Show, Eq, FormFields]

Write the form as direct HTML:

newArticleForm : ArticleForm -> List ValidationError -> Html
newArticleForm input errors =
  <form id="article-form" class="form stack" method="post" action={pathTo createArticleRoute}>
    {errorSummary errors}
    <label class="field">
      <span>Title</span>
      <input name={articleFormTitleField} value={input.title} />
    </label>
    <label class="field">
      <span>Slug</span>
      <input name={articleFormSlugField} value={input.slug} />
    </label>
    <label class="field">
      <span>Body</span>
      <textarea name={articleFormBodyField}>{input.body}</textarea>
    </label>
    <button class="btn-primary" type="submit">Publish</button>
  </form>

The route value supplies the action URL. The generated field values supply the name attributes. If a field is renamed on ArticleForm, stale form markup fails at compile time.

Put the form in a page and route to it:

newArticlePage : ArticleForm -> List ValidationError -> Html
newArticlePage input errors =
  fragment
    [ <title>New Article</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <h1>New article</h1>
        {newArticleForm input errors}
      </main>
    ]

newArticle : ControllerContext -> Response
newArticle context =
  render context (newArticlePage (MkArticleForm "" "" "") [])

newArticleRoute : RouteSpec NoInput NoInput Response
newArticleRoute =
  get "/articles/new"

newArticleBinding : BoundRoute
newArticleBinding =
  handledBy newArticleRoute newArticle

5. Add A Table

Add the table to Application/Schema.sql:

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

Then rebuild:

iwf build

The build generates Generated.Schema, including Article and typed table ids. Import it where handlers or views use generated models:

import Generated.Schema

6. Add TypedSQL Queries

Write the SQL directly beside the handler code. sqlQuery is for statements that return rows; sqlExec is for statements that do not return rows.

Replace the empty page with a data-driven page:

articleIndexView : ControllerContext -> List Article -> Html
articleIndexView context articles =
  fragment
    [ <title>Articles</title>
    , <main id="main-content" class="mx-auto flex max-w-3xl flex-col gap-6 p-6">
        <header class="flex items-center justify-between">
          <h1>Articles</h1>
          <a class="btn-primary" href="/articles/new">New article</a>
        </header>
        {articleList articles}
      </main>
    ]

Run queries directly from the controller. The handler's ControllerContext provides the current database automatically:

articles : ControllerContext -> ControllerApp Response
articles context = do
  rows <-
    sqlQuery
      "select articles.* from articles order by created_at desc"
  pure (render context (articleIndexView context rows))

For writes, use sqlExec:

insertArticle : ArticleForm -> ControllerContext -> ControllerApp ()
insertArticle input context =
  sqlExec
    "insert into articles (slug, title, body) values (${input.slug}, ${input.title}, ${input.body})"

7. Add Validation

Validate the decoded body record before writing:

validateArticle : ArticleForm -> Either (List ValidationError) ArticleForm
validateArticle input =
  allValidations
    [ mapValidation (\_ => input) (requiredString "title" input.title)
    , mapValidation (\_ => input) (requiredString "slug" input.slug)
    , mapValidation (\_ => input) (requiredString "body" input.body)
    ]
    (valid input)

Use the same page when validation fails:

createArticle : ArticleForm -> ControllerContext -> ControllerApp Response
createArticle input context =
  case validateSessionCsrf context.session context.request of
    Left errors => pure (render context (newArticlePage input errors))
    Right _ =>
      case validateArticle input of
        Left errors => pure (render context (newArticlePage input errors))
        Right valid => do
          insertArticle valid context
          pure (seeOther (pathTo showArticleRoute (MkArticlePath valid.slug)))

createArticleRoute : RouteSpec NoInput ArticleForm Response
createArticleRoute =
  post "/articles" |> body ArticleForm |> html

createArticleBinding : BoundRoute
createArticleBinding =
  handledBy createArticleRoute createArticle

The route declaration records the submitted body type, and handledBy checks that the controller implements ArticleForm -> ControllerContext -> ControllerApp Response.

8. Add Auth

Protect only the write path at first:

createArticle : ArticleForm -> ControllerContext -> ControllerApp Response
createArticle input context = do
  _ <- requireCurrentUser context
  case validateSessionCsrf context.session context.request of
    Left errors => pure (render context (newArticlePage input errors))
    Right _ =>
      case validateArticle input of
        Left errors => pure (render context (newArticlePage input errors))
        Right valid => do
          insertArticle valid context
          pure (seeOther (pathTo showArticleRoute (MkArticlePath valid.slug)))

Keep the auth decision in the handler. The route table remains a readable list of HTTP method, path, and handler.

9. Add A Live Fragment

Mark the list as depending on the articles table:

articleFeed : ControllerContext -> List Article -> Html
articleFeed context articles =
  liveFragment context "article-feed" "/articles/partial" ["articles"]
    (articleList articles)

Use it in the full document:

articleIndexView : ControllerContext -> List Article -> Html
articleIndexView context articles =
  fragment
    [ <title>Articles</title>
    , <main id="main-content">
        {articleFeed context articles}
      </main>
    ]

Return the same region from a fragment endpoint:

articlesPartial : ControllerContext -> ControllerApp Response
articlesPartial context = do
  rows <-
    sqlQuery
      "select articles.* from articles order by created_at desc"
  pure (renderFragment context (articleFeed context rows))

articlesPartialRoute : RouteSpec NoInput NoInput Response
articlesPartialRoute =
  get "/articles/partial"

articlesPartialBinding : BoundRoute
articlesPartialBinding =
  handledBy articlesPartialRoute articlesPartial

Enable Auto Refresh once in the app runner:

main : IO ()
main =
  runApp
    (app "My App" appRoutes
      |> withDatabaseFromEnv
      |> withSessionSecretFromEnv
      |> withAutoRefresh)

The page says which table it depends on. Iwf handles the live refresh wiring and refresh request.

10. Ship With Check

Keep the route table readable:

export
htmlArticlesRoute : RouteSpec NoInput NoInput Response
htmlArticlesRoute =
  get "/articles"

htmlArticlesBinding : BoundRoute
htmlArticlesBinding =
  handledBy htmlArticlesRoute articles

export
htmlNewArticleRoute : RouteSpec NoInput NoInput Response
htmlNewArticleRoute =
  get "/articles/new"

htmlNewArticleBinding : BoundRoute
htmlNewArticleBinding =
  handledBy htmlNewArticleRoute newArticle

export
htmlCreateArticleRoute : RouteSpec NoInput ArticleForm Response
htmlCreateArticleRoute =
  post "/articles" |> body ArticleForm |> html

htmlCreateArticleBinding : BoundRoute
htmlCreateArticleBinding =
  handledBy htmlCreateArticleRoute createArticle

export
htmlArticleRoute : RouteSpec ArticlePath NoInput Response
htmlArticleRoute =
  get "/articles/{slug}" |> params ArticlePath |> html

htmlArticleBinding : BoundRoute
htmlArticleBinding =
  handledBy htmlArticleRoute showArticle

export
htmlArticlesPartialRoute : RouteSpec NoInput NoInput Response
htmlArticlesPartialRoute =
  get "/articles/partial"

htmlArticlesPartialBinding : BoundRoute
htmlArticlesPartialBinding =
  handledBy htmlArticlesPartialRoute articlesPartial

export
htmlRoutes : Routes
htmlRoutes =
  [ htmlArticlesBinding
  , htmlNewArticleBinding
  , htmlCreateArticleBinding
  , htmlArticleBinding
  , htmlArticlesPartialBinding
  ]

appRoutes : Routes
appRoutes =
  htmlRoutes

Run the app check before shipping:

iwf check

At this point the feature has direct page HTML, direct forms, declared route records, checked SQL, validation, auth, and one live fragment without leaving the app-facing interface.

Next

Read Architecture when you want to split the single-file starter into Application/, Config/, and Web/ modules.