Programming Languages: Theory and Practice

1 Programming Languages: Theory and Practice (WORKINGDRAFT OFSEPTEMBER19, 2005.)Robert HarperCarnegie Mellon UniversitySpring Semester, 2005 Copyrightc 2005. All Rights is a collection of lecture notes for Computer Science 15 312 Program-ming Languages. This course has been taught by the author in the Spring of1999 and 2000 at Carnegie Mellon University, and by Andrew Appel in theFall of 1999, 2000, and 2001 at Princeton University. I am grateful to An-drew for his advice and suggestions, and to our students at both CarnegieMellon and Princeton whose enthusiasm (and patience!) was instrumentalin helping to create the course and this follows is a working draft of a planned book that seeks to strikea careful balance between developing the theoretical foundations of pro-gramming languages and explaining the pragmatic issues involved in theirdesign and implementation.

2 Many considerations come into play in the de-sign of a Programming language . I seek here to demonstrate the central roleof type Theory and operational semantics in helping to define a languageand to understand its and suggestions are most welcome. Enjoy!ivWORKINGDRAFTSEPTEMBER19, 2005 ContentsPrefaceiiiI Preliminaries11 Inductive Relations and Judgements .. Rules and Derivations .. Examples of Inductive Definitions .. Rule Induction .. Iterated and Simultaneous Inductive Definitions .. Examples of Rule Induction .. Admissible and Derivable Rules .. Defining Functions by Rules.

3 Foundations .. 112 Transition Transition Systems .. Exercises .. 14II Defining a Language153 Concrete Strings .. Context-Free Grammars .. Ambiguity .. Exercises .. 22vviCONTENTS4 Abstract Syntax Abstract Syntax Trees .. Structural Induction .. Parsing .. Exercises .. 275 Abstract Binding Names .. Abstract Syntax With Names .. Abstract Binding Trees .. Renaming .. Structural Induction .. 346 Static Static Semantics of Arithmetic Expressions .. Exercises .. 387 Dynamic Structured Operational Semantics .. Evaluation Semantics.

4 Relating Transition and Evaluation Semantics .. Exercises .. 448 Relating Static and Dynamic Preservation for Arithmetic Expressions .. Progress for Arithmetic Expressions .. Exercises .. 46 III A Functional Language479 A Minimal Functional Syntax .. Concrete Syntax .. Abstract Syntax .. Static Semantics .. Properties of Typing .. Dynamic Semantics .. Properties of the Dynamic Semantics .. Exercises .. 57 WORKINGDRAFTSEPTEMBER19, 2005 CONTENTSvii10 Type Defining Type Safety .. Type Safety .. Run-Time Errors and Safety .. 63IV Control and Data Flow6711 Abstract Control Flow.

5 Environments .. 7712 Informal Overview of Continuations .. Semantics of Continuations .. Coroutines .. Exercises .. 9513 Exercises .. 102V Imperative Functional Programming10514 Mutable References .. 10715 A Monadic language .. Reifying Effects .. Exercises .. 117VI Cost Semantics and Parallelism11916 Cost Evaluation Semantics .. Relating Evaluation Semantics to Transition Semantics .. Cost Semantics .. Relating Cost Semantics to Transition Semantics .. Exercises .. 125 SEPTEMBER19, 2005 WORKINGDRAFT viiiCONTENTS17 Implicit Tuple Parallelism .. Work and Depth .. Vector Parallelism.

6 13218 A Parallel Abstract A Simple Parallel language .. A Parallel Abstract Machine .. Cost Semantics, Revisited .. Provable Implementations (Summary) .. 142 VII Data Structures and Abstraction14519 Aggregate Data Products .. Sums .. Recursive Types .. 15020 A Polymorphic language .. ML-style Type Inference .. Parametricity .. Informal Discussion .. Relational Parametricity .. 16521 Data Existential Types .. Abstract Syntax .. Correspondence With ML .. Static Semantics .. Dynamic Semantics .. Safety .. Representation Independence .. 176 VIII Lazy Evaluation18122 Lazy Lazy Types.

7 Lazy Lists in an Eager language .. 187 WORKINGDRAFTSEPTEMBER19, Delayed Evaluation and Lazy Data Structures .. 19323 Lazy Call-by-Name and Call-by-Need .. Strict Types in a Lazy language .. 201IX Dynamic Typing20324 Dynamic Dynamic Typing .. Implementing Dynamic Typing .. Dynamic Typing as Static Typing .. 21025 Featherweight Abstract Syntax .. Static Semantics .. Dynamic Semantics .. Type Safety .. Acknowledgement .. 221X Subtyping and Inheritance22326 Adding Subtyping .. Varieties of Subtyping .. Arithmetic Subtyping .. Function Subtyping .. Product and Record Subtyping.

8 Reference Subtyping .. Type Checking With Subtyping .. Implementation of Subtyping .. Coercions .. 23427 Inheritance and Subtyping in Inheritance Mechanisms in Java .. Classes and Instances .. Subclasses .. Abstract Classes and Interfaces .. Subtyping in Java .. 244 SEPTEMBER19, Subtyping .. Subsumption .. Dynamic Dispatch .. Casting .. Methodology .. 249XI Concurrency25128 Concurrent ML253 XII Storage Management25529 Storage TheAMachine .. Garbage Collection .. 261 WORKINGDRAFTSEPTEMBER19, 2005 Part IPreliminaries1 Chapter 1 Inductive DefinitionsInductive definitions are an indispensable tool in the study of program-ming languages.

9 In this chapter we will develop the basic framework ofinductive definitions, and give some examples of their Relations and JudgementsWe start with the notion of ann-place, orn-ary,relation,R, amongn 1objects of interest. (A one-place relation is sometimes called apredicate, orproperty, orclass.) A relation is also called ajudgement form, and the asser-tion that objectsx1, .. ,xnstand in the relationR, writtenR x1, .. ,xnorx1, .. ,xnR, is called aninstanceof that judgement form, or just ajudgementfor judgement forms arise in the study of Programming are a few examples, with their intended meanings:nnatnis a natural numberttreetis a binary treepproppexpresses a propositionptruethe propositionpis true typexis a typee: eis an expression of type The descriptions in the chart above are only meant to be suggestive, andnot as precise definitions.

10 One method for defining judgement forms suchas these is by an inductive definition in the form of a collection of Rules and Rules and DerivationsAninductive definitionof ann-ary relationRconsists of a collection ofinfer-ence rulesof the form~x1R ~xkR~x ~xand each~x1.. ,~xkaren-tuples of objects, andRis the relation beingdefined. The judgements above the horizontal line are called thepremisesof the rule, and the judgement below is called theconclusionof the rule. Ifa rule has no premises ( ,n=0), the rule is called anaxiom; otherwise itis aproper relationPisclosedunder a rule~x1R ~xkR~x Riff~x Pwhenever~x1P, .. ,~xkP.