More Agda Tips
Literate Agda
For including Agda code in LaTeX files, Agda’s built-in literate programming support is a great tool. It typesets code well, and ensures that it typechecks which can help avoid typos.
Embedding Agda Code in LaTeX
I write the LaTeX document in one file, and the Agda code in another
.lagda
file. Using the catchfilebetweentags
LaTeX package, I can then embed snippets of the Agda code into the LaTeX
document. For instance, in a file named Lists.lagda
I can
have the following:
%<*head-type>\begin{code}
: List A → Maybe A
head \end{code}
%</head-type>
\begin{code}
= nothing
head [] (x ∷ xs) = just x
head \end{code}
Then, after compiling the Agda file with
agda --latex --output-dir=. Lists.lagda
, I can embed the
snippet head : List A → Maybe A
into the TeX file like
so:
\ExecuteMetaData[Lists.tex]{head-type}
Dealing with Unicode
Most Agda source code will be Unicode-heavy, which doesn’t work well
in LaTeX. There are a few different ways to deal with this: you could
use XeTeX, which handles Unicode better, for instance. I found it easier
to use the ucs package,
and write a declaration for each Unicode character as I came across it.
For the ∷
character above, for instance, you can write:
\usepackage{ucs}
\DeclareUnicodeCharacter{8759}{\ensuremath{\squaredots}}
Live Reloading
For plain LaTeX code, I use Spacemacs and Skim to get live reloading. When I save the LaTeX source code, the Skim window refreshes and jumps to the point my editing cursor is at. I use elisp code from this blog post.
For Agda code, live reloading gets a little trickier. If I edit an
Agda source file, the LaTeX won’t automatically recompile it. However,
based on this
stack exchange answer, you can put the following .latexmkrc
file in the same directory as your .lagda
files and your
.tex
file:
'lagda','tex',0,'lagda2tex');
add_cus_dep(
sub lagda2tex {
my $base = shift @_;
return system('agda', '--latex', '--latex-dir=.', "$base.lagda");
}
This will recompile the literate Agda files whenever they’re changed.
Unfortunately, it doesn’t automate it the first time you do it:
it needs to see the .tex
files to see the dependency. You
can fix this yourself, by running
agda --latex --output-dir=.
when you add a new
.lagda
file (just once, after that the automation will take
over), or you can use a script like the following:
#!/bin/bash
find . -type f -name '*.lagda' | while read -r code ; do
dir=$(dirname "$code")
file=$(basename "$code" .lagda).tex
if [ ! -e "$dir/$file" ]
then
agda --latex --latex-dir=. "$code"
fi
done
This will compile any .lagda
file it finds that
doesn’t have a corresponding .tex
file (so it
won’t slow things down). Then call that script on the first line of your
.latexmkrc
, like so:
system("bash ./init-missing-lagda.sh");
'lagda','tex',0,'lagda2tex');
add_cus_dep(
sub lagda2tex {
my $base = shift @_;
return system('agda', '--latex', '--latex-dir=.', "$base.lagda");
}
Flags for Debugging
There are a number of undocumented flags you can pass to Agda which
are absolutely invaluable when it comes to debugging. One of them can
tell you more about termination checking, another reports on type
checking (tc
), another for profiling
(profile
), and so on. Set the verbosity level
(agda -v 100
) to get more or less info.
Type Checking Order
Agda does type checking from left to right. This isn’t always desired: as an example, if we want to annotate a value with its type, we can use the following function:
: ∀ {a} (A : Set a) → A → A
the _ x = x
the
: _
example = the ℕ 3 example
Coming from Haskell, though, this is the wrong way around. We usually
prefer to write something like 3 :: Int
. We can’t write
that as a simple function in Agda, though, so we instead use a syntax
declaration:
syntax the ty x = x ∷ ty
: _
example = 3 ∷ ℕ example
Changing the order of type checking can also speed up typechecking in some cases. There’s more information about syntax declarations in Agda’s documentation.