Iwf Guide

Views and IDRX

Views are Idris values that render HTML. Most app views should be written in .idrx files because they look like normal HTML while still compiling through Idris.

1. A Page View

In a .idrx file you can write HTML directly:

module Web.View.Articles

import Iwf
import Generated.Schema

%default partial

export
articlePage : Article -> Html
articlePage article =
  fragment
    [ <title>{article.title}</title>
    , <main id="main-content" class="article-page">
        <h1>{article.title}</h1>
        <p>{article.description}</p>
        <section>{article.body}</section>
      </main>
    ]

The .idrx preprocessor writes generated Idris under build/generated/. Application code imports the generated module through the normal package build. For full browser requests, render inserts the default shell around the view. For HTMX requests, render returns only the main content and head-update carrier.

2. Dynamic Text

Use {...} holes for Idris values:

<h1>{article.title}</h1>
<p>{show article.favoritesCount}</p>
<section>{maybe "" id article.description}</section>

Child holes use ToHtml. Dynamic text is escaped by default.

3. Dynamic Attributes

Attribute holes use ToAttribute:

<a href={pathTo htmlArticleRoute (MkArticleSlugInput article.slug)}>
  {article.title}
</a>

<input disabled={isLocked} value={input.email} />
<img src={maybe "/assets/logo.svg" id profile.image} alt="" />

Spread attributes use ToAttributes:

let attrs = [classListAttr ["btn", "btn-primary"], dataAttr "role" "save"]
in <button {...attrs}>Save</button>

4. Lists And Conditionals

Lists of Html render directly:

tagLink : String -> Html
tagLink tag =
  <a class="tag-pill" href={"/tags/" ++ tag}>{tag}</a>

tagList : List String -> Html
tagList tags =
  <div class="tag-list">{map tagLink tags}</div>

Useful helpers:

empty
fragment
forEach
maybeHtml
htmlToString
preEscapedToHtml

Use raw/pre-escaped HTML only for content that has already been sanitized or is framework-owned.

5. Classes And Attributes

Use helpers for dynamic state:

classNames
classAttr
classes
classListAttr
whenClass
unlessClass
maybeClass
dataAttr
ariaAttr
whenAttr
unlessAttr
maybeAttr
whenAttrs
unlessAttrs
maybeAttrs

Example:

<button class={classes ["btn", whenClass isPrimary "btn-primary"]}>
  Save
</button>

6. HTMX Attributes

HTMX helpers are normal attributes:

reloadButton : String -> Html
reloadButton slug =
  let commentsPath = pathTo showArticleCommentsRoute (MkArticleSlugInput slug)
  in <button {...[hxGet commentsPath, hxTarget "#comments", hxSwap "outerHTML"]}>
    Reload comments
  </button>

Use server routes and pathTo instead of repeating route strings in views when the route already has a named value. In multi-file apps, views should import handlerless route specs from Web.Routes; executable handledBy bindings live separately in Web.RouteBindings.

7. Plain `.idr` Files

In plain .idr files, use the string-backed macro:

view : String -> Html
view title =
  idrx "<section><h1>{title}</h1></section>"

Use Idris raw strings when the IDRX contains nested Idris string literals:

link : ShowArticleInput -> Html
link input =
  idrx #"<a href={pathTo showArticleRoute input}>Read</a>"#

In .idrx files, do not write idrx <tag ...>. Write the bare tag.

8. Page Head And SEO

Put simple page titles at the top level. When a page needs additional metadata, return a top-level <head> followed by the content:

articleView : Article -> Html
articleView article =
  fragment
    [ <head>
      <title>{article.title}</title>
      {descriptionMeta article.description}
      {canonicalLink ("https://example.test/article/" ++ article.slug)}
      {openGraphTitle article.title}
    </head>
    , <main id="main-content">
        <h1>{article.title}</h1>
      </main>
    ]

The renderer merges those head entries into the full document. HTMX responses carry the same entries in a head-update template while returning only the main content.

For sitemap responses, use sitemapXml with SitemapUrl values.

Read Forms and Validation.