How was this website built?
Ever since I started working on the Erlang code generator for Idris 2, my goal has been to be able to build websites and web services written in Idris 2. This website is an attempt at doing just that.
By using the Erlang code generator I am able to access functionality from the Erlang ecosystem. This is important, as I would not be able to write all the building blocks (like a web server) that are necessary to make even a simple website.
When building this website I had a few goals in mind:
Write blog posts as Literate Idris
I want all the Idris 2 code snippets to be type-checked (hence the name of this blog)
Support syntax highlighting of code snippets
Write the bulk of the code in Idris 2
And get more experience using the Erlang code generator
In addition to the Erlang code generator, I have created a Mix compiler to ease the integration of Idris 2 in Elixir projects: mix_idris2. This tool automatically recompiles changed Idris 2 modules.
Some parts were written in plain Idris 2:
Parsing of metadata in blog posts
Integration into Phoenix Framework
This website is built on top of Phoenix Framework. Phoenix Framework includes a bunch of middleware modules (called Plug), such as a web server (Cowboy), parsers, static files handling, routing and code reloading.
In order to integrate the Idris 2 code into Phoenix Framework, I created a wrapper around Plug.Conn. This is possible because the Erlang code generator supports calling functions in Erlang as well as exporting named functions that can be called from Erlang. Using the
Plug.Conn wrapper I wrote a very basic router in Idris 2, replacing the existing Elixir router.
The router forwards requests to the approproriate handler. The handlers have access to the
Plug.Conn.Conn value, which can be used to retrieve request parameters, set response headers, send a response etc.
To generate HTML from Markdown, I opted for an Elixir library called Earmark. This library was easy to integrate, needing just a call to
Earmark.as_html/1. Or at least, that's what I thought. I soon realized that Markdown interprets lines starting with the
> character as
<blockquote> tags, while Literate Idris see them as Idris 2 code (Bird style).
Luckily, I discovered that Earmark supports generating an AST (Abstract Syntax Tree) from the Markdown. Using this AST, I was able to transform the generated
<blockquote> tags into
<code> tags. Earmark could then generate HTML from the transformed AST. The transformation was all done in Idris 2. Below you can see how the
markdownToHtml function interoperates with Erlang (Calling the Elixir library):
markdownToHtml : String -> Maybe String
markdownToHtml contents = do
let astResult = erlUnsafeCall ErlTerm "Elixir.Earmark" "as_ast" [contents]
ast <- erlDecodeMay ((\(MkTuple3 _ ast _) => ast) <$> tuple3 (exact (MkAtom "ok")) any any) astResult
Just $ erlUnsafeCall String "Elixir.Earmark.Transform" "transform" [transformLiterateIdris ast]
The syntax highlighting is provided by highlight.js. This library looks for a
Unfortunately, highlight.js does not have a language definition for Idris. To fix this I adapted the language definition for Haskell, to make it work for Idris. The language definition for Idris is surely incomplete (it does not support namespaces for example), but it is better than nothing.
Parsing of metadata in blog posts
As mentioned above, blog posts are written as Literate Idris files. To retrieve information about the author, publish date and similar, each blog post include an HTML comment at the top. As an example, this blog post has the following metadata:
AUTHOR_NAME: Christian Rasmussen
TAGS: meta, idris2, erlang, elixir, phoenixframework, codegen, ffi
These fields (+ title, introduction and body) are parsed into an
Article record. The parser is based on Data.String.Parser from the
Each page is rendered by the server as HTML. The HTML is constructed using a very basic HTML builder. At this point, it does not even handle escaping of characters in attributes or protection from any dangerous tags.
The HTML builder is inspired by Elm's Html library, except it does not support any form of interactivity. I am using meta-programming (called elaborator reflection in Idris) to generate a function per HTML tag/attribute.
Future plans for this website
Besides writing more blog posts, I will consider adding the following functionality, mostly for fun because the low post count does not really call for any of these features:
Add RSS feed
Add search functionality
Add an archive page that lists all titles, grouped by a given period
Improve layout on mobile
Further down the road, I am hopeful that Idris 2 will add type provider functionality, like Idris 1 had. A bit simplified: A type provider is able to run
IO operations at compile-time. Some ideas of what a type provider can be used for:
Validate that the metadata in the blog posts are valid
Validate that referenced images exist on disk
Run a spell-checker when saving changes to a blog post
Pre-render the static HTML when saving changes to a blog post
Given the stated goals, I am quite happy with the result. The solutions presented here may not be perfect (Far from it), but, to me, this is only the beginning. Some of the solutions are currently relying on Erlang/Elixir-specific code. My intention is to create solutions that can work for any code generator. However, that will require more work.
If this blog post made you curious about Idris 2 or the Erlang code generator for Idris 2, you are welcome to join the Idris community at any of the locations listed here: https://www.idris-lang.org