Iwf Guide

Routing

Routes map HTTP requests to Idris handlers. In Iwf, route values are also used to build links, redirects, forms, request decoders, and OpenAPI docs.

1. A Simple Route

Write a handler:

home : ControllerContext -> Response
home context =
  render context homePage

export
htmlHomeRoute : RouteSpec NoInput NoInput Response
htmlHomeRoute =
  get "/" |> html

export
htmlHomeBinding : BoundRoute
htmlHomeBinding =
  handledBy htmlHomeRoute home

export
htmlRoutes : Routes
htmlRoutes =
  [ htmlHomeBinding
  ]

export
appRoutes : Routes
appRoutes =
  htmlRoutes

Because the route has no path captures, query parameters, or body fields, the handler only receives ControllerContext.

2. Path Parameters

Put captures in the route string and fields in the input record:

record ArticleInput where
  constructor MkArticleInput
  slug : String

articleShow : ArticleInput -> ControllerContext -> Response
articleShow input context =
  render context (articlePage input.slug)

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

articleBinding : BoundRoute
articleBinding =
  handledBy articleRoute articleShow

When a request hits /articles/hello-world, Iwf decodes slug and calls:

articleShow (MkArticleInput "hello-world") context

3. Query Parameters

Optional query parameters are Maybe fields:

record ArticleListInput where
  constructor MkArticleListInput
  tag : Maybe String
  limit : Maybe Integer
  offset : Maybe Integer

listArticles : ArticleListInput -> ControllerContext -> Response
listArticles input context =
  render context (articleListPage input)

listArticlesRoute : RouteSpec ArticleListInput NoInput Response
listArticlesRoute =
  get "/articles?{tag}&{limit}&{offset}" |> params ArticleListInput |> html

listArticlesBinding : BoundRoute
listArticlesBinding =
  handledBy listArticlesRoute listArticles

GET /articles?tag=idris&limit=20 produces:

MkArticleListInput (Just "idris") (Just 20) Nothing

4. Body Records

For forms and JSON requests, keep path/query params and body fields as separate records:

record CommentParams where
  constructor MkCommentParams
  slug : String

record CommentInput where
  constructor MkCommentInput
  body : String

createComment : CommentParams -> CommentInput -> ControllerContext -> Response
createComment params input context =
  createCommentForArticle params.slug input.body context

commentRoute : RouteSpec CommentParams CommentInput Response
commentRoute =
  post "/articles/{slug}/comments" |> params CommentParams |> body CommentInput |> html

commentBinding : BoundRoute
commentBinding =
  handledBy commentRoute createComment

The first record comes from the URL. The second record comes from the request body. The decoder is chosen from Content-Type, so the same route can accept JSON or form data when the body type supports it.

5. Links And Redirects

Use pathTo instead of string-building URLs:

articlePath : String
articlePath =
  pathTo articleRoute (MkArticleInput "hello-world")

For a RouteSpec without path/query input, call the same function without an input record:

homePath : String
homePath =
  pathTo htmlHomeRoute

The same name is used for typed Route values. When the route has no path or query input, pathTo route returns a String; when it has input, pathTo expects the generated input record.

Redirect with the generated path:

afterSave : Response
afterSave =
  seeOther (pathTo articleRoute (MkArticleInput "hello-world"))

Larger apps should keep named route values in Web/Routes.idr and group them by surface, for example htmlRoutes and apiRoutes. That file is the canonical route table: do not hand-write a second public module of route values or path helpers.

In multi-file apps, views and redirect-only controllers should import handlerless route specs from Web.Routes and call pathTo against those route values. Keep executable handledBy bindings in Web.RouteBindings so views do not import controller handlers.

6. Forms

Forms should also use route values for their action:

commentForm : Article -> CommentInput -> Html
commentForm article input =
  <form method="post" action={pathTo commentRoute (MkCommentParams article.slug)}>
    <textarea name={commentInputBodyField}>{input.body}</textarea>
    <button type="submit">Post comment</button>
  </form>

In that example, input is the CommentInput value currently being rendered; input.body reads its body field. commentInputBodyField is generated by FormFields from CommentInput.body, and renders the HTML field name "body".

When a .idrx form uses pathTo and generated FormField values, Iwf checks that form field names belong to the route body. If the form action is written directly as action={pathTo ...}, Iwf also adds the matching HTMX verb attribute, such as hx-post, hx-put, hx-patch, or hx-delete.

7. Matching And Errors

Dispatch matches path first and method second.

no matching path returns 404 Not Found.
matching path but wrong method returns 405 Method Not Allowed.
native POST forms with _method=PUT, _method=PATCH, or _method=DELETE are canonicalized before route matching, so normal browser forms can target PUT, PATCH, and DELETE routes.
generated route forms include the matching HTMX verb attribute when Iwf knows the route method.
HTMX requests do not need _method; HTMX sends the actual HTTP method.

Normal apps keep custom error pages in app handlers and still boot through runApp:

main : IO ()
main =
  runApp (app "My App" routes)

Lower-level dispatch hooks are available from the advanced route modules when a framework integration needs to own the raw request dispatch boundary.

8. Advanced Dispatch Hooks

Cross-cutting raw dispatch hooks live behind explicit advanced imports. Normal handlers should keep authentication and authorization in ordinary ControllerContext helpers unless a framework integration needs to own route dispatch policy.

Read Controllers.