move link
[lambda.git] / topics / week5_simply_typed.mdwn
index 1a0425f..68dbcf5 100644 (file)
@@ -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.
+