Edit:
A few things to note:
- my agda-helper program is obsolete, given that “agda -I” works (though it might say that it’s not supported). :typeOf is equivalent to the :t in agda-helper.
- the problems getting emacs’s agda-mode to work properly was due to a version mis-match between the Haskell Agda library and the Agda I installed with apt-get.
- to fix everything, build Agda from source or find an up to date binary rather than using apt-get
Original Post
Agda is a dependently typed, functional programming language. It bears some syntactic resemblance to Haskell, though I am told that once I actually start using it, I’ll find this resemblance to only be skin deep. This post is not about the Agda programming language, but about the development environment one uses when programming in Agda. That is, it’s about the tools used to write, compile, check and test Agda code. More specifically, it’s about my experience setting up these tools on my computer. I’m posting this because the experience was somewhat tedious, and so knowledge of it may help others make their experiences less tedious. It also resulted in the development of a simple tool that might make some people’s lives easier when testing Agda programs, but more on that later.
Installing Agda
For the record, my box runs 64 bit Ubuntu 12.04. The first thing I did was:
% apt-get install agda
So far so good. Next, I installed the Agda libraries for Haskell. “Agda libraries for haskell?” you ask. Operations on Agda programs are done through a Haskell interface. For people new to Haskell, it has its own package manager called “cabal”.
% cabal install agda agda-executables
And cross your fingers. Cabal has always been very touch and go in my experience, but after re-installing ghc (the Haskell compiler) and deleting my “~/.cabal” directory several times the, gods of Haskell decided to grant me with a working install of the Agda-2.3.0.1 library (the version compatible with ghc7.4.1 which I happen to run). I know there was probably a more elegant way to install that, but meh - it worked. For people treating this as instructions for setting up Agda, I recommend you at least try to install the Haskell library without doing what I did.
Hello, World?
Not exactly. Once Agda was installed, I had a nice little “agda” binary that was, among other things, an Agda compiler. I wrote a little Agda program to make sure everything worked. It wasn’t the traditional first-program-in-language, that just prints out “Hello, World!”, because in Agda, like in most functional languages, the emphasis is on defining equations rather than doing things, and printing out a string is doing something so is actually non-trivial. Instead, I defined a simple type:
-- file: hello.agda
module hello where
data Blah : Set where
a : Blah
Without getting into too much detail, this code defines a type “Blah”, and a data constructor “a” that is a member of that type. It’s worth noting that this will not compile, since it lacks a “main” function (which is what the compiled program does when it’s run). But it took me a while for me to figure out how to get that information.
I’ll highlight my thought process. First I looked at the documentation that came with Agda:
[/home/steve]
[steve@stevebox] $ agda --help [19:20:24]
Agda
Usage: agda [OPTIONS...] FILE
-V --version show version number
-? --help show this help
-I --interactive start in interactive mode
-c --compile compile program using the MAlonzo backend (experimental)
--epic compile program using the Epic backend
--js compile program using the JS backend
--compile-dir=DIR directory for compiler output (default: the project root)
--ghc-flag=GHC-FLAG give the flag GHC-FLAG to GHC when compiling using MAlonzo
--epic-flag=EPIC-FLAG give the flag EPIC-FLAG to Epic when compiling using Epic
--test run internal test suite
--vim generate Vim highlighting files
--html generate HTML files with highlighted source code
--dependency-graph=FILE generate a Dot file with a module dependency graph
--html-dir=DIR directory in which HTML files are placed (default: html)
--css=URL the CSS file used by the HTML files (can be relative)
--ignore-interfaces ignore interface files (re-type check everything)
-i DIR --include-path=DIR look for imports in DIR
--no-forcing disable the forcing optimisation
--safe disable postulates, unsafe OPTION pragmas and primTrustMe
--show-implicit show implicit arguments when printing
-v N --verbose=N set verbosity level to N
--allow-unsolved-metas allow unsolved meta variables (only needed in batch mode)
--no-positivity-check do not warn about not strictly positive data types
--no-termination-check do not warn about possibly nonterminating code
--termination-depth=N allow termination checker to count decrease/increase upto N (default N=1)
--no-coverage-check do not warn about possibly incomplete pattern matches
--type-in-type ignore universe levels (this makes Agda inconsistent)
--sized-types use sized types (inconsistent with coinduction)
--injective-type-constructors enable injective type constructors (makes Agda anti-classical and possibly inconsistent)
--guardedness-preserving-type-constructors treat type constructors as inductive constructors when checking productivity
--no-universe-polymorphism disable universe polymorphism
--universe-polymorphism enable universe polymorphism (default)
--no-irrelevant-projections disable projection of irrelevant record fields
--experimental-irrelevance enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)
--without-K disable the K rule (maybe)
Plugins:
That’s actually it. There is no man page for this program. The first bit of that that looked relevant is the “-c” option which compiles an Agda program. This was before I realized the necessity for a main function. So I ran:
$ agda -c hello.agda
The resulting error message explains that I need a main function. Good we’re getting somewhere.
Then I tried importing a standard library function into my agda program. I added this line to the start of the module:
open import Data.Char
and compiled:
[/home/steve/src/agda]
[steve@stevebox] $ agda -c test.agda [19:39:35]
Checking test (/home/steve/src/agda/test.agda).
/home/steve/src/agda/test.agda:3,1-22
Failed to find source of module Data.Char in any of the following
locations:
/home/steve/src/agda/Data/Char.agda
/home/steve/src/agda/Data/Char.lagda
when scope checking the declaration
open import Data.Char
Pretty easy to figure out what’s going on here. The compiler doesn’t know where to look for the standard library. I had a wild stab in the dark:
[/home/steve/src/agda]
[steve@stevebox] $ ls /usr/share/agda-stdlib [19:41:35]
Algebra/ Foreign/ IO/ Algebra.agda Coinduction.agdai Induction.agda IO.agdai Record.agda Reflection.agdai Universe.agda
Category/ Function/ Level/ Algebra.agdai Function.agda Induction.agdai Level.agda Record.agdai Size.agda Universe.agdai
Data/ Induction/ Relation/ Coinduction.agda Function.agdai IO.agda Level.agdai Reflection.agda Size.agdai
(I tab-completed from “ag”.) Yay I found it! Looking back at the usage of “agda”, I use “-i” to add import paths. So:
[/home/steve/src/agda]
[steve@stevebox] $ agda -c -i /usr/share/agda-stdlib test.agda [19:41:40]
The name of the top level module does not match the file name. The
module test should be defined in one of the following files:
/usr/share/agda-stdlib/test.agda
/usr/share/agda-stdlib/test.lagda
Huh? It’s looking for my source file “test.agda” in the import path. This story will be resolved later, but first, a tangent:
Enter Emacs
It was around this time that someone on the IRC channel on which I was asking for help asked if I was using emacs (I wasn’t) and I asked if I should be (and the reply was “yes”).
Emacs is a very extensible text editor with many powerful tools to help programmers. Some extensions exist for various languages that add tools for testing and compiling code from in the editor. One such extension exists for Agda, and it was installed when I apt-got Agda (but all the documentation I read said I should have gotten a “agda-mode” binary with Agda (I didn’t) and when I run that it will install agda-mode in emacs (the name of the agda extension)).
At this point I’ll make readers aware that I use VIM as my editor of choice. I have nothing against emacs, I just happened to be around lots of VIM users when I outgrew gedit (another editor).
So I quickly learnt the basics of emacs. This was a bit frustrating because I’ve spent the better part of the last three years building up muscle memory for VIM shortcuts (dvorak VIM shortcuts mind you), and having to learn an entire new set of commands with lots of Control and Meta key presses was…unpleasant. Nevertheless, emacs’s agda-mode gave me a nice drop-down menu of things to do with Agda code (including compile, evaluate an expression and find the type of an expression).
So I tried compiling my code with the standard library import. I got an error message:
Problem encountered. The *ghci* buffer can perhaps explain why.
(ghci is the name of an interactive Haskell interpretter.)
Nice. This was before I realized that Agda operations are performed through a Haskell interface, and before I learnt all about buffers in emacs, so I was pretty confused by this. I found out that buffers are effectively containers for text. When you open a file in emacs, its contents is copied to a buffer. When you save a file, the buffer is written to the file on disk. Buffers can also exist for non-files, and the ghci buffer is one such example. Since Haskell is used to compile Agda, a ghci session is run which can be accessed in a ghci buffer. It allows you to interact with the ghci shell just as you normally would in a terminal. After the failed compile attempt, I had a look at the buffer:
HCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :set -package Agda-2.3.0
cannot satisfy -package Agda-2.3.0
(use -v for more information)
Prelude> :mod + Agda.Interaction.GhciTop
location info>:
Could not find module `Agda.Interaction.GhciTop'
It is a member of the hidden package `Agda-2.3.0.1'.
Prelude> ioTCM "/home/steve/src/agda/test.agda" Nothing ( cmd_write_highlighting_info "/home/steve/src/agda/test.agda" "/tmp/agda2-mode8592JyE" )
<interactive>:4:1: Not in scope: `ioTCM'
<interactive>:4:50: Not in scope: `cmd_write_highlighting_info'
Prelude> ioTCM "/home/steve/src/agda/test.agda" (Just "/tmp/agda2-mode8592jGR") ( cmd_compile MAlonzo "/home/steve/src/agda/test.agda" [".", "/usr/share/agda-stdlib"] )
<interactive>:5:1: Not in scope: `ioTCM'
<interactive>:5:74: Not in scope: `cmd_compile'
<interactive>:5:86: Not in scope: data constructor `MAlonzo'
Alright. So something is going horribly wrong. This first thing that fails (well, the first thing it’s trying to do) is setting the package to “Agda-2.3.0” (the Agda library package for Haskell I installed at the start). But hang on. The version of that package was 2.3.0.1, not 2.3.0. At some point, wires are getting crossed about which version of Agda to load, and the wrong one is being attempted and failing because it doesn’t exist. Ok, so this is an interactive shell, so I can fix this. At the ghci prompt, I ran:
Prelude> :set -package Agda-2.3.0.1
package flags have changed, resetting and loading new packages...
...
Lookin’ good! Let’s try compiling. The ghci buffer says:
Prelude> ioTCM "/home/steve/src/agda/test.agda" (Just "/tmp/agda2-mode8592Xvp") ( cmd_compile MAlonzo "/home/steve/src/agda/test.agda" [".", "/usr/share/agda-stdlib"] )
<interactive>:5:1: Not in scope: `ioTCM'
<interactive>:5:74: Not in scope: `cmd_compile'
<interactive>:5:86: Not in scope: data constructor `MAlonzo'
Aww man! Ok so ioTCM is a function for doing Agda magic, but it’s not currently in scope. Loading the package made ghci aware of the existence of some Haskell modules, and ioTCM resides within one of them. In ghci, there is a “:browse” command that lists the functions in a module, and this coupled with some nice tab-completion inside ghci means I can navigate around the modules inside the Agda package. But this doesn’t really help me find the function quickly.
Here’s my solution. Forget about Haskell for a second. Even if these Haskell modules are compiled code, in order for them to be of any use, people have to be able to call functions from inside them using a function call in source code. For this to work, the name of each function probably exists in plain text somewhere in the module file which contians it. And how do we find a string inside a file inside a directory structure? GREP!
[/home/steve]
[steve@stevebox] $ grep -rn 'ioTCM' ~/.cabal/lib [20:29:16]
Binary file /home/steve/.cabal/lib/Agda-2.3.0.1/ghc-7.4.1/libHSAgda-2.3.0.1.a matches
Binary file /home/steve/.cabal/lib/Agda-2.3.0.1/ghc-7.4.1/Agda/Interaction/GhciTop.hi matches
Binary file /home/steve/.cabal/lib/Agda-2.3.0.1/ghc-7.4.1/HSAgda-2.3.0.1.o matches
Once again, possibly not the most elegant way to solve the problem but it works and it works fast. This reveals that the module is “Agda.Interaction.GhciTop”. So let’s import it!
Prelude> import Agda.Interaction.GhciTop
Prelude Agda.Interaction.GhciTop>
And compile again. The long pause means that it works. It will have compilation errors, but at least the compiler is being invoked. Success.
Now let’s do something useful
…where useful is context sensitive and this is the context of learning Agda. When I was learning Haskell, the most valuable tool by far was ghci (yes, the prompt that I just fought to get my Agda to compile). It lets you enter Haskell expressions and it will print out what the expression returns. You can define functions, and then call them. It lets you load a Haskell source file and use functions and types defined in that file in the interactive shell. Here’s an example:
Prelude> concat ["hello", "world"]
"helloworld"
Prelude> 1 + 2
3
Prelude> let incr = (1+)
Prelude> incr 5
6
Haskell is strongly typed, and as a result, it’s much easier to encounter type errors than in say, perl. Sometimes, it’s useful to confirm the types of expressions with Hasell’s type checker before using them. ghci can do this:
Prelude> :t concat
concat :: [[a]] -> [a]
Prelude> :t (+)
(+) :: (Num a) => a -> a -> a
As more information gets encoded in the type system, this tool becomes more and more useful. In Agda, the type system is more powerful than in Haskell, and more information can be encoded in it. As such it would be very useful to have a similar tool. I asked if such a tool was available on the IRC channel and was told that in emacs, C-c C-d can be used to check the type of an expression. Similarly, C-c C-n can be used to evaluate or “normalize” an expression.
But I missed the way it worked in ghci. In emacs, I can’t see my history as I enter new expressions to infer types or normalize. Doing it all through emacs just felt too constrictive.
Remember how when I did anything Agda the Haskell function being called would be sent to the ghci buffer. When I use emacs to infer types or normalize, I can see the Haskell function call being made. I jumped into my own ghci shell in a terminal and tried to reproduce the results:
Prelude Agda.Interaction.GhciTop> ioTCM "/home/steve/src/agda/test.agda" (Just "/tmp/agda.tmp") ( cmd_load "/home/steve/src/agda/test.agda" [".", "/usr/share/agda-stdlib"] )
...
Prelude Agda.Interaction.GhciTop> ioTCM "/home/steve/src/agda/test.agda" Nothing ( cmd_compute_toplevel False "a" )
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Normal Form*" "a")
agda2_mode_code (agda2-goals-action '())
Prelude Agda.Interaction.GhciTop> ioTCM "/home/steve/src/agda/test.agda" Nothing ( cmd_infer_toplevel Agda.Interaction.BasicOps.Normalised "a" )
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Inferred Type*" "Blah")
agda2_mode_code (agda2-goals-action '())
There is a lot of superfluous information there, but the value and type of the expression “a” is displayed. Knowing the Haskell functions that get this information, I knocked together a command line program that behaves similarly to ghci for type inferring and expression evaluation.
Get it here: agda-helper
Here’s an example of its use using the hello.agda from earlier:
$ ./agda-helper hello.agda
...
hello.agda:
a
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Normal Form*" "a")
agda2_mode_code (agda2-goals-action '())
hello.agda:
:t a
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Inferred Type*" "Blah")
agda2_mode_code (agda2-goals-action '())
hello.agda:
:t 'c'
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Inferred Type*" "Char")
agda2_mode_code (agda2-goals-action '())
hello.agda:
'c'
agda2_mode_code (agda2-status-action "Checked")
agda2_mode_code (agda2-info-action "*Normal Form*" "'c'")
agda2_mode_code (agda2-goals-action '())
So it still prints the same stuff as before but now there is a nice wrapper. I might make a little perl script to wrap this to scrape out the meaningful information in the future.
Compiling from a terminal
I almost forgot. I was having this problem:
[/home/steve/src/agda]
[steve@stevebox] $ agda -c -i /usr/share/agda-stdlib test.agda [19:41:40]
The name of the top level module does not match the file name. The
module test should be defined in one of the following files:
/usr/share/agda-stdlib/test.agda
/usr/share/agda-stdlib/test.lagda
While I was reading an online tutorial, I came upon the solution:
[/home/steve/src/agda]
[steve@stevebox] $ agda -c -i /usr/share/agda-stdlib -i . test.agda [19:41:40]
The “-i .” tells the compiler to also look in the current directory. Don’t ask why it’s necessary.
Exit Emacs?
Not exactly. This tool is more of a compliment to emacs’s agda-mode, which provides additional useful tools for writing Agda. If you want your VIM key bindings inside emacs, have a look at evil.