Blogging Literately: markdown from literate agda

This post discusses how we achieved writing our articles using literate-style coding and having the results transformed into markdown for processing with Hakyll. Afterwards, an example is shown —in fact, this post is a literate document realized by our scripts below.

module blogliterately where

Problem Statement

Ideally, I would like to write my blog posts as mostly-literate documents in-case I desire, say, to produce PDFs from them. I would like to write

    ---
    title: my literate document
    date: August 20, 1991
    ---
    english and latex
    english and latex
    begin{code}
      lots of math, i.e., agda
    end{code}
    more english and latex

and have that translate to a .markdown file for Hakyll to use.

One of my main usages for LaTeX comments is to use them to fold, or organize, the structure of my document. I use folding-mode.el for Emacs.

Problem Solution

As done in the first post, we write a script that converts the code-block delimiters from the literate style to the so-called fenced-style of Pandoc, then move the resulting file to the blog/posts directory -we keep the literate files in their own directory blog/literate. Along the way we translate LaTeX forward-quotes to markdown single-quotes, ignore LaTeX comments, savagely delete any line containing a LaTeX command (i.e., a backslash), and transform literate in-line code-delimiters into markdown back-ticks.

Again, the major advantages of such a translation is that it’d be easier for me to produce PDF’s from blog-posts and I’d use the same literate-agda syntax I’m accustomed to. Also, I tend to view my work in PDF form, and so this will be a pleasant familiarity for me.

Running fromliterate on the literate source file of this page produces markdown which is used to generate this page. The same literate source leads to PDF by running NAME=blogliterately ; lhs2TeX --agda $NAME.lagda > $NAME.tex && pdflatex $NAME.tex at the command-line. Admittedly, the PDF has room for improvement, but with little effort can be made clear —emphasis on ‘little’!— then again, I might incorporate more changes into the script when I need them. Perhaps most importantly, I can edit the code within Emacs by C-c C-l and prepare it for presentation in the same file!

The rest of the article is just an example of our script’s power.

Example Usage :: What does it mean: ‘lists with concatenation form a monoid’?

To understand the phrase we need to understand what lists are, what concatenation is, and what a monoid is. A monoid is a set with an operation such that certain equations hold –wait to talk of equations, we need to know what equality means. Let’s begin there!

Equality is an ‘easy one’

It’s a type x ≡ y for any x , y of the same type,

data _≡_ {T : Set} : (x y : T) → Set where

such that any element x is equal to itself

  ≡-refl : ∀{x} → x ≡ x

and there are no other ways to construct equality proofs besides this.

Let’s take equality to be an infix operation with a relatively low binding,

infix 5 _≡_

An important property is ‘substitution of equals for equals’, or Leibniz Principle,

≡-cong : ∀{A B} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
≡-cong f ≡-refl = ≡-refl

What this says is that given p : x ≡ y we must have p is ≡-refl since that is the only way to construct an equality proof. But if p is ≡-refl the necessarily x and y are the same item –‘definitionally equal’. But then f x and f y are also definitionally equal and so ≡-refl is a valid proof and we are done.

We want to avoid such paragraphs of English expaining a single line of code. So we introduce combinators for reflexitivity and transitivity of equality:

infix 8 _∎
_∎ : ∀{A} (x : A) → x ≡ x
x ∎ = ≡-refl

infixr 5 _≡⟨_⟩_
_≡⟨_⟩_ : ∀{A} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
y ≡⟨ ≡-refl ⟩ ≡-refl = ≡-refl

Why the funky-looking names? Keep reading ;)

Before you move on, test your comprehension by proving a restatement of Leibniz Principle: those that share all properties are necessarily identical.

exercise : ∀{A} {x y : A} → (given : ∀ {P : A → Set} → P x → P y) → x ≡ y

Monoids are one-sorted structures

The suffix -oid is usually taken to mean sorted or typed, as in ‘ringoid’ and ‘groupoid’, and the prefix mono- means one. So monoid means, more-or-less, one-typed —the generalization is called a category ;)

