Notesale: Turn your study into money

Document Preview

Extracts from the notes are below, to see the PDF you'll receive please use the links above

---

See discussions, stats, and author profiles for this publication at: https://www
...
net/publication/228882836

Programming Language Notes
Article · April 2009

CITATIONS

READS

0

75,636

1 author:
Morgan Mcguire
Williams College
63 PUBLICATIONS   1,727 CITATIONS   
SEE PROFILE

All content following this page was uploaded by Morgan Mcguire on 04 June 2014
...


Programming Language Notes
May 12, 2009
Morgan McGuire∗
Williams College

Contents
1

Introduction

1

2

Computability

3

3

Life of a Program

5

4

Interpreters and Compilers

7

5

Syntax

8

6

Semantics

10

7

The λ Calculus

15

8

Macros

19

9

Type Systems

21

10 Memory Management

27

11 Some Popular Languages

31

1

Introduction

A well-written program is a poem
...
For a program, the topic is
an algorithm and the implementation should emphasize the key steps while minimizing the details
...

The choice of programming language most closely corresponds to the choice of poem structure, e
...
, sonnet or
villanelle, not the choice of natural language, e
...
, English or French
...

To author elegant programs, one must master a set of languages and language features
...
Languages are themselves designed
...
A language designer crafts a set of expressive tools suited to the
safety, performance, and expressive demands of a problem domain
...

A programming language is a mathematical calculus, or formal language
...
Like any calculus, a language defines both syntax
and semantics
...
Semantics is the meaning of that notation
...

Church and Turing (and Kleene) showed that the minimal semantics of the λ calculus and Turing machine
are sufficient to emulate the semantics of any more complicated programming language or machine
...

∗ morgan@cs
...
edu, http://graphics
...
williams
...
g
...

In these notes, features are our aperture on programming languages
...
Why would we want to decrease expressiveness?
The primary reason is to make it easier to automatically reject invalid programs, thus aiding the debugging and
verification process
...
You might have previously considered such errors to be bad
...
A
major challenge and theme of programming language design is simultaneously pushing the boundaries of what
is checkable and expressive in a language
...
1

Types

Every language makes some programs easy to express and others difficult
...
A
well-suited language furthermore makes it hard to express programs that are incorrect
...
The cost of a language design is that some correct and potentially useful programs also become
hard to express in the language
...
A type system associates metadata with values and the
variables that can be bound to them
...
When these are violated, e
...
, by assigning a “String” value
to an “int” variable in Java, the program is incorrect
...
Some kinds of errors cannot be detected
efficiently through static analysis, or are statically undecidable
...

We say that a language exhibits type soundness if well-typed programs in that language cannot “go
wrong” [Mil78]
...
Another view of this is that “A language is type-safe if the only operations that can
be performed on data in the language are those sanctioned by the type of the data
...

All languages (even assembly languages) assign a type to a value at least before it is operated on, since
operations are not well-defined without an interpretation of the data
...
One set of languages that does not is assembly languages: values
in memory (including registers) are just bytes and the programmer must keep track of their interpretation
implicitly
...
C++ and Java are statically typed languages
...
Some languages, like ML, are
dynamically typed but the interpreter uses type inference to autonomously assign static types where possible
...
2

Imperative and Functional

The discipline of computer science grew out of mathematics largely due to the work of Church and his students,
particularly Turing
...
It is minimalist
in the sense that it contains the fewest possible number of expressions, yet can encode any decidable function
...
These
were then shown to be equivalent an minimal models of computation, which is today called the Church-Turing
Thesis
...
Turing’s machine
model leads to imperative programming, which operates by mutating (changing) state and proceeds by iteration
...
Church’s mathematical model leads to functional
programming, which operates by invoking functions and proceeds by recursion
...
So-called scripting languages like Python and
Perl encourage blending of the two styles, since they favor terseness in all expressions
...
1

The Incompleteness Theorem

