3 Getting Started

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

Perhaps the greatest barrier to taking this course might be setting up the required tools, if you want to use your own machine. I have only done this on Mac OS X, and I did run into some issues (which, fortunately, I could solve). If you are using Windows or Linux, there is a limit to how much help I can give.

Agda interaction is best managed with the Emacs text editor. Other alternatives are less supported and more buggy. (You’re welcome to try them, but I can’t offer support if things go wrong.) This means you need to install the current versions of Haskell, Emacs, Agda, and the Agda standard library (a separate install step). If you are doing this using your Linux package manager, check version numbers against the ones given here, as some distributions run behind. We’re using 2.6.1.3, which is what the PLFA code is checked against currently. But probably anything from 2.6.0.x to 2.6.2.x should work.

On OS X, you can try to do everything through Homebrew, or you can try installing the various components separately. You can’t mix and match, because there seems to be no way to tell Homebrew that you’ve already installed part of what it needs. I installed Emacs through Homebrew, Haskell using the Haskell Platform, and Agda from source. It takes a long time to build it from source.

Emacs: https://www.gnu.org/software/emacs/
Haskell: https://www.haskell.org
Agda: https://agda.readthedocs.io/

The last time I used Homebrew, it installed the standard library, but if you’re installing from source, you have to do that yourself, a step that’s easy to overlook. PLFA uses version 1.3; we are using 1.5, though I suspect anything from 1.3 to 1.7 will be compatible.

Agda standard library: https://github.com/agda/agda-stdlib

I will provide cut-down and tweaked versions of the PLFA Agda code, so you don’t need to set up PLFA as a library, unless you want to work with the original files.

You will need to configure Emacs to automatically use Agda mode when a file with the .agda (or .lagda for "literate" files) extension is loaded. This is typically done as part of Agda installation but sometimes it doesn’t work properly and you have to edit your .emacs initialization file.

It’s best to use a graphical version of Emacs. Some commands may not work in the terminal version, and getting to menu items is awkward. This is particularly true of the older terminal version that comes with Mac OS X.

You don’t need to know a lot of Emacs to work with Agda, but you need to know the basics. You can use the mouse (unless you’re remotely logged into a server, in which case even some important keyboard commands may not work for you). Arrow keys should work. But learning some basic keyboard commands will speed things up for you. There is a built-in Emacs tutorial, which you can run by typing C-h t. (That’s control and h together, followed by t.) Take notes, especially on how to exit Emacs. A lot of what’s in the tutorial isn’t necessary (all the C-u stuff) but you should learn basic navigation, cut-and-paste, and search. Here are some commands mentioned in the tutorial, separated here by semicolons, that I find useful and recommend to you. I haven’t documented them here because you should learn about them through the tutorial.

C-x C-c; C-x k; C-g; C-v; M-v; C-l; C-p; C-n; C-b; C-f; M-f; M-b C-a; C-e; M-<; M->; C-x 1; C-<SPC>; C-w; C-y; M-y; C-/; C-x C-f; C-x C-s; C-x C-b; C-x b; C-s; C-r

The Agda documentation can be frustrating. Its organization is quirky, and parts are incomplete. The documentation for Agda Emacs mode is fairly brief. I still don’t know what many of the commands do. Fortunately, we can get along with relatively few commands. There are, however, a lot of Unicode characters we’d like to insert, and that process generally starts by typing backslash (\), followed by a few characters. The documentation shows some of these shortcuts, but not nearly enough.

If you have a file with a character in it that you’d like to see the shortcut for, you can put the cursor on it and use the menu item "Information about the character at point". Sometimes that information is incomplete or even incorrect. The Emacs command M-x agda-input-show-translations (you can just type M-x agda-i and hit the TAB key) will give a complete list that you can poke through. Sometimes there are many characters associated with a shortcut. For example, if you type \r, you will get the short single right arrow, which is used a lot. But there are many other right arrows available, and you’ll see a numbered list in the echo area at the very bottom of the Emacs frame. You can type a number to choose one, and then it will be the default choice next time.

You shouldn’t be browsing in the Agda standard library in search of assignment solutions, but if you want to use it for your own work, you will need to become familiar with its structure. The entire source is on GitHub, as described above but there is also a site hosting an HTML version that has nice cross-links and some useful README files.

Agda standard library browser: https://agda.github.io/agda-stdlib/index.html