Writing Agda Code in Another Edtior

Officially the only editor supported by the Agda-community is Emacs, through the Agda Emacs Mode. It is true that one forsakes many features by using another editor, but I want to convey my experience of using Acme for editing Agda code, and say something in general about editing Agda code without agda-mode.

Writing Agda without the training wheels?

Writing Agda-code can be seen as a very interactive process. You say where you want to go, give a partial solution containing one or more holes, and Agda will inform you what goals you have to reach in order to fill the gaps of your reasoning. The ability to leave holes is one of Agda’s greatest features, and if you have never tried programming like this — you should!

However, I often find the code which comes out of this process is not always the best. Some times I leave a hole, but the bits I wrote around the hole are not really helping. As I chase down the hole, I find my self adding more and more code to make the essence of the proof fit the oddly shaped hole I made. Of course I might realise my mistake, but if I first manage to get the hole filled then the motivation to start refactoring stuff to make it beautiful is low.

How to avoid this? I am not sure. In the course of solving a difficult problem one is bound to take detours and one will be lucky to arrive at an optimal solution at the first attempt. This seems inherent to the way we humans solve problems. I think that relying a less on the guidance of agda-mode, one can develop a better understanding of the matter at hand — that is the type checker, and the reduction of expressions.

Case study: Agda in Acme

Acme is a fantastic programming environment — a true pearl from forgotten times. Acme was designed with Unicode editing in mind. It makes very few assumptions about the nature of what you are editing, but rather integrates it self to the other tools on the system. So what happened when I tried to use it to write Agda code?

First thing one notices is that there is no syntax highlighting for Agda. Actually Acme has no syntax highlighting what-so-ever! However strange as it may sound, once you are used to living without, you do not miss it. In stead of a circus of colours on your screen, you get to focus on the beauty of the code itself. One effect of this is that I become less tolerant to clutter in the code, especially in the form of commented out code.

Next thing I did was to write a small script which runs a specific command periodically and monitors the output in an Acme window. Running the type checker in this way gives instant feedback on the status of my code every time I save the file — which I do often. One of the strengths of Acme is that the plumber — a complementary program working in sync with Acme — understands the kind of file-line-column adresses a compiler error comes with. So without any extra efforts I can right click the errors from agda to jump to the right place in the code.

Even without the interactive mode, making holes is useful, but I found that I more often would factor out the holes to a lemma with a type declaration — usually using where — and just letting the definition be ?. This would make it clear from just looking at the code what is missing. It also gave time to stop and think about the structure of the proof.

After writing like this for a while, I started having the deprecated Agda Interactive Mode running in an Acme window. Mostly just to evaluate expressions in the context of a hole, or check the odd type. I would also use this space as a scratch pad, writing down the types of various expressions currently under consideration.

To replace the jumping to the definition of a term functionality, I keep the following grep in my tagline:

> rc -c 'echo -n ''^''; cat ; echo '' ''' | grep -rn -f - $AGDA_STD

Certainly there is room for improvement on this one. I only spent one minute on the problem. However, even this simple solution allows me to mark a term with the mouse then middle-click the tag to get the type declaratation and definition of the term pop up in a window. This also prints the file and line number of the definition, so I can right click on that to open the file. Additional directories, such as the current project are simply added to the end of this command, and it will search those as well.

The AGDA_STD variable you see above is just an environment variable with the path to the agda standard library. To compile Agda-code I just use an mkfile with the following pattern:

%.agdai: %.agda
    agda -i . -i $AGDA_STD $stem.agda

Conclusions and the future

What I hope this shows is that Agda only works in Emacs is a truth with modificaions. Certainly some features of Agda are only available through the emacs mode, but these features are not essential to writing Agda code. Indeed showing some restriction as to which features one uses may improve overall code quality and readability.