X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek5_simply_typed.mdwn;h=68dbcf516faf10065643d1750b2cc9c989743509;hp=1a0425feef46b5802638cde9bc20e89f57b77490;hb=42ea318d0e066534ffd016c299eb75e7f2efcca7;hpb=340e045ffdf3ebf60771af2d74d0bafe9eb08283

diff --git a/topics/week5_simply_typed.mdwn b/topics/week5_simply_typed.mdwn
index 1a0425fe..68dbcf51 100644
--- a/topics/week5_simply_typed.mdwn
+++ b/topics/week5_simply_typed.mdwn
@@ -99,8 +99,8 @@ and so on.
 Given a set of types `T`, we define the set of typed lambda terms <code>&Lambda;_T</code>,
 which is the smallest set such that
 
-*    each type `t` has an infinite set of distinct variables, {x^t}_1,
-     {x^t}_2, {x^t}_3, ...
+*    each type `t` has an infinite set of distinct variables, x<sup>t</sup><sub>1</sub>,
+     x<sup>t</sup><sub>2</sub>, x<sup>t</sup><sub>3</sub>, ...
 
 *    If a term `M` has type &sigma; -> &tau;, and a term `N` has type
      &sigma;, then the application `(M N)` has type &tau;.
@@ -359,3 +359,37 @@ When we talk about monads, we will consider Montague's treatment of
 intensionality in some detail.  In the meantime, Montague's PTQ is
 responsible for making the simply-typed lambda calculus the baseline
 semantic analysis for linguistics.
+
+
+## Wordsworth on types
+
+Wordsworth wrote the following sonnet about the constraints of the
+sonnet form in 1806, but he could have been writing about
+strictly-typed programming languages.
+
+### Nuns Fret Not at Their Convent's Narrow Room
+
+Nuns fret not at their convent's narrow room
+And hermits are contented with their cells;
+And students with their pensive citadels;
+Maids at the wheel, the weaver at his loom,
+Sit blithe and happy; bees that soar for bloom,
+High as the highest Peak of Furness-fells,
+Will murmur by the hour in foxglove bells:
+In truth the prison, into which we doom
+Ourselves, no prison is: and hence for me,
+In sundry moods, 'twas pastime to be bound
+Within the Sonnet's scanty plot of ground;
+Pleased if some Souls (for such there needs must be)
+Who have felt the weight of too much liberty,
+Should find brief solace there, as I have found.
+
+This sonnet has an octave (the first eight lines, with rhyme scheme
+abbaabba) followed by a sestet (cddccd).  But the words apply to types
+as well as to sonnets.  "The prison into which we doom / Ourselves, no
+prison is": as long as we get to choose the types of our expressions,
+we can accomplish whatever we need to.  Let anyone who wants to code
+in the free 'verse of the untyped lambda calculus---but those of us
+"who have felt the weight of too much liberty" will find solace in a
+strictly typed language.
+