At the beginning of the 20th century, mathematicians widely believed that all true theorems could be reduced
to a small set of axioms
...
Hilbert’s program1 was to actually reduce the different fields of mathematics to a small and consistent
set of axioms, thus putting them all on a solid and universal foundation
...
e
...
This Incompleteness
Theorem was a surprising result and indicated that a consistent set of axioms could not exist
...
This is also known
as the First Incompleteness Theorem; there is a second theorem that addresses the inconsistency of languages
that claim to prove their own consistency
...
Let every statement in the
language be encoded by a natural number, which is the G¨odel Number of that statement
...
(This is roughly equivalent to treating the
text of a program as a giant number containing the concatenation of all of its bits in an ASCII representation
...
”

(2)

evaluated at n = i
...
” Sn (n) creates an inconsistency
...

As a result of the Incompleteness Theorem, we know that there exist functions whose results cannot be
computed
...

For computer science, we define computability as:
A function f is computable if there exists a program P that computes f , i
...
, for any input x, the
computation P(x) halts with output f (x)
...
A constant challenge in programming language development is that it is mathematically impossible to
prove certain properties about arbitrary programs, such as whether a program does not contain an infinite loop
...
2

The Halting Problem

Let the Halting Function H(P, x) be the function that, given a program P and an input x to P, has value “halts”
if P(x) would halt (terminate in finite time) were it to be run, and has value “does not halt” otherwise (i
...
, if
P(x) would run infinitely, if run)
...

1 “program”

as in plan of action, not code
answered Hilbert’s “second problem”: prove that arithmetic is self-consistent
...

2
...
H(P, x) is undecidable
...
Assume program Q(P, x) computes H (somehow)
...

Now, consider the effect of executing D(D)
...
Because D(D)
cannot both halt and run forever, this is a contradiction
...
We made no further assumption beyond H being decidable, therefore H must be
undecidable
...
It is possible to
prove that a specific program with a specific input halts
...
For example, every finite program in a language without recursion or iteration must
halt
...
For example, within
the same structure one can prove that it is undecidable whether a program prints output or reaches a specific
line in execution
...
See
http://www
...
uwaterloo
...

Two straightforward ways to prove that a property is undecidable are:
• Show that the Halting Problem reduces to this property
...

• Rewrite a Halting Problem proof, substituting the property for halting
...


2
...
One choice is to abandon checking certain properties until run
time
...
The enables a language to easily express many kinds of
programs, however, it means that the programmer has little assurance that the program is actually correct
...
Python and Scheme are two languages that defer almost all
checking until run time
...

Another choice is to restrict the expressive power of the language somewhat, so that more properties can
be checked before a program is run
...
k
...
compile-time checking)
...
C++ and
ML are languages that provide significant static checking facilities
...
It performs some checks statically, but in order to make the language more flexible the designers
made many other checks dynamic
...
Java programmers may be pleasantly
surprised to discover that there are many languages (unfortunately none of the popular ones mentioned in this
paragraph) in which most null-pointer checks can be made statically, and therefore appear very infrequently as
run-time errors
...
This is useful for metalanguages, like type systems, and for embedded languages, like

3

LIFE OF A PROGRAM

5

early versions of the 3D graphics DirectX HLSL and OpenGL GLSL languages
...
Of course, programmers often find those restrictions burdensome and most practical
languages eventually evolve features that expand the expressive power to defeat their static checkability
...


3

Life of a Program

A program goes through three major stages: Source, Expressions, and Values
...
This is called the
expression domain of the language
...

Expressions are also called terms
...

An analogy to a person reading a book helps to make clear the three stages
...
The reader scans the page, distinguishing tokens of individual letters and symbols from clumps
of ink
...
e
...
When those expressions are
evaluated, the value (meaning) of the words arises in the readers mind
...
Consider a number written on the page, such as “32”
...
The
set of two digits next to each other is the expression
...
The number value is not something that can be written, because the act of writing it down
converts it back into an expression
...
4

3
...
This is the ASCII (or, increasingly, unicode!) string describing the program,
which is usually in a file stored on disk
...
For example, in Java the period character “
...
g
...
length() versus 3
...
See java
...

Figures 3
...
1 show an example of the source code and resulting token stream for a simple factorial
function implemented in the Scheme programming language
...
For this
example, the tokenizer tags each token as a parenthesis, reserved word, identifier, or numeral
...
A typical data structure for storing the token stream is an array of instances of a token
class
...


3A

language in which programs always halt is called strongly normalizing
...
The actual number that the numeral 32 represents is unique
...
AI, PL, and philosophy meet when we consider whether the human mind is different, or just shuffling
around around representations like a computer
...


3
...
The legal expressions are described by the
expression domain of the language, which is often specified in BNF
...
g
...
The
structure of the parse tree visually resembles the indenting in the source code
...
2 shows a parse tree for
the expressions found in the token stream from figure 3
...


Figure 3: Parse tree for factorial
...
The drawback of this approach is that simply quoting the factorial code in figure 3
...
2
...


3
...
The set of legal values that can exist during execution is called the value domain
...
In general, a value is first-class in a language if all of the following hold:
1
...
The value can be an argument to a function
3
...
The value can be stored in a data structure
Java generics (a polymorphism mechanism) do not support primitive types like int, so in some sense those
primitives are second-class in Java and should be specified in a separate domain from Object and its subclasses,
which are first-class
...
Java methods are not first-class, so that language contains a Method class that describes
a method and acts as a proxy for it
...
g
...


3
...
Using the same
types in the implementation language for source, expressions, and values reduces the amount of packing and
unpacking of values that is needed, and allows procedures in the implementation language to operate directly on
the values in the target language
...
This avoids the
need for an explicit tokenizer and parser
...
This can make the implementation of the language harder to understand (when it grows large), and
limits the ability of the type checker to detect errors in the implementation
...
It would be easy to accidentally pass a piece of
source code to a method that expected an identifier, and the Java compiler could not detect that error at compile
time because the method was only typed to expect a String, not a SchemeIdentifier
...
The result is sometimes called a native binary because it is in the native language of the
computer5
...

There is a wide range of translation within the classification of interpreters
...
At the other end,
some interpreters essentially translate code down to native machine language at runtime so that the program
executes very efficiently
...
C++, C, Pascal, Fortran, Algol, and Ada are typically compiled
...
Java is an interesting case that compiles to machine language for a computer that does not exist
...

Compilers tend to take advantage of the fact that they are run once for a specific instance of a program and
perform much more static analysis
...
Detecting errors before a program actually runs is important because it
reduces the space of possible runtime errors, which in turn increases reliability
...

