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=7869f6b4aa660c07913dddd1def3fc69256aa69b;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 `Λ_T`

,
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^{t}_{1},
+ x^{t}_{2}, x^{t}_{3}, ...
* If a term `M` has type σ -> τ, and a term `N` has type
σ, then the application `(M N)` has type τ.
@@ -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.
+