# 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: ```idris home : ControllerContext -> Response home context = render context homePage ``` Register it: ```idris 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: ```idris 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: ```idris articleShow (MkArticleInput "hello-world") context ``` ## 3. Query Parameters Optional query parameters are `Maybe` fields: ```idris 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: ```idris MkArticleListInput (Just "idris") (Just 20) Nothing ``` ## 4. Body Records For forms and JSON requests, keep path/query params and body fields as separate records: ```idris 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: ```idris articlePath : String articlePath = pathTo articleRoute (MkArticleInput "hello-world") ``` For a `RouteSpec` without path/query input, call the same function without an input record: ```idris 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: ```idris 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: ```idris commentForm : Article -> CommentInput -> Html commentForm article input =
``` 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`: ```idris 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. ## Next Read [Controllers](controllers.md).