PrefacetotheFirstEdition
Types are the central organizing principle of the theory of programming languages.
Language features are manifestations of type structure. The syntax of a language is
governedbytheconstructsthat define its types, anditssemanticsis determined by the
interactionsamongthoseconstructs.Thesoundnessofalanguagedesign—theabsenceof
ill-definedprograms—followsnaturally.
Thepurposeofthisbookistoexplainthisremark.Avarietyofprogramminglanguage
features are analyzed in the unifying framework of type theory. A language feature is
defined by its statics, the rules governing the use of the feature in a program, and its
dynamics, the rules defining how programs using this feature are to be executed. The
conceptofsafetyemergesasthecoherenceofthestaticsandthedynamicsofalanguage.
In this way, we establish a foundation for the study of programming languages. But
whytheseparticularmethods?Themainjustificationisprovidedbythebookitself.The
methods we use are both precise and intuitive, providing a uniform framework for
explainingprogramming languageconcepts.Importantly,thesemethods scale to a wide
rangeofprogramminglanguageconcepts,supportingrigorousanalysisoftheirproperties.
Althoughitwouldrequireanotherbookinitselftojustifythisassertion,thesemethodsare
alsopracticalinthattheyaredirectlyapplicabletoimplementationanduniquelyeffective
asabasisformechanizedreasoning.Nootherframeworkoffersasmuch.
Beingaconsolidationanddistillationofdecadesofresearch,thisbookdoesnotprovide
anexhaustiveaccountofthehistoryoftheideasthatinformit.Sufficeittosaythatmuch
ofthedevelopmentisnotoriginalbutratherislargelyareformulationofwhathasgone
before.Thenotesattheendofeachchaptersignpostthemajordevelopmentsbutarenot
intended as a complete guide to the literature. For further information and alternative
perspectives,thereader isreferredto suchexcellentsources asConstable(1986, 1998),
Girard (1989), Martin-Löf (1984), Mitchell (1996), Pierce (2002, 2004), and
Reynolds(1998).
Thebookisdividedintopartsthatare,inthemain,independentofoneanother.PartsI
and II, however, provide the foundation for the rest of the book and must therefore be
consideredpriortoallotherparts.Onfirstreading,itmaybebesttoskimPartI,andbegin
in earnest with Part II, returning to Part I for clarification of the logical framework in
whichtherestofthebookiscast.
Numerouspeoplehavereadandcommentedonearliereditionsofthisbookandhave
suggested corrections and improvements to it. I am particularly grateful to Umut Acar,
JesperLouisAndersen,CarloAngiuli,AndrewAppel,StephanieBalzer,EricBergstrom,
GuyE.Blelloch,IlianoCervesato,LinChase,KarlCrary,RowanDavies,DerekDreyer,
DanLicata,Zhong Shao, Rob Simmons,andToddWilson for their extensiveeffortsin
readingandcriticizingthebook.Ialsothankthefollowingpeoplefortheirsuggestions:
Joseph Abrahamson, Arbob Ahmad, Zena Ariola, Eric Bergstrome, William Byrd,
AlejandroCabrera,Luis Caires,LucaCardelli, Manuel Chakravarty, Richard C.Cobbe,
JamesCooper,YiDai,DanielDantas,AnupamDatta,JakeDonham,BillDuff,Matthias
Felleisen, Kathleen Fisher, Dan Friedman, Peter Gammie, Maia Ginsburg, Byron