Interpreters tend to take advantage of the fact that code can be easily modified while it is executing to allow
extensive interaction and debugging of the source program
...
Many interpreted languages were designed with the
knowledge that they would not have extensive static analysis and therefore omit the features that would support
it
...
Combined with the ease of debugging, this makes interpreted languages often feel “friendlier”
to the programmer
...

Compiled programs are favored for distributing proprietary algorithms because it is hard to reverse engineer
a high-level algorithm from machine language
...
This allows them include new architectural optimizations without changing the public interface, for
compatibility
...


5

Syntax

Although we largely focus on semantics, some notable points about syntax:
• A parser converts source code to expressions
• Backus-Naur Form (BNF) formal grammars are a way of describing syntax using recursive patterns
• Infix syntax places an operator between its arguments, e
...
, “1 + 2”
...

• Prefix syntax places the operator before the operands, e
...
, “add(1, 2)”, which conveniently allows
more than one or two operands and unifies operator and function syntax
...

• Postfix places the operator after the operands, which allows nested expressions where the operators take
a fixed number of arguments, without requiring parentheses
...

• Scheme’s “abstract syntax” makes it easy to parse
• Macros allow a programmer to introduce new syntax into a language
• Python has an interesting syntax in which whitespace is significant
...
1

Backus-Naur Form

Backus-Naur Form (BNF) is a formal way of describing context-free grammars for formal languages
...
e
...
BNF was first used to specify the ALGOL programming language
...
Examples include file formats, types, database records, and
string search patterns
...
These are patterns that legal
programs in the specified language must follow
...
In the BNF syntax, the
nonterminal being defined is enclosed in angular brackets, followed by the “::=” operator, followed by an
expression pattern
...
For example,
hdigiti
hdigitsi

::=
::=

‘0’ | ‘1’ | ‘2’ | ‘3’ | ‘4’ | ‘5’ | ‘6’ | ‘7’ | ‘8’ | ‘9’
hdigiti | hdigitihdigitsi

In this document, these are typeset using an unofficial (but common) variation, where terminals are typeset as
x and nonterminals as x
...
With this convention, digits are:
digit

::=

digits

::=

0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
digit | digit digits

It is common to extend BNF with regular expression patterns to avoid the need for helper productions
...
e
...
g
...
digit +

real

::=

integer | rational | decimal

BNF can be applied at both the character level (e
...
, to describe a lexer/tokenizer) and the token level (e
...
,
to describe a parser)
...
An example of a subset of Scheme’s expression domain represented in BNF at the token level is:
variable

::=

id

let

::=

(

lambda

::=

(

exp

::=

let

[ id exp ]

(

lambda

variable  let


∗

) exp )

( id ∗ ) exp )

 lambda
(3)

5
...
We say that an expression is syntactic sugar and adds no expressive
power if it can be reduced to another expression with only local changes
...
Such expressions are also referred
to as being macro-expressive
...

For example, in Java any FOR statement, which has the form:
for ( init ; test ; incr ) body
can be rewritten as a WHILE statement of the form:
init ; while ( test ) { body

incr ; }

FOR therefore does not add expressivity to the language and is syntactic sugar
...
Java exceptions are an example of an expressive form
that cannot be eliminated without completely rewriting programs in the language
...
This is an example
of a general mechanism for ascribing formal semantics to syntax that is described further in the following
section
...
1

Operational Semantics

An operational semantics is a mathematical representation of the semantics of a language
...
Equivalently, it gives a set of progress
rules for progressing from complex expressions to simpler ones, and eventually to values
...
Any rule whose preconditions
are met can be applied
...
If it halts with a value, that is the result of
the computation
...
The nature and location of the error are determined by the
remaining expression and the last rule applied
...
For example, an operation
that requires O(n2 ) rule applications may require only O(n) operations on an actual computer
...
We say that two implementations are
semantically equivalent if they always reduce identical expressions to identical vales, even if they use different
underlying algorithms to implement the semantics
...
The most
general form of a rule is:
x ⇒ y

(5)

“Expressions matching x reduce to y”
where x is a placeholder in this notation, not a variable in the programming language
...
Here, the name of the variable
indicates its domain (often, expression or value), and the subscript is a tag to distinguish multiple variables
in the same statement6 Sometimes rules are written more casually using the subscripts as the variables and
ignoring the domains, when the domain is irrelevant
...
Variables numx and numy are expressions; the hat on the right side indicates that we
mean the value corresponding to that operation
...
e
...
The hat on the 3 to the
right of the arrow indicates that it is a value, i
...
, it represents an actual number and not just the syntax for a
number
...
We will see some cases in which the line
between the expression domain and the value domain is blurry
...

Sometimes we have complicated conditions on a rule that constrain the pattern on the left side of ⇒
...
”

(9)

In gen-

6 This is admittedly a suboptimal notation, since the “name” that carries the meaning for the reader but is buried in the
subscript, while the “type” dominates
...


6

SEMANTICS

11

eral, both a and b are reductions
...
These rules are useful for making progress
when no other rule directly applies
...
The rule for making progress on addition with nested subexpression on the right of the
plus sign is:
exp2 ⇒ num2
exp1 + exp2 ⇒ exp1 + num2

(10)

which reads, “if expression #2 can be reduced to some number (by some other rules), then the entire sum can
be reduced to the sum of expression #1 and that number
...

