Given a set of types `T`, we define the set of typed lambda terms <code>Λ_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 σ -> τ, and a term `N` has type
σ, then the application `(M N)` has type τ.
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.
+