Principles Of Programming Languages Version 1.0

3y ago
47 Views
3 Downloads
819.61 KB
164 Pages
Last View : 3d ago
Last Download : 3m ago
Upload by : Oscar Steel
Transcription

Principles of Programming LanguagesVersion 1.0.3Mike GrantZachary PalmerScott Smithhttp://pl.cs.jhu.edu/pl/book

iCopyright 2002-2020 Scott F. Smith.This work is licensed under the Creative Commons Attribution-Share Alike 3.0 UnitedStates License. To view a copy of this license, /us/ or send a letter to CreativeCommons, 171 Second Street, Suite 300, San Francisco, California, 94105, USA.This document was last compiled on March 16, 2021.

Contents1 Introduction12 Operational Semantics2.1 A First Look at Operational Semantics . . . . . . . .2.2 BNF grammars and Syntax . . . . . . . . . . . . . .2.2.1 Operational Semantics for Logic Expressions2.2.2 Abstract Syntax . . . . . . . . . . . . . . . .2.2.3 Operational Semantics and Interpreters . . .2.3 The F[ Programming Language . . . . . . . . . . . .2.3.1 F[ Syntax . . . . . . . . . . . . . . . . . . . .2.3.2 Variable Substitution . . . . . . . . . . . . .2.3.3 Operational Semantics for F[ . . . . . . . . .2.3.4 The Expressiveness of F[ . . . . . . . . . . .2.3.5 Russell’s Paradox and Encoding Recursion .2.3.6 Call-By-Name Parameter Passing . . . . . . .2.3.7 F[ Abstract Syntax . . . . . . . . . . . . . .2.4 Operational Equivalence . . . . . . . . . . . . . . . .2.4.1 Defining Operational Equivalence . . . . . . .2.4.2 Properties of Operational Equivalence . . . .2.4.3 Examples of Operational Equivalence . . . .2.4.4 The λ-Calculus . . . . . . . . . . . . . . . . .3 Tuples, Records, and Variants3.1 Tuples . . . . . . . . . . . . .3.2 Records . . . . . . . . . . . .3.2.1 Record Polymorphism3.2.2 The F[R Language . .3.3 Variants . . . . . . . . . . . .3.3.1 Variant Polymorphism3.3.2 The F[V Language .4 Side Effects: State and Exceptions4.1 State . . . . . . . . . . . . . . . . . .4.1.1 The F[S Language . . . . . .4.1.2 Cyclical Stores . . . . . . . .4.1.3 The “Normal” Kind of 52535454.5757586365

51201237 Concurrency7.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7.1.1 The Java Concurrency Model . . . . . . . . . . . . . . . . . . . . .7.2 The Actor Model and AF[V . . . . . . . . . . . . . . . . . . . . . . . . .1261261271284.24.34.44.1.4 Automatic Garbage Collection . .Environment-Based Interpreters . . . . . .The F[SR Language . . . . . . . . . . . .4.3.1 Multiplication and Factorial . . . .4.3.2 Merge Sort . . . . . . . . . . . . .Exceptions and Other Control Operations4.4.1 Interpreting Return . . . . . . . .4.4.2 The F[X Language . . . . . . . . .4.4.3 Implementing the F[X Interpreter5 Object-Oriented Language Features5.1 Encoding Objects in F[SR . . . . .5.1.1 Simple Objects . . . . . . . .5.1.2 Object Polymorphism . . . .5.1.3 Information Hiding . . . . . .5.1.4 Classes . . . . . . . . . . . .5.1.5 Inheritance . . . . . . . . . .5.1.6 Dynamic Dispatch . . . . . .5.1.7 Static Fields and Methods . .5.2 The F[OB Language . . . . . . . . .5.2.1 Concrete Syntax . . . . . . .5.2.2 A Direct Interpreter . . . . .5.2.3 Translating F[OB to F[SR .6 Type Systems6.1 An Overview of Types . . . . . . . . . . . . . . . . . . . . . . . . . .6.2 TF[: A Typed F[ Variation . . . . . . . . . . . . . . . . . . . . . . .6.2.1 Design Issues . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2.2 The TF[ Language . . . . . . . . . . . . . . . . . . . . . . . .6.3 Type Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.4 Types for an Advanced Language: TF[SRX . . . . . . . . . . . . .6.5 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.5.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.5.2 The STF[R Type System: TF[ with Records and Subtyping6.5.3 Implementing an STF[R Type Checker . . . . . . . . . . . .6.5.4 Subtyping in Other Languages . . . . . . . . . . . . . . . . .6.6 Type Inference and Polymorphism . . . . . . . . . . . . . . . . . . .6.6.1 Type Inference and Polymorphism . . . . . . . . . . . . . . .6.6.2 An Equational Type System: EF[ . . . . . . . . . . . . . . .6.6.3 PEF[: EF[ with Let Polymorphism . . . . . . . . . . . . . .6.7 Constrained Type Inference . . . . . . . . . . . . . . . . . . . . . . .

CONTENTS7.2.17.2.27.2.37.2.47.2.57.2.6ivSyntax of AF[V . . . . . . . . .An Example . . . . . . . . . . .Operational Semantics of ActorsThe Local Rules . . . . . . . . .The Global Rule . . . . . . . . .The Atomicity of Actors . . . . .8 Compilation by Program Transformation8.1 Closure Conversion . . . . . . . . . . . . .8.1.1 The Official Closure Conversion . .8.2 A-Translation . . . . . . . . . . . . . . . .8.2.1 The Official A-Translation . . . . .8.3 Function Hoisting . . . . . . . . . . . . . .8.4 Translation to C . . . . . . . . . . . . . .8.4.1 Memory Layout . . . . . . . . . . .8.4.2 The toC translation . . . . . . . .8.4.3 Compilation to Assembly code . .8.5 Summary . . . . . . . . . . . . . . . . . .8.6 Optimization . . . . . . . . . . . . . . . .8.7 Garbage Collection . . . . . . . . . . . . 153153154Bibliography155Index157

Chapter 1IntroductionIn this book, our goal is to study the fundamental concepts in programming languages,as opposed to learning a range of specific languages. Languages are easy to learn, itis the concepts behind them that are difficult. The basic features we study in turn include higher-order functions, data structures in the form of records and variants, mutablestate, exceptions, objects and classes, and types. We also study language implementations, both through language interpreters and language compilers. Throughout the bookwe write small interpreters for toy languages, and in Chapter 8 we write a principledcompiler. We define type checkers to define which programs are well-typed and whichare not. We also take a more precise, mathematical view of interpreters and type checkers, via the concepts of operational semantics and type systems. These last two conceptshave historically evolved from the logician’s view of programming.The material has evolved from lecture notes used in a programming languages coursefor juniors, seniors, and graduate students at Johns Hopkins University [21].While the book uses formal mathematical techniques such as operational semanticsand type systems, it does not emphasize proofs of properties of these systems. We willnonetheless sketch the intuitions of some proofs.The OCaml LanguageThe OCaml programming language [15] is used throughout the book, and assignmentsrelated to the book should be written in OCaml. OCaml is a modern dialect of MLwhich has the advantages of being reliable, fast, free, and available on just about anyplatform through http://ocaml.org.The FbDKComplementing the book is the F[ Development Kit, FbDK. It is a set of OCaml utilitiesand interpreters for designing and experimenting with the toy F[ and F[SR languagesdefined in the book. It is available from the book homepage at http://pl.cs.jhu.edu/pl/book.1

CHAPTER 1. INTRODUCTION2Background NeededThe book assumes familiarity with the basics of OCaml, including the module system(but not the objects, the “O” in OCaml). Beyond that there is no absolute prerequisite,but knowledge of C, C , and Java is helpful because many of the topics in this book areimplemented in these languages. The compiler presented in chapter 8 produces C codeas its target, and so a basic knowledge of C will be needed to implement the compiler.More nebulously, a certain “mathematical maturity” greatly helps in understanding theconcepts, some of which are deep. for this reason, previous study of mathematics, formal logic and other foundational topics in Computer Science such as automata theory,grammars, and algorithms will be a great help.Now, make sure your seat belts are buckled, sit back, relax, and enjoy the ride. . .

Chapter 2Operational Semantics2.1A First Look at Operational SemanticsThe syntax of a programming language is the set of rules governing the formation ofexpressions in the language. The semantics of a programming language is the meaningof those expressions.There are several forms of language semantics. Axiomatic semantics is a set of axiomatic truths in a programming language. Denotational semantics involves modelingprograms as static mathematical objects, namely as set-theoretic functions with specificproperties. We, however, will focus on a form of semantics called operational semantics.An operational semantics is a mathematical model of programming language execution. It is, in essence, an interpreter defined mathematically. However, an operationalsemantics is more precise than an interpreter because it is defined mathematically, andnot based on the meaning of the programming language in which the interpreter is written. This might sound sound like a pedantic distinction, but interpreters interpret e.g. alanguage’s if statements with the if statement of the language the interpreter is writtenin. This is in some sense a circular definition of if. Formally, we can define operationalsemantics as follows.Definition 2.1 (Operational Semantics). An operational semantics for a programming language is a mathematical definition of its computation relation, e v, where eis a program in the language.e v is mathematically a 2-place relation between expressions of the language, e, andvalues of the language, v. Integers and booleans are values. Functions are also valuesbecause they don’t compute to anything. e and v are metavariables, meaning theydenote an arbitrary expression or value, and should not be confused with the (regular)variables that are part of programs.An operational semantics for a programming language is a means for understanding inprecise detail the meaning of an expression in the language. It is the formal specificationof the language that is used when writing compilers and interpreters, and it allows us torigorously verify things about the language.3

CHAPTER 2. OPERATIONAL SEMANTICS2.24BNF grammars and SyntaxBefore getting into meaning we need to take a step back and first precisely define languagesyntax. This is done with formal grammars. Backus-Naur Form (BNF) is a standardgrammar formalism for defining language syntax. You could well be familiar with BNFsince it is often taught in introductory courses, but if not we provide a brief overview.All BNF grammars comprise terminals, nonterminals (aka syntactic categories), andproduction rules. Terminals are traditionally identified using lower-case letters; nonterminals are identified using upper-case letters. Production rules describe how nonterminals are defined. The general form of production rules is:hnonterminali :: hform 1i · · · hform niwhere each “form” above describes a particular language form – that is, a string ofterminals and non-terminals. A term in the language is a string of terminals whichmatches the description of one of these rules (traditionally the first).For example, consider the language Sheep. Let {S} be the set of nonterminals, {a, b}be the set of terminals, and the grammar definition be:S :: b SaNote that this is a recursive definition. Examples of terms in Sheep areb, ba, baa, baaa, baaaa, . . .That is, any string starting with the character b and followed by zero or more a charactersis a term in Sheep. The following are examples that are not terms in SHEEP: a: Terms in Sheep must start with a b. bbaaa: Sheep does not allow multiple b characters in a term. baah: h is not a terminal in Sheep. Saaa: S is a non-terminal in Sheep. Terms may not contain non-terminals.Another way of expressing a grammar is by the use of a syntax diagram. Syntaxdiagrams describe the grammar visually rather than in a textual form. For example, thefollowing is a syntax diagram for the language Sheep:SbSaThe above syntax diagram describes all terms of the Sheep language. To generatea form of S, one starts at the left side of the diagram and moves until one reaches theright. The rectangular nodes represent non-terminals while the rounded nodes representterminals. Upon reaching a non-terminal node, one must construct a term using thatnon-terminal to proceed.

CHAPTER 2. OPERATIONAL SEMANTICS5As another example, consider the language Frog. Let {F, G} be the set of nonterminals, {r, i, b, t} be the set of terminals, and the grammar definition be::: rF iGFG :: bG bF tNote that this is a mutually recursive definition. Note also that each production ruledefines a syntactic category. Terms in FROG include:ibit, ribbit, ribibibbbit . . .The following terms are not terms in Frog: rbt: When a term in Frog starts with r, the following non-terminal is F . Thenon-terminal F may only be exapnded into rF or iG, neither of which start withb. Thus, no string starting with rb is a term in Frog. rabbit: a is not a terminal in Frog. rrrrrrF : F is a non-terminal in Frog; terms may not contain non-terminals. bit: The only forms starting with b appear as part of the definition of G. As F isthe first non-terminal defined, terms in Frog must match F (which does not haveany forms starting with b).The following syntax diagram describes Frog:FGrFiGbGbFt2.2.1Operational Semantics for Logic ExpressionsIn order to get a feel for what an operational semantics is and how it is defined, we willnow examine the operational semantics for a very simple language: propositional booleanlogic with no variables. The syntax of this language is as follows. An expression e isrecursively defined to consist of the values True and False, and the expressions e And e,e Or e, e Implies e, and Not e.1 This syntax is known as the concrete syntax,1Throughout the book we use syntax very similar to OCaml in our toy languages, but with theconvention of capitalizing keywords to avoid potential conflicts with the OCaml language.

CHAPTER 2. OPERATIONAL SEMANTICS6because it is the syntax that describes the textual representation of an expression in thelanguage. We can express it in a BNF grammar as follows:e :: v Not e e And e e Or e e Implies e (e) expressionsv :: True FalsevaluesThe following is an equivalent syntax diagram:veNoteeAndeeOreeImpliesevTrueFalseNote that the syntax above breaks tradition somewhat by using lower-case lettersfor non-terminals. Terminals are printed in fixed-width font. The rationale for this isconsistency with the metavariables we will be using in operational semantics below andwill become clear shortly.We can now discuss the operational semantics of the boolean language. Operationalsemantics are written in the form of logic rules, which are written as a series of preconditions above a horizontal line and the conclusion below it. For example, the logicrule(Apple Rule)Red(x) Shiny(x)Apple(x)indicates that if a thing is red and shiny, then that thing is an apple. This is, of course, nottrue; many red, shiny things exist which are not apples. Nonetheless, it is a valid logicalstatement. In our work, we will be defining logical rules pertaining to a programminglanguage; as a result, we have control over the space in which the rules are constructed.We need not necessarily concern ourselves with intuitive sense so long as the programminglanguage has a mathematical foundation.Operational semantics rules discuss how pieces of code evaluate. For example, let usconsider the And rule. We may define the following rule for And:(And Rule (Try 1))True And False False

CHAPTER 2. OPERATIONAL SEMANTICS7This rule indicates that the boolean language code True And False evaluates toFalse. The absence of any preconditions above the line means that no conditions mustbe met; this operational semantics rule is always true. Rules with nothing above the lineare termed axioms since they have no preconditions and so the conclusion always holds.As a rule, though, it isn’t very useful. It only evaluates a very specific program.This rule does not describe how to evaluate the program True And True, for instance.In order to generalize our rules to describe a full language and not just specific termswithin the language, we must make use of metavariables.To maintain consistency with the above BNF grammar, we use metavariables startingwith e to represent expressions and metavariables starting with v to represent values.We are now ready to make an attempt at describing every aspect of the And operatorusing the following new rule:(And Rule (Try 2))v1 And v2 the logical and of v1 and v2Using this rule, we can successfully evaluate True And False, True and True, andso on. Note that we have used a textual description to indicate the value of the expressionv1 And v2 ; this is permitted, although most rules in more complex languages will notuse such descriptions.We very quickly encounter limitations in our approach, however. Consider the program True And (False And True). If we tried to apply the above rule to that program,we would have v1 True and v2 (False And True). These two values cannot be applied to logical and as (False and True) is not a boolean value; it is an expression.Our boolean language rule does not allow for cases in which the operands to And areexpressions. We therefore make another attempt at the rule:(And Rule (Try 3))e1 v1 e2 v2e1 And e2 the logical and of v1 and v2This rule is almost precisely what we want; in fact, the rule itself is complete. Intuitively, this rule says that e1 And e2 evaluates to the logical and of the values representedby e1 and e2 . But consider again the program True And False, which we expect toevaluate to False. We can see that e1 True and that e2 False, but our evaluationrelation does not relate v1 or v2 to any value. This is because, strictly speaking, we donot know that True True.Of course, we would like that to be the case and, since we are in the process ofdefining the language, we can make it so. We simply need to declare it in an operationalsemantics rule.(Value Rule)v v

CHAPTER 2. OPERATIONAL SEMANTICS8The value rule above is an axiom declaring that any value always evaluates to itself.This satisfies our requirement and allows us to make use of the And rule. Using thisformal logic approach, we can now prove that True And (False And True) Falseas follows:False False True TrueTrue TrueFalse And True FalseTrue And (False And True) FalseOne may read the above proof tree as an explanation as to why True And (FalseAnd True) evaluates to False. We can choose to read that proof as follows: “True And(False And True) evaluates to False by the And rule because we know True evaluatesto True, that False And True evaluates to False

iomatic truths in a programming language. Denotational semantics involves modeling programs as static mathematical objects, namely as set-theoretic functions with speci c properties. We, however, will focus on a form of semantics called operational semantics. An operational semantics is a mathematical model of programming language execu-tion.

Related Documents:

-graphical programming languages PLC ladder diagram Classification according to programming language paradigm -procedural programming languages C, Ada83 -functional programming languages LISP -logical programming languages PROLOG -object-oriented programming languages C , Smalltalk, Ada95 Classification according to language level

1 Languages at Harvard 2014 – 2015 Why Study a Foreign Language? 2 Planning Your Language Study 5 Languages Offered 2014-2015 (by Department) 6 African Languages 7 Celtic Languages 9 Classical Languages 10 East Asian Languages 11 English 17 Germanic Languages 17 Linguistics 20 Near Eastern Languages 21 Romance La

the bit patterns. So, these machine languages were the rst programming languages, and went hand-in-hand with general-purpose computers. So, programming languages are a fundamental aspect of general-purpose computing, in contrast with e.g., networks, operating systems, and databases. 1.1 The Pre-History of Programming Languages

Principles of Programming Languages Lecture Notes for CSC324 (Version 2.1) Department of Computer Science University of Toronto. principles of programming languages 3 Many thanks to Alexander Biggs, Peter Chen, Rohan Das, Ozan Erdem, Itai David Hass, Hengwei Guo, Kasra Kyanzadeh,

The study of programming languages is valuable for a number of reasons: Increase our capacity to use different constructs Enable us to choose languages more intelligently Makes learning new languages easier Most important criteria for evaluating programming languages include: Readability, writability, reliability, cost

targeted at a particular type of programming practice. Domain-specific languages are programming languages designed for writing programs for a particular kind of work or practice. End-user programming may or may not involve such languages, since what de-fines end-user programming is the intent, not the choice of languages or tools. 2.3.

Applications of traditional scripting languages are: 1. system administration, 2. experimental programming, 3. controlling applications. Application areas : Four main usage areas for scripting languages: 1. Command scripting languages 2.Application scripting languages 3.Markup language 4. Universal scripting languages 1.

Arduino Programming Part 6: EAS 199B Programming Paradigms To think about styles of programming, we can organize programming languages into paradigms Note that many modern program languages have features of more than one paradigm 26 Paradigm Representative Languages Procedural or Sequential Fortran, C, Basic Object-oriented C , smalltalk