Iwf Guide

Iwf Guide

Markdown source

Route Specs and Forms

Iwf uses Idris types to keep routes, links, request decoding, and forms in agreement. The public interface should still feel like ordinary web code: route strings, input records, handlers, pathTo, and literal HTML forms.

The internal dependent representation exists so the compiler can prove things for you. Application code should not destructure route internals by hand.

The User-Facing Rule

Write a handlerless route spec from the HTTP method, path, and declared input types, then bind the handler:

record ArticleForm where
  constructor MkArticleForm
  title : String
  description : String
  body : String
  tagList : Maybe String

createArticle : ArticleForm -> ControllerContext -> Response
createArticle input context =
  ...

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

createArticleBinding : BoundRoute
createArticleBinding =
  handledBy createArticleRoute createArticle

The body type belongs to the route spec. handledBy reads the type of createArticle at compile time, sees ArticleForm -> ControllerContext -> Response, and checks that the handler implements the spec.

Do not write an adapter that pulls fields out of the decoded body. The binding macro generates that adapter.

Path and Query Records

Route strings name path and query inputs:

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

The {slug} capture belongs to ArticleInput.slug. A request for /articles/hello-world calls:

articleShow (MkArticleInput "hello-world") context

Query fields work the same way:

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

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

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

articleListBinding : BoundRoute
articleListBinding =
  handledBy articleListRoute articleList

Optional query inputs are Maybe fields. Repeated query inputs are List fields.

Path or Query Plus Body

When a route has both URL inputs and a request body, use two records:

record CommentInput where
  constructor MkCommentInput
  slug : String

record CommentBody where
  constructor MkCommentBody
  body : String

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

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

commentBinding : BoundRoute
commentBinding =
  handledBy commentRoute createComment

The first record is matched against the route string. Fields named in the path or query pattern come from the URL. The second record is the request body.

That rule also applies to JSON routes:

createCommentApi : CommentInput -> CommentBody -> ControllerContext -> CommentEnvelope
createCommentApi input body context =
  MkCommentEnvelope input.slug body.body

createCommentApiRoute : RouteSpec CommentInput CommentBody CommentEnvelope
createCommentApiRoute =
  post "/api/articles/{slug}/comments"
    |> params CommentInput
    |> body CommentBody
    |> respondsJson CommentEnvelope

createCommentApiBinding : BoundRoute
createCommentApiBinding =
  handledBy createCommentApiRoute createCommentApi

When a route spec declares a JSON response type, handledBy checks that the handler returns that type and wraps it as JSON.

What Gets Checked

From this declaration:

post "/articles/{slug}/comments?{notify}"
  |> params CommentInput
  |> body CommentBody
  |> html

and this handler type:

createComment : CommentInput -> CommentBody -> ControllerContext -> Response

Iwf checks:

  • slug comes from the path.
  • notify, if present on the first record, comes from the query string.
  • fields on CommentBody come from the declared request body.
  • the request body can be decoded before user code runs.
  • OpenAPI request metadata can be derived when schema information is available.

If the route string and first handler record do not agree, compilation fails. For example, a route with {slug} needs a compatible slug field.

Use pathTo instead of string concatenation:

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

Routes without path or query inputs need no input record:

homePath : String
homePath =
  pathTo homeRoute

The route value decides the call shape. If it has required path inputs, pathTo expects a record. If it has no path or query inputs, pathTo returns a String directly.

Forms

Forms stay literal HTML:

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

commentBodyBodyField is generated from CommentBody.body by FormFields. When IDRX sees that field inside a form whose action is pathTo commentRoute, it checks that the route body accepts a body : String field.

That catches common mistakes:

  • a form field name no longer exists on the body record.
  • a form field has the right name but the wrong Idris type.
  • a form points at a route whose body record does not contain that field.

The source code remains normal HTML. The proof work happens in generated Idris terms.

Request Decoding

The same body record is used for browser forms and JSON requests. The server chooses the decoder from Content-Type:

  • application/json decodes JSON fields.
  • application/x-www-form-urlencoded decodes browser form fields.
  • multipart/form-data decodes text fields and typed upload fields when the route supports file uploads.

This keeps HTML forms, JSON clients, validation, and OpenAPI metadata aligned around one handler type.

Route Specs and Runtime Bindings

Iwf has two route layers:

  • RouteSpec params body response, the importable route contract used by views, redirects, forms, and OpenAPI docs.
  • BoundRoute, the executable route produced by handledBy and used in Routes.

Normal applications write named RouteSpec declarations by starting with the HTTP method and path, then piping in URL params, request body, and response metadata. They then assemble BoundRoute bindings in a runtime route list:

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

export
htmlHomeBinding : BoundRoute
htmlHomeBinding =
  handledBy htmlHomeRoute home

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

export
htmlArticleBinding : BoundRoute
htmlArticleBinding =
  handledBy htmlArticleRoute articleShow

export
htmlCommentRoute : RouteSpec CommentInput CommentBody Response
htmlCommentRoute =
  post "/articles/{slug}/comments" |> params CommentInput |> body CommentBody |> html

export
htmlCommentBinding : BoundRoute
htmlCommentBinding =
  handledBy htmlCommentRoute createComment

export
htmlRoutes : Routes
htmlRoutes =
  [ htmlHomeBinding
  , htmlArticleBinding
  , htmlCommentBinding
  ]

The route macros build importable specs. handledBy builds the runtime route entry and generates the typed decoding adapter from the spec and handler type.

What Bugs This Prevents

These mistakes fail before the server starts:

  • a route path mentions a field missing from the handler input record.
  • a query field has an unsupported or mismatched Idris type.
  • a link omits required route input.
  • a form submits a field that is not in the request body record.
  • a form field has a stale generated name after a record rename.
  • a JSON or form request body no longer matches the handler type.

The point is not that users write dependent types. The point is that users write normal records and HTML while the compiler checks the wiring.