From ea10982d1bd7560c652e62516535b0b4ebe47cf6 Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Tue, 1 Dec 2009 12:43:07 +0100
Subject: [PATCH] Document the use of type annotations on variable references.

---
 Chapters/Prototype.tex | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/Chapters/Prototype.tex b/Chapters/Prototype.tex
index 78f5ecf..ac4cc93 100644
--- a/Chapters/Prototype.tex
+++ b/Chapters/Prototype.tex
@@ -271,23 +271,23 @@
     \startdesc{Variable reference}
       \defref{variable reference}
       \startlambda
-      x
+      x :: T
       \stoplambda
       This is a reference to a binder. It's written down as the
-      name of the binder that is being referred to, which should of course be
-      bound in a containing scope (including top level scope, so a reference
-      to a top level function is also a variable reference). Additionally,
-      constructors from algebraic datatypes also become variable references.
+      name of the binder that is being referred to along with its type. The
+      binder name should of course be bound in a containing scope (including
+      top level scope, so a reference to a top level function is also a
+      variable reference). Additionally, constructors from algebraic datatypes
+      also become variable references.
 
       The value of this expression is the value bound to the given binder.
 
-      Each binder also carries around its type, but this is usually not shown
-      in the Core expressions. Occasionally, the type of an entire expression
-      or function is shown for clarity, but this is only informational. In
-      practice, the type of an expression is easily determined from the
-      structure of the expression and the types of the binders and occasional
-      cast expressions. This minimize the amount of bookkeeping needed to keep
-      the typing consistent.
+      Each binder also carries around its type (explicitly shown above), but
+      this is usually not shown in the Core expressions. Only when the type is
+      relevant (when a new binder is introduced, for example) will it be
+      shown. In other cases, the binder is either not relevant, or easily
+      derived from the context of the expression. \todo{Ref sidenote on type
+      annotations}
     \stopdesc
 
     \startdesc{Literal}
-- 
2.30.2