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=fc7bfd27731c6f8c7bcf3237bd6415586ab08819;hb=fd2cb06c9e18732a6fbbf20da0b2f92dc981a5db;hpb=c04c0731a576ea9e9fcacaf6981e556546ae312d

diff --git a/topics/week5_simply_typed.mdwn b/topics/week5_simply_typed.mdwn
index fc7bfd27..68dbcf51 100644
--- a/topics/week5_simply_typed.mdwn
+++ b/topics/week5_simply_typed.mdwn
@@ -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.
+