revisions.md

We summarize the major changes to the paper. There are also some minor
typo fixes/re-wordings in various sections.

1. To clarify the applicability of the main results, we added a few
   paragraphs to the discussion section at the end to discuss what
   languages should be models of GTT, how things like reference
   equality fit in and the difference between call-by-name and
   Haskell's notion of laziness. We also put some forward references
   to this discussion in the introduction.
2. We expanded the related work a great deal, adding comparisons to
   Henglein and Degen and Thiemann's work. We also clarified that AGT
   is based on the *type safety proof* of the static language, and not
   just its dynamic semantics.
3. We added an explicit list of contributions to the end of the
   introduction.
4. The list of contributions has forward references giving an overview
   of the paper structure, and we also added an overview to the
   beginning of section 2.
5. To avoid "story of discovery" with the dynamic type models, we
   mention type tags and how this is the usual way of constructing a
   dynamic type for the value type and the novel aspect is the fact
   that the dual is useful for interpreting the dynamic computation
   type.
6. We named the rules, specifically in figures 1-5.
7. We re-ordered some paragraphs in the introduction to introduce eta
   equality before the discussion of eager and transient cast
   semantics.