Iwf Guide

Forms and Validation

Iwf forms are normal HTML forms backed by typed routes and input records. The route decides where the form submits. The input record decides which fields are accepted.

1. Define The Input Record

Create a record for the submitted fields:

record SettingsForm where
  constructor MkSettingsForm
  email : String
  username : String
  bio : Maybe String

Derive form fields:

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

This generates field values such as:

settingsFormEmailField : FormField SettingsForm "email" String
settingsFormUsernameField : FormField SettingsForm "username" String

When you rename a record field, the generated field value changes too. Stale form field names fail at compile time.

2. Define The Submit Route

A handler with a body record receives decoded form data:

saveSettings : SettingsForm -> ControllerContext -> Response
saveSettings input context =
  case validateSettings input of
    Left errors => renderValidation context input errors settingsPage
    Right valid =>
      flashInContext "notice" "Settings saved" context
        (seeOther (pathTo settingsRoute))

settingsRoute : RouteSpec NoInput SettingsForm Response
settingsRoute =
  put "/settings" |> body SettingsForm |> html

settingsBinding : BoundRoute
settingsBinding =
  handledBy settingsRoute saveSettings

For routes with path/query params and body fields, use two records:

createComment : CommentParams -> CommentInput -> ControllerContext -> Response

The first record comes from the URL. The second record comes from the request body.

3. Render The Form

In .idrx, write normal HTML:

settingsForm : SettingsForm -> List ValidationError -> Html
settingsForm input errors =
  <form id="settings-form" class="form stack" method="post" action={pathTo settingsRoute}>
    {errorSummary errors}
    <label class="field">
      <span>Email</span>
      <input name={settingsFormEmailField} value={input.email} type="email" />
    </label>
    <label class="field">
      <span>Username</span>
      <input name={settingsFormUsernameField} value={input.username} />
    </label>
    <button class="btn-primary" type="submit">Update settings</button>
  </form>

render injects the CSRF hidden input into non-GET forms.

Route-backed forms are HTMX-enhanced by default when the .idrx macro can see the target route. Write the form action directly as action={pathTo ...} and Iwf renders the matching HTMX verb attribute:

<form action="/settings" hx-patch="/settings" method="POST">
  ...
</form>

If the action is a precomputed String, the macro cannot recover the route method or body membership from that string. Keep pathTo visible in the form attribute when you want compile-time field checks and generated HTMX verbs.

Iwf still keeps the native HTML fallback. Browsers without JavaScript only submit GET or POST. For a PUT, PATCH, or DELETE route, Iwf accepts the common method-override pattern:

<form method="post" action="/settings">
  <input type="hidden" name="_method" value="PATCH">
  ...
</form>

The browser still sends POST, but Iwf reads _method and treats the request as PATCH before route matching. Direct forms should spell that hidden field explicitly when they need a no-JavaScript fallback for PUT, PATCH, or DELETE routes.

If you write an HTMX-only control yourself, use the HTMX verb directly:

<button hx-patch="/settings" hx-target="#settings-form">Save</button>

Use hx-put, hx-patch, or hx-delete for the HTMX request. Keep _method only when the same form should also work as normal HTML without JavaScript.

4. Decode And Validate

For simple records:

settingsFormDecoder : FromFormBody SettingsForm
settingsFormDecoder =
  derivedFromFormBody settingsFormParams settingsFormFromParams

Useful validation helpers:

requiredString
minLength
matches
fieldError

Validation returns:

Either (List ValidationError) value

Render errors back to the same page:

renderValidation context input errors settingsPage

Use renderValidationWithFlashes when the failed response should also set flash messages. Submitted values stay in the input record, field errors are rendered, CSRF still works, and boosted HTMX requests stay on the fragment path.

5. Direct Forms Are Canonical

The public surface is literal HTML plus typed values:

action={pathTo route ...} for the route-backed URL.
Generated FormField values for name attributes.
A normal method, enctype, and optional _method hidden field when the form needs a browser fallback for non-POST routes.

This keeps the interface inspectable as HTML while still letting Idris check that field names match the route body at compile time.

6. Multipart Forms

Use multipart when the body contains files:

<form method="post" enctype="multipart/form-data" action="/avatar">
  <input type="file" name="avatar" />
  <button type="submit">Upload</button>
</form>

Route bodies can contain:

UploadedFile
Maybe UploadedFile
List UploadedFile

Use multipartFile for one file and multipartFilesFor for repeated uploads when you need to inspect raw multipart data.

uploadAvatar : MultipartFormData -> IO (Either String StoredFile)
uploadAvatar formData =
  case multipartFile "avatar" formData of
    Nothing => pure (Left "missing avatar upload")
    Just file =>
      storeUploadedFile
        (localFileStorage (MkLocalFileStorage "uploads" "/uploads"))
        file

7. CSRF

render injects CSRF fields into non-GET forms. Validate submitted forms with:

validateSessionCsrf
handleProtectedFormWith

The CSRF token is stored in the signed session.

For the dependent-type mechanics behind FormField, route body membership, and IDRX form checks, see Dependent Routes and Forms.

Read Database and Migrations.