Type Theory, Agda and Some Good Books Thereon
In my quest to understand type theory, I came across links to two very good books. The first, Programming Language Foundations in Agda, by Philip Wadler, is available online. The second, Verified Functional Programming in Agda, by Aaron Stump, is avaialble from Amazon for $79.95 paperback, $51.19 kindle. Ouf! Maybe less expensive elsewhere.
Some progress
For the last few days I’ve been working on both
Wadler’s notes (PLFA) and Stump’s book (VFPA), going through
all the examples with Agda (in Emacs). If you
are an Agda && type-theory novice, as am I, I’d
recommend working through the first three
chapters of VFPA before starting PLFA. VFPA
has very detailed explanations of the proofs in Agda,
as well as practical advice on using Agda. I found
the explanation of rewrite in VFPA especially
helpful.
My current modus operandi is to have an Emacs window open on the left, and either PLFA or VFPA open on the right.
Note on Emacs
I’ve found Emacs to work more reliably with Agda than Atom, and would be interested to hear what the experience of others is. See Appendix C below for the Emacs macros in Stump’s book. They go in your .emacs file and are of general use, whether or not you are using VFPA.
You will
need to install the Iowa Agda Library to do the exercises in
Verified Functional Programming. The README for the
IAL GithHUb repo has
installation instructions. After the library is installed,
edit the file $HOME/.agda/libraries so that
it looks like the below.
/usr/local/lib/agda/standard-library.agda-lib
/Users/carlson/dev/agda/ial/.agda-lib
Once this is done, the file $Home/.agda/defaults must consist of the
line standard-library or ial as the case may be. You will have to
create the file corresponding to /Users/carlson/dev/agda/ial/.agda-lib:
name: ial
include: .
A little shell script for switching back and forth between libraries can be found in this gist.
Other Agda resources
There is some interesting material at Introduction to Dependent Types and Agda, 8th Summer School on Formal Techniques. Unfortunately, some of the files are corrupted – a text encoding problem?
Appendix C of VFPA: Emacs macros
The code below defines some convenient Emacs macros for working with Agda. It is taken directly from Verified Functional Programming in Agda (p. 252), by Aaron Stump. Association for Computing Machinery and Morgan & Claypool Publishers. Kindle Edition.
NOTE: I’m on Mac OS and found that for some reason C-c C-, doesn’t work. To work around this, I changed C-, to C-j in the below.
; This defines backslash commands for some extra symbols.
(eval-after-load "quail/latin-ltx"
'(mapc (lambda (pair)
(quail-defrule (car pair) (cadr pair) "TeX"))
'( ("\\bb" "B") ("\\bl" "L") ("\\bs" "S")
("\\bt" "T") ("\\bv" "V") ("\\cv" "g")
("\\comp" "◦") ("\\m" "↦") ("\\om" "ω"))))
; This sets the Ctrl+c Ctrl+k shortcut to
; describe the character under your cursor.
(global-set-key "\C-c\C-k" 'describe-char)
; Change Ctrl+c Ctrl+, and Ctrl+c Ctrl+.
; in Agda mode so they show the normalized rather
; than the "simplified" goals
(defun agda2-normalized-goal-and-context ()
(interactive)
(agda2-goal-and-context '(3)))
(defun agda2-normalized-goal-and-context-and-inferred ()
(interactive)
(agda2-goal-and-context-and-inferred '(3)))
(eval-after-load "agda2-mode"
'(progn
(define-key agda2-mode-map (kbd "C-c C-,")
'agda2-normalized-goal-and-context)
(define-key agda2-mode-map (kbd "C-c C-.")
'agda2-normalized-goal-and-context-and-inferred)))
; NOTE ADDED (JC). The below is optional
; This sets the Agda include path.
; Change YOUR-PATH to the path on your computer
; to the Iowa Agda Library directory. Use forward
; slashes to separate subdirectories.
(custom-set-variables '(agda2-include-dirs (quote ("." "YOUR-PATH/ial"))) )