There are two major interpreter designs: substitution and evaluation interpreters
...
Their value domain is
their literal domain
...
Such a procedure recursively invokes itself, but program execution involves a
single top-level EVAL call
...
Small-step operational semantics rules reduce expressions to expressions (like a substitution
interpreter)
2
...
We use the context of a
simple language that contains only single-argument procedure definition, variable, conditional, application, and
booleans
...
2
6
...
1

(12)

Small-step Example
Rules

Small-step operational semantics rules reduce expressions to expressions
...
g
...
Under small-step semantics the value domain is merely the terminal subset of
the expression domain, plus procedure values
...
It is useful to us later to define a
subdomains in this definition:

true  ( λ ( id ) exp )
ok ::=

val ::=
false  ok
(13)
Those expressions require no progress rules because they are values
...
Only conditional and application need be defined
...
However, recall that Scheme treats any
non-false value as true for the purpose of an IF expression
...
When the test
expression for the conditional is not in the value domain, we need some way of making progress on reducing
the expression
...
This is:
[id  v] body

(17)

The

“Substitute v for id in body”
...
In
an eager language, the v expression must be in the value domain
...

For semantic purposes the distinction between eager and lazy is irrelevant in a language without mutation and
small step semantics are almost always restricted to languages without mutation
...
If we choose lazy evaluation, it is:
E-Applazy : (

(

λ

( id ) expbody )

⇒

exparg )



id  exparg expbody

(18)

plus a progress rule:
E-AppProgress1 :

exp1 ⇒ val1
⇒

( exp1 exp2 )

(19)

( val1 exp2 )

To specify eager evaluation, we simply require the argument to be a value:
E-Appeager : (

(

λ

( id ) expbody )

valarg )

⇒



id  valarg expbody

(20)

and introduce another progress rule (we still require rule E-AppProgress1):
E-AppProgress2eager :

6
...
2

exp2 ⇒ val2
( exp1 exp2 )

⇒

(21)

( exp1 val2 )

A Proof

Because each rule is a mathematical statement, we can prove that a complex expression reduces to a simple
value by listing the rules that apply
...
Operational semantics are used this way, but they are more often used as a rigorous way of
specifying what an interpreter should do
...

We list the statements in the order they are applied
...
To do this, we replace each antecedant with its own proof; that is, we start nesting the conditional
statements until all are satisfied
...
(if ((λ (x) x) true) false true) reduces to false
...
)

⇒

true
(E-IfTrue)

Proof
...
3
6
...
1

Big-step Example
Rules

Under big-step operational semantics, the left side of the progress arrow is always an expression and the right
side of the arrow is always a value
...
The
value and expression domains must be disjoint to make this distinction, so we define the value domain more
carefully here
...
12, the big-step value domain is:
proc

::=

ok

::=

val

::=

hid, exp, E i

proc  tˆ

ok  fˆ

(22)

The angle brackets in the procedure notation hid, exp, E i denote a tuple, in this case, a 3-tuple
...
The specific
tuple we’re defining here is a 1-argument closure value, which has the expected three parts: formal parameter
identifier, body expression, and captured environment
...
The environment is placed on the left side
of the progress arrow and separated by an expression by a comma
...

Forget all of the previous small-step rules
...

The rules for evaluating IF expressions are largely the same as for small step, but we can ignore the progress
rules because they are implicit in the big steps:

¬ expt , E ⇒
E-IfOk:
(

E-IfFalse:



expc , E ⇒ valc

if expt expc expa ) , E ⇒ valc

expt , E ⇒
(

fˆ

fˆ

expa , E ⇒ vala

if expt expc expa ) , E ⇒ vala

(24)

Each reduction, whether a conditional or a simple a ⇒ b, is a mathematical statement
...
Each progress rule is really a step within a proof whose theorem is
7
...


6

SEMANTICS

14

“this program reduces to (whatever the final value is)
...

Thus the E-IfOk rule has as an antecedent “the test expression does not reduce to fˆ ”
...

To express the semantics of APP we need a notation for extending an environment with a new binding
...

Note that the arrow inside the brackets points in the opposite direction as for substitution, following the convention of [Kri07, 223]
...
”
Observe that the body expression is evaluated in the stored environment extended with the new binding,
creating lexical scoping
...
We conclude with the trivial variable rule:
E-Var : id, E [id  val] ⇒ val

(27)

Examining our big-step rules, we see that they map one-to-one to the implementation of an interpreter for
the language
...
Within a rule, each antecedant corresponds to one recursive call to EVAL
...
These correspond to the recursive calls to evaluate the first
subexpression (which should evaluate to a procedure), the second (i
...
, the argument), and then the body
...
The environments specified on the left sides of
the antecedants tell us which environments to pass to EVAL
...

6
...
2

A Proof

This is a proof of the same statement from the small-step example, now proven with the big-step semantics
...

Lemma 1
...


(λ (x) x) , E

(E-Lambda)

⇒

h x , x ,E i

true , E

(E-True)

⇒

tˆ

((λ (x) x) true) , E ⇒ tˆ

x , [ x  tˆ ]E

(E-Var)

⇒

tˆ

(E-App) 

7

THE λ CALCULUS

15

Theorem 3
...


Proof
...
Because ((λ (x) x) true) , E

(Lemma 1)

