typedtext.io
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:
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.
Libraries/frameworks used:
Some parts were written in plain Idris 2:
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 <pre>/<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 <pre>/<code> tag combination that include a class name for a given language. The following code snippet will get syntax highlighting for JavaScript: <pre><code class="javascript">var answer = 42;</code></pre>
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.
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
AUTHOR_EMAIL: christian.rasmussen@me.com
PUBLISH_DATE: 2020-09-21
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 contrib package.
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.
Even if the view code is written in Idris 2, it is merely a DSL to generate the corresponding HTML, which means that you still need to know HTML/CSS/JavaScript in order to use it. In the future, I want to explore other ways to build user interfaces. I think Elm UI and SwiftUI have some interesting ideas in this regard.
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:
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:
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