The notion of a type arises from the observation that all functions A → A with function-composition and the identity function form a monoid.

Enough shenanigans! What is a monoid? It is a type

record Monoid : Set₁ where
 field

that consists of a set

  𝒮 : Set  -- slash-McS is the agda-input sequence in emacs
  -- looks really nice in the PDF ;) check it out!

with a particular element

  0₊ : 𝒮

and a binary operation on that set

  _⊕_ : 𝒮 → 𝒮 → 𝒮

such that the operation is associative

  ⊕-assoc : ∀{x y z} → (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)

and it has 0₊ as a unit

  rightId  : ∀{x} → x  ⊕ 0₊ ≡ x
  leftId : ∀{y} → 0₊ ⊕  y ≡ y

We can list it!

A ‘list of type A’ is a type

data List (A : Set) : Set where

that has an ‘empty list’

  [] : List A

and every non-empty list can be expressed as an element of A followed by a list of type A:

  _∷_ : A → List A → List A  -- slash-::

Given any two lists, we can stick them ‘side by side’, or ‘concatenate’ them, to produce another list:

infix 10 _++_

_++_ : ∀{A} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

As will be immediately clear, let us make a synonym,

definition : ∀{A} {x : A} → x ≡ x
definition = ≡-refl

Now we prove associativity of concatenation by casing on the two possible forms of the argument xs. We case on this argument since it is the left argument of ++ which is defined inductively on its left-argument.

++-assoc : ∀{A} {xs ys zs : List A} →  (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc {xs = []} {ys} {zs} =
   ([] ++ ys) ++ zs
  ≡⟨ definition ⟩    -- i.e., first clause of definition of ++
    ys ++ zs
  ≡⟨ definition ⟩ 
   [] ++ (ys ++ zs)
  ∎
++-assoc {xs = x ∷ xs'} {ys} {zs} =
    ((x ∷ xs') ++ ys) ++ zs
  ≡⟨ definition {- of ++, second clause -} ⟩
    (x ∷ (xs' ++ ys)) ++ zs
  ≡⟨ definition {- of ++, first clause -} ⟩
    x ∷ ( (xs' ++ ys) ++ zs)
  ≡⟨ (let inductive-step : (xs' ++ ys) ++ zs ≡ xs' ++ (ys ++ zs)
          inductive-step = ++-assoc {xs = xs'}{ys = ys}{zs = zs}
      in ≡-cong (λ l → x ∷ l) inductive-step) ⟩
    x ∷ (xs' ++ (ys ++ zs))
  ≡⟨ definition {- of ++, first clause -} ⟩ 
    (x ∷ xs') ++ (ys ++ zs)
  ∎

Notice that we began with xs being x ∷ xs' then at the inductive step we used the structurally smaller list xs'.

Notice how we have a ‘calculational’, or equational, proof and such style is not even primitively supported in the language! After all, you witnessed the definitions of the combinators above!

Of-course, since all we did was mostly chase definitions, we can rewrite the lengthy proofs more succinctly as

++-assoc' : ∀{A} {xs ys zs : List A} →  (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc' {xs = []} = ≡-refl
++-assoc' {xs = x ∷ xs'} = ≡-cong (λ l → x ∷ l) (++-assoc {xs = xs'})

Which you choose depends on your level of comfort —both with the language and with the theory.

The reader would do well to show that [] is a unit of _++_ and so we have a monoid:

freemon : ∀{A : Set} → Monoid
freemon {A} =
  record
    { 𝒮 = List A
    ; 0₊ = []
    ; _⊕_ = _++_
    ; ⊕-assoc = λ {x y z} → ++-assoc {A} {x} {y} {z}
    ; rightId = {! exercise!}
    ; leftId = {! exercise!}
    }

Since this article is in-fact a literate document, the reader need only load it into their Emacs and begin having fun.

Enjoy!