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, xt1, + xt2, xt3, ... * 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. +