tˆ , and tˆ 6= fˆ

the negation of the contradiction of Lemma 1, ¬ ((λ (x) x) true) , E ⇒


¬

((λ (x) x) true) , E ⇒

⇒

fˆ



fˆ


, is also true
...


E-IfOk
(if ((λ (x) x) true) false true) , E ⇒ fˆ

7

The λ Calculus

The λ calculus is Church’s [Chu32] minimalist functional model of computation
...
e
...
Variations of λ calculus are heavily used in
programming language research as a vehicle for proofs
...

Philosophically, λ calculus is the8 foundation for our understanding of computation and highlights the power
of abstraction
...
This leads the way to emulating constructs that are
missing in a language at hand, which makes for a better programmer
...
The
Java API designers quickly learned to use anonymous classes to create anonymous closures, enabling the use
of first-class function-like objects in a language that does not support functions
...

On learning a new language, the sophisticated programmer does not learn the specific forms of that language
blindly but instead asks, “which forms create closures, recursive bindings, iteration, etc
...

If any of the desired features are missing, that programmer then emulates them, using techniques learned by
emulating complex features in the minimalist λ calculus
...

Andr´e van Meulebrouck describes an alternative motivation:
“Perhaps you might think of Alonzo Church’s λ -calculus (and numerals) as impractical mental
gymnastics, but consider: many times in the past, seemingly impractical theories became the underpinnings of future technologies (for instance: Boolean Algebra [i
...
, today’s computers that operate
in binary build massive abstractions using only Boole’s theoretical logic!])
...
For instance, imagine computer architectures that run combinators or λ -calculus as their machine instruction sets
...


9 http://www
...
com:16080/articles/mactech/Vol
...
06/ChurchNumerals/

7

THE λ CALCULUS

7
...
exp
exp exp

exp

::=

var | abs | app | ( exp )

The last expression on the right simply states that parentheses may be used for grouping
...
In set notation
this is:
val = proc = var × exp
and in BNF:
val

::=

λ id
...


7
...
expbody val ⇒ [id  val] expbody

(30)

App-Abs: (apply a procedure to a value)

The App-Abs rule relies on the same syntax for the val value and abs expression, which is fine in λ calculus
because we’re using pure textural substitution
...
expbody
val p vala ⇒ [id  vala ] expbody

7
...
Consider the evaluation of the following expression:
λ x
...


(32)

7

THE λ CALCULUS

17

This is an app expression
...
Rule
App-Abs is the only rule that applies here, since both the procedure and the integer cannot be reduced further
...
(x + 3) 7
⇒ [x  7](x + 3)
= (7 + 3)
= 10

(33)
(34)
(35)
(36)

Arithmetic then reduces this to 10
...
( f 3)) (λ x
...
In this case, both the left and right are abs expressions
...
( f 3)) (λ x
...
(1 + x)) ]( f 3))
= λ x
...
4

(38)
(39)
(40)
(41)
(42)
(43)

Partial Function Evaluation

Because procedure application is left associative and requires no function application operator:
f x y = ( f x) y

(44)

we can emulate the functionality of multiple-argument procedures using single argument procedures
...
λ y
...
This is a first-order
procedure
...
λ y
...
(1 + y) 2
⇒ 1+2
=3

(46)
(47)
(48)
(49)

The process of converting a 0th-order function of n arguments into an nth-order function of one argument,
like the one above, is called currying
...

When an nth-order function is applied to k < n arguments, in λ calculus, the result reduces to an (n − k)th
order function
...

This is called partial function evaluation, and is a feature of some languages including Haskell (which is
also named for Haskell Curry, who did not invent it either
...
λ y
...
(5 + y)

(50)
(51)

11 The idea is commonly credited to Sch¨
onfinkel in the 20th century, and was familiar to Frege and Cantor in the
19th [Pie02, 73]

7

THE λ CALCULUS

7
...
A function may have zero or more fixed points
...
x has
infinitely many fixed points
...
x2 be the function that squares its argument; it has fixed points at 0 and
1
...
This is interesting
because it is related to recursion
...
For
example, define factorial (for convenience, we temporarily extend the language with conditionals and integers;
those can be reduced as shown previously):
λ n
...
Alternatively, the
problem is that f is a free variable
...
λ n
...
That’s close to the idea of recursion, but is not fully recursive because we’ve
only implemented one inductive step
...
To let this inductive step run further,
say that f is the function that we’re defining, which means that the inner call requires two arguments: f and
n − 1:
λ f
...
(if (iszero n)
1
(n ∗ ( f f (n − 1))))
Call this entire function g
...
At first
this does not sound useful–if we had the factorial function, we wouldn’t need to write it! However, consider
that what we have defined g such that (g f ) = f
...

For this particular function, we can find the fixed point by binding it and then calling it on itself
...
An expression of the form:
(λ z
...
Wrapping our entire definition with this:
(λ z
...
λ n
...
Convince yourself of this by
running it in Scheme, using the following translation and application to 4:
(
((lambda (z) (z z))
(lambda (f)
(lambda (n)
(if (zero? n)
1
(* n ((f f) (- n 1)))))))
4)

8

MACROS

19

When run, this correctly produces 4! = 4 ∗ 3 ∗ 2 ∗ 1 = 24
...
For the factorial case, we manually constructed a generator function g and its
fixed point
...

Curry discovered the simplest known fixed point combinator for this application
...
k
...
applicative-order Z combinator as expressed here), and is defined as:
Y

=

λ f
...
z z)
(λ x
...
x x y)))

