17 More

In this chapter, discussing useful extensions to the basic systems described in the previous three chapters, PLFA makes the decision to largely abandon English prose. Informal descriptions are given by grammars and inference rules; formal descriptions are provided by code that one is expected to read. This is a reasonable decision at this point. We have already seen examples of these features in the Agda language itself, in Part 1. One can always delete sections of the code and attempt to rederive it in order to gain further insight. There are corresponding chapters in both TaPL and SF, each of which uses more English prose than PLFA.

This chapter demonstrates that the elegance of the previous chapter was not a carefully-tuned sweet spot from which all directions lead down. Rather, the extensions discussed have natural and straightforward implementations. The code remains readable, and for that reason, I don’t find a need to say much about it in these notes.

I have assigned the recommended exercises in this chapter, and left the others as optional work. The nature of the exercises is different from earlier ones. For the first time, you are being asked to define formal Agda syntax corresponding to an informal description. You have some latitude in doing this. For example, eliminating a value of the empty type is described in the informal notation as a case statement with no cases (because there are no constructors for the empty type). Previously, case statements had the various cases surrounded with square brackets, with vertical bars separating each case from others. When there are no cases, this looks like: [].

That [] makes no difference to the semantics; it is purely syntactic. You have a choice as to whether to use it in the formal syntax or not. I don’t know how to automate any part of the marking for the assigned exercises; I will do it all by hand.

The alternate formulation of products using a case eliminator requires double substitution. There is a stretch exercise at the end that asks you to show that double substitution is equivalent to two single substitutions. This is rather difficult, and best handled in the context of a general algebraic theory of explicit substitutions. Recently this development has been added as an appendix to PLFA, and you can find it after Part 3 in the table of contents.

You will find, when doing the assigned exercises, that Agda will help locate places where you need to do work. Some will be type errors, and some will be missing cases corresponding to added constructors. In other words: don’t try to do all the work and then see if it typechecks. Do a bit of it, and let the typechecker show you what to do next. If it is complaining about things you don’t want to work on yet, you can comment them out.

There is a cryptic comment in the Values section of the PLFA implementation: "Implicit arguments need to be supplied when they are not fixed by the given arguments." I paid no attention to this, and ran into trouble when I attempted to solve the exercises that I have set you. I found with both new features that Agda complained about not being able to instantiate an implicit argument, highlighting it in yellow. It turned out that that argument could be "anything", and to solve the problem, I had to implicitly quantify over "anything" to give it a name, and then provide that name in braces as the implicit argument Agda was complaining about. Just be warned that this may happen to you.

Another issue with implicits that may arise is trying to find out which specific implicit argument Agda is complaining about. To try to fill in implicit arguments, Agda replaces an implicit argument named A with a metavariable named something like _A1463 (a different number chosen each time to ensure it is a fresh variable), and then tries to find a solution for all the metavariables. If it can’t, it will complain about _A1463, and that is a clue. But we have a tendency to reuse variable names (certainly it is already done in the existing code supplied by PLFA) so that may not be enough to precisely locate the source of the problem. One way to deal with this is to try to use a fresh name in the code and see if the error message changes.