Egg #6: Improved Support For Literate Programming

The Idea.

Currently the Idris compiler has basic support for literate programming. Bird-style notation together with a a special file extension is currently used to indicate that a source file is in the 'literate' style. For example:

> module LiterateModule
>
> import Effects
> import Effect.StdIO

I am free form text treated as documentation.

> ||| Unimplemented function.
> abstract func : Nat -> Nat

More free form text.

> ||| An Actual function
> addition : Nat -> Nat -> Nat
> addition x y = x + y

Text

Within Haskell there is support for the classic Bird-style and a LaTeX-style.

This RFC positions that the Idris compiler should be extended to provide:

1. Similar support for literate programming to that seen in the Haskell compiler.
2. Literate mode functionality in the Idris compiler should be extended to incorporate other functionality that aims to provide a true 'literate programming style' namely:
3. Recognition of hidden active code blocks
4. Support for other literate styles.

A true literate programming style is defined as:

the creation of documents in a known documentation system that contains executable elements without interferring with the host documentation system's original modus operandi.

A requirement of this RFC is that a literate Idris file must be processed correctly by both the host system's executable and the Idris compiler.

This will require that support must be given to both:

• a) the host system for syntax highlighting support; and
• b) the Idris compiler to recognise Literate elements.

The remainder of this RFC details a phased approach to

Phase 1: Addition of support for LaTeX style literate programming.

The first phase is to include the support for LaTeX-style literate programming. From recollection, the Haskell style requires that all code environments within the document environment should treated as executable code. For example:

\documentclass{article}
\title{A Literate Idris \& \LaTeX}
\begin{document}
\begin{code}
module LiterateModule

import Effects
import Effect.StdIO
\end{code}
\maketitle

\section{Introduction}
I am free form text treated as documentation.

\begin{code}
||| Unimplemented function.
abstract func : Nat -> Nat
\end{code}

More free form text.
\begin{code}
||| An Actual function
addition : Nat -> Nat -> Nat
addition x y = x + y
\end{code}
\end{document}

Moreso, the Idris project comes complete with an existing idrislang.sty that provides support for using Idris within LaTeX such that a code environment is already defined.

Phase 2: Better command line support for literate programming.

With the addition of multiple literate styles, a question arises over: Should the different literate-styles be used in a mutually exclusive fashion? Given the requirement that a literate style should not interfere with the host documentation system's processing, that answer is simply: yes. Also by making the use of literate styles mutually exclusive also enforces the use of a consistent literal style within a literate-idris file less confusing. Thus, a user must use either style.

To implement this functionality, the CLI to the Idris compiler needs updated. For example, long and short options for a literate flag could be:

$ idris --literate=<style> LiterateModule.lidr
$ idris -l <style> LiterateModule.lidr

With the default style selected being bird.

Phase 3: Added Hidden Executed Code Support

With basic support for multiple literate modes our attention turns towards hidden active code blocks. A feature of a literate mode should be that the programmer should be able to specify that a literate code block should not be visible when the document is processed by both the host documentation system, and the Idris compiler. For example, in lhs2tex the spec environment hides Haskell code during PDF file generation. Current practises as seen from lhs2tex, and haskell, indicate the preference for:

Bird Style

An example document written using Markdown and Bird style would be:

< module LiterateModule

# Hello 

< import Effects
< import Effect.StdIO
< %default public
    
## Stuff
    
< abstract func : ()
 
> func : Nat -> Nat

LaTeX Style

An example document written using LaTeX would be:

\documentclass{article}
\title{LiterateMode}
\begin{document}
\begin{spec}
module LiterateModule

import Effects
import Effect.Stdio
\end{spec}
\maketitle

\begin{code}
abstract
addition : Nat -> Nat -> Nat
\end{code}
\end{document}

Alternate LaTeX

With LaTeX there is the option to use LaTeX's comments to indicate hidden code, for code that falls outside of the document environment. For example:

% module LiterateModule
\documentclass{article}

% import Effects
% import Effect.StdIO
%
% %default public

\begin{document}

\begin{comment}
abstract func : ()
\end{comment}

\begin{code}
func : Nat -> Nat
\end{code}

\end{document}

This is advantageous in that comments are hidden naturally within LaTeX. Moreover the Idris file preamble can be moved to the top of the file, rather than be contained within the document environment. However special comment blocks may need to be recognised to avoid processing ordinary comment blocks as Idris code. Otherwise, ordinary LaTeX comments will be processed as Idris code. The structure of the special comment blocks are open for debate, and an example of one such style is:

%% idris
% module LiterateModule
%%
\documentclass{article}

%% idris
% import Effects
% import Effect.StdIO
%
% %default public
%%

\title{A Title}
\begin{document}
\maketitle

\begin{spec}
abstract func : String
\end{spec}

\begin{code}
addition : Nat -> Nat -> Nat
\end{code}

\end{document}

Phase 4: Support for other literate styles.

Bird style and LaTeX style are not conducive for use in other documentation systems, for example markdown. For instance, if Bird-style is used with Markdown then code blocks get treated as block quotes. Native support within the Idris compiler should be given to recognise literate code blocks in known documentation systems. Examples are given below for Markdown, and Org-Mode. Naturally, the CLI to Idris would need to be updated to recognise these alternate literate-styles.

Markdown

Within Markdown, fenced code blocks should be used to recognise visible Idris code, and HTML comments with an indicator should be used for hidden code. An example:

<!--idris
module LiterateModule
-->
# Hello

<!--idris
import Effects
import Effect.StdIO

%default public
-->

Hello again.

<!--idris
abstract func : ()
-->

```idris
func : Nat -> Nat
```

Org-Mode

Within Org-Mode, code blocks should be used for visible Idris code, and special comment blocks for hidden code.

#+IDRIS: module LiterateMode
#+TITLE: Hello

#+IDRIS: import Effects
#+IDRIS: import Effect.Stdio
#+IDRIS: %default public

Hello 

#+IDRIS: abstract func : ()

#+BEGIN_SRC idris
func : Nat -> Nat
#+END_SRC

OPT Phase 5: Make .lidr extensions optional.

Currently, literate mode is turned on by recognising a special file extension: .lidr. With changes suggested above, a literate mode flag was introduced to indicate the literate style being used.

Should the semantics of this flag be extended? Should this flag not only turn on the literate mode for a given style, but also indicate that files passed to the compiler be treated as literate files if:

1. They do not have a .idr file extension, and
2. Their file extension is one for that literate style's host documentation system.

For example, should the LaTeX style indicate that literate files have extension .tex?

$ idris --literate=latex Main.idr file.tex file.tex

Further file associations include:

Style	Extension
Bird	.lidr
LaTeX	.tex
Markdown	.markdown
Org-Mode	.org

OPT Phase 6: Improve Literate Mode in Editor Support

The literate modes of Idris-mode and Idris-vim should be updated accordingly.