(53)

When applied to a generator function, Y finds its fixed point and produces that recursive function
...
That is, the step where we
rewrote ( f (n − 1)) as ( f f (n − 1)) in our derivation is no longer necessary
...
The use of the DEFINE statement is merely to make the implementation more readable
...

; Creates the fixed point of its argument
(define Y
(lambda (f)
((lambda (z) (z z))
(lambda (x) (f (lambda (y) ((x x) y)))))))
; Given the factorial function, returns the factorial function
(define generator
(lambda (fact)
(lambda (n)
(if (zero? n)
1
(* n (fact (sub1 n)))))))
; The factorial function: prints (lambda
...
For example, a short-circuiting OR expression like the one
in Scheme can be reduced within the parser by the small-step rule:
(

or exp1 exp2 ) ⇒ (

let

(

[ id exp1 ]

)

(

if id id exp2 )

)

(54)

Languages with a macro system feature allow the programmer to add rules such as this to the parser
...
Macros are written in a separate language that is often similar
to the base language, and they generally describe pattern matching behavior
...
For example, a short-circuiting OR cannot be
written using only procedures, IF, and application in a language with eager evaluation of procedure arguments
...
If it did, the macro would accidentally capture that variable and change the meaning of exp1 and
exp2
...
One way to achieve this is to append the level of evaluation
at which an identifier was inserted to the end of its name
...
Not all macro systems are hygienic
...
This does not mean that C macros are useless, just that extreme care must be taken when using
them
...
1

C Macros

The C macro system contains two kinds of statements: #if and #define
...
h>
# i f d e f i n e d ( MSC VER )
//
Windows
#
d e f i n e BREAK : : DebugBreak ( ) ;
# e l i f d e f i n e d ( i 3 8 6 ) && d e f i n e d ( GNUC )
//
g c c on some I n t e l p r o c e s s o r
#
d e f i n e BREAK
asm
volatile
( ” i n t $3 ” ) ;
#else
//
H o p e f u l l y , some o t h e r g c c
#
d e f i n e BREAK : : a b o r t ( )
# endif
# d e f i n e ASSERT ( t e s t e x p r , m e s s a g e ) \
i f ( ! ( t e s t e x p r ) ) {\
p r i n t f ( ”%s \ n A s s e r t i o n \”% s \” f a i l e d i n %s a t l i n e %d
...
They allow the
program to function differently on different machines without the expense of a run-time check
...
The #define statement creates a new macro
...
Here, two macros are defined: BREAK, which halts execution of the program when the code it emits
is invoked, and ASSERT, which conditionally halts execution if a test expression returns false
...

Within the body of the ASSERT definition we see several techniques that are typical of macro usage
...
Unlike procedures in most languages, macros have access to the source code context from which they were invoked
...
The expression #test expr is applying the # operator to
the test expr macro variable
...
Procedures have no way of accessing the expressions that produced their arguments, let
alone the source code for those expressions
...
This is necessary because C macros operate at a pre-parse (in fact, pre-tokenizer!)
level, unlike Scheme macros
...
This is
12 Adapted

from the G3D source code, http://g3d-cpp
...
net
...

C’s macro system is practical, though ugly
...
Templates
were originally introduced as a straightforward polymorphic type mechanism, but have since been exploited by
programmers as a general metaprogramming mechanism that has Turing-equivalent computational power
...
1

Type Systems
Types

A type is any property of a program that we might like to check, regardless of whether it is computable
...
We will restrict ourselves to properties of values, which
is what is commonly meant by programers when they refer to “types”
...
}
uint = {x ∈ num ⊆ val | x ≥ 0}
x ∈ num and x ≥ 0
(define (uint? x) (and (number?
non-negative integers

x) (>= x 0)))

Values have types in all programming languages
...
In some implementations of some languages, types are explicitly stored with the values at runtime
...

In other implementations and languages, types are implicit in the code produced by a compiler
...
For an implementation to avoid storing explicit type values at runtime, it must ascribe static types
to variables, meaning that each variable can be bound to values of a single type that is determined at compile
time
...

Dynamically typed variables can be bound to any type of value
...
One exception is C++, where the reinterpret cast operator allows the program to
reinterpret the bits stored in memory of a value as if they were a value of another type
...
2

Type Checking

Recall that an operational semantics is a set of rules for reducing expressions to values
...
Type judgements are a parallel set of
rules for reducing expressions to types
...
An interpreter would encounter an error condition under operational semantics if it was unable to apply
any rule to reduce an expression further
...
In both cases, that situation
indicates an error in the program being checked
...
However, proving that it reduces to a value is exactly
as hard as executing the program, which means that it is undecidable in general
...
Furthermore, this proof can
be undertaken in the form of a derivation, where the result type and a proof of its correctness are discovered
simultaneously
...

If the types and judgements are carefully defined, type checking is decidable
...
Because they are just rules, the type judgements are a kind of metalanguage
...

A type system comprises the types, the type judgments, and the algorithm for applying the type judgments
to form a proof/discover the result type
...
This is desirable because a well-defined type system generally prohibits programs that would have been
incorrect anyway
...

Furthermore, when we limit the type system in order to make type checking decidable, we lose the ability to
eliminate all incorrect programs
...


9
...
g
...
First, it looks like an operational semantics, so we
might be confused as to what we were seeing
...
e
...
That is, environments store values that we’ve already discovered, but for
type checking we aren’t discovering values
...
Therefore, type judgements use a slightly different notation than
operational semantics
...
Gamma (Γ) is a variable
representing a type environment
...
It is then extended with other types
that are discovered
...
It replaces the comma from
operational semantics notation
...
The T-plus and T-equal judgments are similar to T-and, but with the appropriate types inserted
...
The type of a conditional depends on what the types of the consequent and alternate
expressions are
...
This will limit
the number of invalid programs that we can detect
...
For example, the following is a proof that (if (and true false) 1 4) has type bool:
(T-bool)

(T-bool)

9
...
 lambda  app

proc
val

::=
::=

hid ∗ , exp, evti


...
g
...

The application rule is straightforward
...
× an → r)

∀i, Γ ` expi : ai

(63)

Γ ` ( exp p exp1
...
Some languages, like
ML, tackle that challenge using a process called type inference
...
This is the strategy
taken by languages like Java and C++
...
Now we can express a type judgement for procedure creation:
Γ[id1 ← a1 ,
...
idn : an expb )

(66)

: r : (a1 ×
...
× an → r)”
...

• When typing a function application, we guarantee the argument has the type that the function
demands, and assume the result will have the type the function promises
...

From a theoretical perspective, type annotations are merely a crutch for the type checker and would not
be required in any language
...
The type annotations are a form of documentation
...
If this is true, then
a system that infers procedure types will tend to generate misleading error messages that blame the application
and not the procedure when the argument types do not match due to an error in the procedure
...
5

Inference

The following is an alternative discussion of [Kri07] chapter 30
...
A Hindley-Milner-Damas type system operates by discovering constraints on the types of expressions
and then unifying those constraints
...

The unification process corresponds to running a substitution interpreter in a metalanguage where the values

9

TYPE SYSTEMS

25

are types
...
| -1 | 0 | 1 |
...
| -1 | 0 | 1 |
...
That’s
because we’re going to write a substitution interpreter (i
...
, no mutation!) for the metalanguage, and for a
substitution interpreter the expression/value distinction is less significant
...

A type inference system assigns types to all bound program variables
...
Thus it checks types while discovering
them
...
For example, we might describe
the program:
((λ (x) x) 7)
(70)
as having the following variables:
Let t1

=

[[ ((λ (x) x) 7) ]]

(71)

t2

=

[[ (λ (x) x) ]]

(72)

t3

=

[[ 7 ]]

(73)

t4

=

[[ x ]]

(74)

where [[
...
In solving for these variables, we encounter the
following constraints, from the application, the lambda, and the literal expressions:

9

TYPE SYSTEMS

26

[[ (λ (x) x) ]] = 7 ]] → [[ ((λ (x) x) 7) ]]

(75)

[[ (λ (x) x) ]] = [[ x ]] → [[ x ]]

(76)

num
[[ 7 ]] = \

(77)

Writing these in terms of the type variables, we have:
t2
t2

=
=

t3

=

t3 → t1
t4 → t4
\
num

(78)

This is a set of simultaneous constraints, which we can solve by substitution (much like solving simultaneous
equations in algebra!) A substitution type interpreter solves for their values
...
k
...
a substitution)
...
The type environment initially contains the types of
the built-in procedures
...
While
the stack is not empty, the interpreter pops a constraint of the form X = Y off the top, where X and Y are both
texp, and processes that constraint as follows:
• If X ∈ tvar and X = Y , do nothing
...

• If X ∈ tvar, replace all occurrences of X with Y in the stack and the environment and let extend the
environment with [X 7→ Y ] (N
...
that arrow denotes a binding of a type variable, not a procedure type)
...

• If Y ∈ tvar, replace all occurrences of Y with X in the stack and the environment and let extend the
environment with [Y 7→ X]
...
These are both procedure type expressions, so their argument and return types must match each
other
...

• In any other case, the constraint X = Y is unsatisfiable, indicating an error in the target program
...

Constraint solving is a general problem in computer science
...


9
...
Here are a few:
• Informally, t 0 <: t if you can use an instance of t 0 anywhere that you can use an instance of t
• Considering types as sets of values, the subset notation holds literally: t 0 is a subtype of t if it is also a
subset of t
• By the Liskov substitution principle, if q(x) is a property provable about objects x of type t, then q(y)
should be true for objects y of type t 0 , where t 0 <: t [Lis87]
...

• t 0 <: t if t 0 is a sort of t

10

MEMORY MANAGEMENT

27

The subtype rule is:
T-sub:

9
...
1

Γ ` exp : t 0 t 0 <: t
Γ ` exp : t

(79)

Procedure Subtypes

Because ((λ () exp1 )) ⇒ exp1 , it must be the case that both sides of the reduction arrow have the same type
...
By rule T-sub, we can substitute any expression exp2 for exp1 if exp2 : r0 and r0 <: r
...
This is not surprising
...
Procedure subtype argument types have a contravariant relationship, however: the procedure subtype must accept at least all values that the procedure base type
accepted
...
6
...

In Java, arrays are covariant
...
Java must therefore check every array assignment at runtime, which makes it both inefficient and
less checkable than languages that have no subtype relationship between arrays of subtypes
...


10

Memory Management

Early languages had no memory management, e
...
, FORTRAN required all arrays to have static size and prohibited recursive procedure calls
...
The stack grows and shrinks (
...
Values on the stack are no longer available after that stack frame is
popped, e
...
, when the procedure that created the frame returns
...
unfortunately, unlike a “heap” data structure)
...

With the introduction of the heap, a language needs a process for managing heap memory to ensure that
programs don’t ever allocate the same block of memory twice, and reclaim memory once it is no longer in
use
...
g
...
Let the free list and allocated list are each lists of block descriptors that have been,
respectively, not allocated (i
...
, are free) or allocated
...

A manual memory management scheme provides the programmer with explicit procedures for allocating and
deallocating heap memory
...
firstNode ( )
w h i l e c u r ! = None :
i f c u r
...
s t a r t , numBytes )
i f ( c u r
...
s i z e −= numBytes
c u r
...
remove ( c u r )
a l l o c L i s t
...
remove ( b l o c k )
f r e e L i s t
...

In order to recover the block size, they often stash it (by convention) in the bytes right before that start address
...
e
...
,
MyObj∗ p t r = ( MyObj ∗ ) m a l l o c ( s i z e o f ( MyObj ) ) ;

...

Some problems with manual memory management:
1
...

2
...

3
...

4
...

In C++, new and delete allow for proper initialization of heap allocated objects
...
Delete invokes the destructor and then frees memory
...

As a result, most C++ programmers will try to allocate objects on the stack whenever possible and create chains
of destructors that automate much of the heap memory management
...
But can
we do better, building this type-safety automation right into the language and addressing the other drawbacks
of memory management?
The allocation part is easy–values have to be explicitly created, so their allocation is necessarily part of the
program
...
Unfortunately,
the function that determines whether a value will be used in the future is noncomputable

...
So we can at best
conservatively approximate this function
...
Algorithms for implementing this
strategy are called garbage collection algorithms
...
In it, each object maintains a count of the number
of incoming references (pointers)
...
This

10

MEMORY MANAGEMENT

29

is used by many implementations of the Python language, by operating systems for managing shared libraries,
and can be implemented in C++ using operator overloading to implement faux-pointers
...
Reference counting has a key weakness: cycles of pointers
ensure that even a completely disconnected component appears to always be in use
...
really the entire structure should crash (in our case, be
deallocated)
...

gc ( )
x = alloc ( size )
i f x == None :
# A f t e r c o l l e c t i n g , s t i l l n o t enough memory
...
marked :
b l o c k
...
p o i n t e r s :
mark ( x )
d e f sweep ( ) :
for x in a l l o c L i s t :
i f n o t x
...
remove ( x )
f r e e L i s t
...
marked = F a l s e
This is much more accurate than reference counting for identifying dead objects, but some problems remain
...
Some calls to alloc may take a
very long time to return as they sweep the allocated part of the heap
...
In addition:
• Free memory becomes fragmented into little blocks over time
...

• We need run-time type information to identify pointers within blocks
...
If it is too small, then we’ll garbage collect too frequently in the beginning
...

One interesting side note is conservative collection, which allows gc to operate on an implementation that
does not provide run-time types
...
Assuming block sizes are stashed right in front of the first byte of the block and that
we have an allocated list, we can quickly reject many false pointers and for the rest can trace them through
the system with mark-sweep
...
Recall that mark-sweep
could not determine whether a block will actually be used in the future, only whether it is referenced
...
One popular
implementation is the Boehm-Demers-Weiser collector http://www
...
hp
...


11

11

SOME POPULAR LANGUAGES

Some Popular Languages

Every language is a point in a large design space
of possible legal semantics (and syntax)
...
Furthermore, if we consider general
use, both in production systems and for theoretical analysis, to be a large testing environment,
then we can have the hope that the environment
exerts a kind of natural selection on languages
and that over time they are hopefully becoming
better at trading expressivity and static checkability
...
Every
language has many variants and implementations
...
So please take this
table as the broad overview that it is intended
...

Often, no single language is appropriate for a
project
...


31

REFERENCES

32

References
Alonzo Church
...
Annals of Mathematics, 33:346–366, 1932
...
Uber
formal unentscheidbare s¨atze der principia mathematica und verwandter systeme
...
Monatshefte f¨ur
Mathematik und Physik, 38:173–198, 1931
...
Programming Languages: Application and Interpretation
...

Barbara Liskov
...
In OOPSLA ’87: Addendum to the proceedings on Objectoriented programming systems, languages and applications (Addendum), pages 17–34, New York, NY, USA, 1987
...

Robin Milner
...
Journal of Computer and System Sciences, 17:348–375,
1978
...
Pierce
...
MIT Press, Cambridge, MA, USA, 2002
...
Java is not type-safe
...
http://www
...
att
...
html
...
On computable numbers, with an application to the Entscheidungsproblem
...
http://www
...
org/browse
...

Jean van Heijenoort, editor
...
Harvard University
Press, 1967
...
Wright and Matthias Felleisen
...
Information and Computation, 115:38–
94, 1994

---