# 22 January 2018: Introduction to Comp 105

There are PDF slides for 1/23/2018.

Handout: Experiences of successful 105 students

Handout: Five proof systems for natural numbers

There is a shared album with photos of lecture. Anybody can add photos.

## Overview

### A ton of languages: Why?

The stuff software is made of: C#, Ruby, JavaScript, Rust, Swift, Dart, …

- Thousands
- Each one unique
- Why do you suppose so many?

Conclusion: **make it easier to write programs that really work**

- An invaluable skill for software practitioners

### What this course isn’t

- Java in January
- F# in February
- Mathematica in March
- ActionScript in April

### Reusable Principles

What if the course were called “Houses”?

You’d need to know something about houses work

- Want to cut a new door? How does wood-frame construction work?
- Digging in yard with backhoe. Then the house blows up. Why?

You’d want to know something about what makes a house livable:

Northern temperate zone: face south, roof with eaves

There are a few different kitchen layouts that work (galley, farmhouse); know what they are and how to exploit them.

Problem: keep water out—while letting water

*vapor*escape

The same thing for programming languages:

How programming languages work: MATH

What makes programming languages usable: Great features for writing CODE

### What Programming Languages is, technically

The marriage of math and code

Principal tools: Induction and recursion

### What can you get out of Comp 105?

New ways of thinking about programming (found in many languages)

Double your productivity

Become a sophisticated consumer, aware of old wine in new bottles

Learn new languages quicklly

Bonus: preparation for advanced study

(Course serves everyone from recent 15/61 grads to grad students)

Students who get the most out of 105 report

- They enjoy programming (15)
- They also like math (61, sort of—induction and proofs)
- They work hard

### Introductions

My pronouns are he, him, his.

Please call me “Norman,” “Professor Ramsey,” or “Mr Ramsey”

Most of the senior staff: Nate, JM, Brian (Lexi, Marilyn)

**For any issue with recitations**: see JM

## Your turn: What makes something a programming language?

Think. Then pair. Then share.

- If you’ve taken 170, a caution: every programming language is a formal language, but not every formal language is a programming language.

This week: new ways of thinking about stuff you already know

## Syntactic structure: induction

#### Numerals

Show some example numerals

Numerals:

```
2018
73
1852
```

Not numerals:

```
3l1t3
2+2
-12
```

**Q:** What does a numeral stand for?

That is, if a numeral appears in the syntax, what sort of value flies around at run time?

**Q:** Does every numeral stand for one of these things?

**Q:** How many of them are there?

**Q:** How many numerals are there?

##### In-class Exercise: Inductive definitions of numerals

Write an inductive definition of numerals

There is more than one! When you finish one, look for another

#### Inductive descriptions of concrete syntax: Backus-Naur Form

**Board**: BNF for numerals**Exercise**: BNF for calculator expressions

#### Ambiguity

Looky here:

`9 - (6 / 13) 9 - 6 / 13 (9 - 6) / 13`

*Superficially different* ways of writing one expression?

### Introducing our common framework

### Recursion: a review

**Case analysis depends on the inductive structure of the input data**

#### Consuming natural numbers recursively

**Q:** How many natural numbers are there?

**Q:** What is a structure that works for natural numbers?

The ways a recursive function could decompose a natural number *n* are related to mathematical ideas about natural numbers:

How we

**define**natural numbers, which in turn can be expressed asHow to

**prove**that something is a natural number

Some examples of decomposition:

Peano’s definition (recursive call drops down one):

`n = 0 n = m + 1, m is also a natural number`

Based on proof judgments:

- ⊢0
`n`

`a`

`t`

- ⊢(
*m*+ 1)`n`

`a`

`t`

Inference rules in handout

- ⊢0
Sequence of decimal digits (see study problems on digits, decimal proof system in handout)

`n = 0 n = 10 * m + d, where 0 <= d < 10`

What does the recursive call do? For example, given

`n`

, how do you find`m`

?Here’s an alternative:

`n = d, where 0 <= d < 10 n = 10 * m + d, where 0 <= d < 10, m > 0`

Both alternatives are in the handout.

Split into two pieces—harder to connect to a proof system:

`n = 0 n = k + (n - k) 0 < k < n (everything gets smaller)`

To do your homework problems, which I recommend starting today, you’ll need to invent at least one more way of decomposing natural numbers.

Let’s try one now!

## Course logistics: Books

My book is available in the CS office in Halligan.

The Ullman book on ML is optional, but very useful. If you can, spend money to gain time.

## Course logistics: Recitation

- Some students are waitlisted for recitation. Find one that’s not full.
- If you have trouble, help from JM, Lexi, Marilyn

# 24 January 2018: Abstract syntax and operational semantics

There are PDF slides for 1/25/2018.

Handout: 105 Impcore Semantics, Part 1

### Where have we been?

**Short discussion**: *Two things you learned in the first class*

## Opening sermon: What the course is like

Why get a university education?

- The opportunity to stretch yourself

The course is hard, but we are totally committed to your success

- There is no grading curve
- Everyone can get A’s
- But you have to work hard

In practice, about half A’s—sometimes more, sometimes less.

#### Your approach

- It’s nice to be smart
- It’s good to work hard
- What’s most important are
*mindful, thoughtful work habits*

If you’re not sure how to work mindfully, start with *frequent pauses* (try every 15 minutes)

## Course logistics and administration

You **must** get my book (Both Volumes!!!)

You won’t need the book on ML for about a month

### Homework

Homework will be frequent and challenging:

- Many small programming problems
- Some theory problems, more like a math problem set
- The occasional larger project, like a type checker or a game solver
- The course is relentlessly cumulative.

Both individual and pair work:

**All**problems should be discussed with others

(Essential to your success)- Discussions must be acknowleged
- Most problems must be
*completed*individually **Do not allow any other student to see your code**.

Arc of the homework looks something like this:

- impcore one star
- opsem two stars
- scheme three stars
- hofs four stars

Four-star homeworks from there on out.

Lesson: **Don’t make plans based on the first couple of homeworks!**

### The role of lectures

- We don’t cover everything in lecture
- Lecture is for just the hard parts
- Lecture is also for modeling problem-solving
- We’ll talk very little about the code (just the interesting bits)

In a 100-level course, you are responsible for your own learning

Like an internship: we point you in the right direction and identify traps and pitfalls, and we find good problems for you to work on.

If you’re expecting to see everything in lecture, you have a couple of choices: change your expectations, or take the course next year when you will have more experience and will be more prepared to manage your own learning.

### Recitations

- Class goes very fast; recitations provide chance to dig in to key topics with classmates.
- Start
*this Thursday and Friday*. - Location information available in SIS.
- Designed to be interactive, so bring your thinking cap.
- An important part of your grade

If you haven’t got a recitation yet:

- You should have gotten an email.
- We’ll make final assignments when we see homework.

### Other policies and procedures in the syllabus

- You are responsible!
- Treasure Hunt for class participation points

### Who am I? What am I called?

Call me “Norman,” “Professor Ramsey,” or “Mister Ramsey.” In a pinch, “Professor” will do. Do not call me “Ramsey”; where I come from, that form of address is insulting.

My pronouns are he, him, and his.

### Who are you? What are you called?

- First homework includes photo, preferred name, pronunciation
- Your photos will be graded!

## Recursion from data

**Case analysis depends on the inductive structure of the input data**

#### Consuming natural numbers recursively

The ways a recursive function could decompose a natural number *n* are related to mathematical ideas about natural numbers:

How we

**define**natural numbers, which in turn can be expressed asHow to

**prove**that something is a natural number

Some examples of decomposition:

Peano’s proof system:

*n*is 0 or*m*+ 1How do you do the case analysis?

If

*n*=*m*+ 1, recover*n*from*m*n = 0 n = m + 1, m is also a natural number

Second decimal proof system:

*n*is*d*or is 10 ×*m*+*d*, where*m*> 10.How do you do the case analysis?

If

*n*= 10 ×*m*+*d*, recover*m*and*d*from*n*

## Thinking about programming languages

This week: abstract syntax and operational semantics (next homework)

### Concrete and abstract Syntax

Programming-languages people are wild about **compositionality**.

- Build sensible things from sensible pieces using just a few construction principles.

Example of compositionality: **concrete syntax** (grammar)

`(x + y)`

is a grammatical expression`(x - y)`

is a grammatical expression- Any two expressions can be be multiplied
`(x + y) * (x - y)`

is an expression`fish`

is a noun phrase;`red`

is an adjective;`red fish`

is a noun phrase

Programming languages more orderly than natural language.

Example of non-compositionality

`fish`

vs`ghoti`

Both composed from letters, but no rules of composition

## Programming-language semantics

“Semantics” means “meaning.”

We want a *computational* notion of meaning.

**What problem are we trying to solve?**

Know

what’s supposed to happen when you run the code

Ways of knowing:

*People*learn from examples- You can build intuition from words

(Book is full of examples and words) - To know
*exactly*,*unambiguously*, you need more precision

(For homework, you’ll prove that our specification is unambiguous.)

**Q:** Does anyone know the beginner exercise “make a peanut butter and jelly sandwich”? (Videos on YouTube)

- You can watch and learn
- A computer can’t
- “Put the peanut butter on the bread”

### Why bother with precise semantics?

(Needed to build implementation, tests)

Same reason as other forms of math:

- Distill down your understanding and express it
- Prove properties people care about (e.g., private information doesn’t leak; device driver can’t bring kernel down)
- Most important for you:
*things that look different are actually the same*

The programming languages you encounter after 105 will certainly look different from what we study this term. But most of them will actually be the same. Studying semantics helps you identify that.

The idea: **your new skills will apply**

### Behavior decomposes

What happens when we run

`(* y 3)`

?

We must know something about `*`

, `y`

, 3, and function application.

**Knowledge is expressed inductively**

Atomic forms: Describe behavior directly (e.g., constants, variables)

Compound forms: Behavior specified by composing behaviors of parts

### ASTs

Question: What do we assign behavior to?

Answer: The **Abstract Syntax Tree (AST)** of the program.

An AST is a

*data structure*that represents a program.A

*parser*converts program text into an AST.

Question: How can we represent all while loops?

`while (i < n && a[i] < x) { i++ }`

Answer:

- Tag code as a while loop
- Identify the condition, which can be any expression
- Identify the body, which can be any expression

As a data structure:

- WHILEX(exp1, exp2), where
- exp1 is the representation of (i < n && a[i] < x), and
- exp2 is the representation of i++

# 29 January 2018: Rules and metatheory

There are PDF slides for 1/30/2018.

Today:

- How do we know what happens when we run the code?
**valid derivations** - What can we prove about it?
**metatheory**

Review: **What elements are needed to know run-time behavior?**

**OK, your turn:** what do you think is rule for evaluating literal, variable? (Base cases)

## Good and bad judgments

## Proofs: Putting rules together

Every terminating computation is described by a data structure—we’re going to turn computation into a data structure: a tree. Proofs about computations are hard (see: COMP 170), but proofs about trees are lots easier (see: COMP 61).

Code example

```
(define and (p q)
(if p q 0))
(define digit? (n)
(and (<= 0 n) (< n 10)))
```

Suppose we evaluate `(digit? 7)`

**Exercise**:

In the body of

`digit?`

, what expressions are evaluated in what order?As a function application, the body matches template

`(`

*f**e*_{1}*e*_{2}`)`

. In this example,- What is
*f*? - What is
*e*_{1}? - What is
*e*_{2}?

- What is

Let’s develop the ApplyUser rule for the special case of two arguments: ⟨*A**P**P**L**Y*(*f*, *e*_{1}, *e*_{2}),*ξ*, *ϕ*, *ρ*⟩⇓?

What is the result of `(digit? 7)`

?

How do we know it’s right?

## From rules to proofs

### Example derivation (in handout)

### Building derivations (Bonus content not covered in class)

## Proofs about derivations: metatheory

Cases to try:

- Literal
- GlobalVar
- SetGlobal
- IfTrue
- ApplyUser2

For your homework, “Theory Impcore” leaves out While and Begin rules.

# 31 Jan 2018: Metatheory wrapup, functional programming

There are PDF slides for 2/1/2018.

Handout: Impcore semantics (page 81), proof template from book (page 61)

Review questions (not easy):

What is the evaluation judgment?

How do you say it?

What’s up with

*ξ*and*ξ*′?How do we capture the time element of a computation?

## Proofs about derivations: metatheory

Cases to try:

- Literal
- GlobalVar
- SetGlobal
- IfTrue
- ApplyUser2

For your homework, “Theory Impcore” leaves out While and Begin rules.

Today: more induction and recursion

## Where are we going?

Recursion and composition:

Recursive functions in depth

Two recursive data structures: the list and the S-expression

More powerful ways of putting functions together (compositionality again, and it leads to reuse)

### Recursion comes from inductive structure of input

Structure of the input drives the structure of the code.

You’ll learn to use a three-step design process:

- Inductive structure
- Equations (“algebraic laws”)
- Code

To discover recursive functions, write algebraic laws:

```
sum 0 = 0
sum n = n + sum (n - 1)
```

Which direction gets smaller?

Code:

```
(define sum (n)
(if (= n 0) 0 (+ n (sum (- n 1)))))
```

Another example:

```
exp x 0 = 1
exp x (n + 1) = x * (exp x n)
```

Can you find a direction in which something gets smaller?

Code:

```
(define exp (x m)
(if (= m 0)
1
(* x (exp x (- m 1)))))
```

## For a new language, five powerful questions

As a lens for understanding, you can ask these questions about any language:

**What is the abstract syntax?**What are the syntactic categories, and what are the terms in each category?**What are the values?**What do expressions/terms evaluate to?**What environments are there?**That is, what can names stand for?**How are terms evaluated?**What are the judgments? What are the evaluation rules?**What’s in the initial basis?**Primitives and otherwise, what is built in?

(Initial basis for *μ*Scheme on page 149)

## Introduction to Scheme

Question 2: what are the **values**?

Two new kinds of data:

The function closure: the key to “first-class” functions

Pointer to automatically managed cons cell (mother of civilization)

Picture of a cons cell: (cons 3 (cons 2 (cons 1 ’())))

### Scheme Values

Values are *S-expressions*.

An S-expression is either

a

**symbol**`'Halligan`

`'tufts`

a

**literal integer**`0`

`77`

a

**literal Boolean**`#t`

`#f`

`(cons`

*v*_{1}*v*_{2}`), where*v*_{1}and*v*_{2}are S-expressions

Many predefined functions work with a **list of S-expressions**

A list of S-expressions is either

the empty list

`'()`

`(cons`

*v*_{1}*v*_{2}`), where*v*_{1}is an S-expression and*v*_{2}is a list of S-expressionsWe say “an S-expression

*followed by*a list of S-expressions”

## For a new language, five powerful questions

As a lens for understanding, you can ask these questions about any language:

**What is the abstract syntax?**What are the syntactic categories, and what are the terms in each category?**What are the values?**What do expressions/terms evaluate to?**What environments are there?**That is, what can names stand for?**How are terms evaluated?**What are the judgments? What are the evaluation rules?**What’s in the initial basis?**Primitives and otherwise, what is built in?

(Initial basis for *μ*Scheme on page 149)

# 5 February 2018: Programming with lists and S-expressions

There are PDF slides for 2/6/2018.

### Homework

- Looks good
- This one time, extensive feedback
- Compare general coding rubric

### Upcoming homework

- Recursive-function practice
- Preparation varies
- May seem redundant

## Review

## Lists

### Subset of S-Expressions.

Can be defined via a recursion equation or by inference rules:

**Constructors**: `'(),`

cons

**Observers**: `null?`

, `pair?`

, `car`

, `cdr`

(also known as “first” and “rest”, “head” and “tail”, and many other names)

### Why are lists useful?

Sequences a frequently used abstraction

Can easily approximate a set

Can implement finite maps with

**association lists**(aka dictionaries)You don’t have to manage memory

These “cheap and cheerful” representations are less efficient than balanced search trees, but are very easy to implement and work with—see the book.

The only thing new here is **automatic memory management**. Everything else you could do in C. (You can have automatic memory management in C as well.)

### Immutable data structures

Key idea of functional programming: **constructed data**. Instead of mutating, construct a new one. Supports composition, backtracking, parallelism, shared state.

### Algebraic laws of lists

You fill in these right-hand sides:

```
(null? '()) ==
(null? (cons v vs)) ==
(car (cons v vs)) ==
(cdr (cons v vs)) ==
(length '()) ==
(length (cons v vs)) ==
```

Combine creators/producers with observers

Can use laws to prove properties of code and to write better code.

### Recursive functions for recursive types

**Any** list is therefore *constructed* with `'()`

or with `cons`

applied to an atom and a smaller list.

- How can you tell the difference between these types of lists?
- What, therefore, is the structure of a function that consumes a list?

Example: `length`

Algebraic Laws for `length`

Code:

`;; you fill in this part`

### Algebraic laws to design list functions

Using informal math notation with .. for “followed by” and e for the empty sequence, we have these laws:

```
xs .. e = xs
e .. ys = ys
(z .. zs) .. ys = z .. (zs .. ys)
xs .. (y .. ys) = (xs .. y) .. ys
```

The underlying operations are `append`

, `cons`

, and `snoc.`

Which ..’s are which?

But we have no

`snoc`

If we cross out the

`snoc`

law, we are left with three cases… but case analysis on the first argument is complete.So cross out the law

`xs .. e == xs`

.Which rules look useful for writing append?

You fill in these right-hand sides:

```
(append '() ys) ==
(append (cons z zs) ys) ==
```

Why does it terminate?

### Cost model

The major cost center is `cons`

because it corresponds to **allocation**.

How many cons cells are allocated?

Let’s rigorously explore the cost of append.

### Induction Principle for List(A)

Suppose I can prove two things:

IH (’())

Whenever a in A and also IH(as), then IH (cons a as)

then I can conclude

Forall as in List(A), IH(as)

*Claim*: Cost (append xs ys) = (length xs)

*Proof*: By induction on the structure of xs.

Base case: xs = ’()

I am not allowed to make any assumptions.

`(append '() ys) = { because xs is null } ys`

Nothing has been allocated, cost is zero

`(length xs) is also zero.

Therefore, cost = `(length xs).

Inductive case: xs = (cons z zs)

I am not allowed to assume the inductive hypothesis for

`zs`

.Therefore, I may assume the number of cons cells allocated by

`(append zs ys)`

equals`(length zs)`

Now, the code:

`(append (cons z zs) ys) = { because first argument is not null } = { because (car xs) = z } = { because (cdr xs) = zs } (cons z (append zs ys))`

The number of cons cells allocated is 1 + the number of cells allocated by

`(append zs ys)`

.`cost of (append xs ys) = { reading the code } 1 + cost of (append zs ys) = { induction hypothesis } 1 + (length zs) = { algebraic law for length } (length (cons z zs)) = { definition of xs } (length xs)`

Conclusion: Cost of append is linear in length of first argument.

# 7 February 2018: Laws, list leftovers, accumulating parameters, let-bound names and anonymous functions

There are PDF slides for 2/8/2018.

Today:

- Algebraic laws
- Costs again: accumulating parameters
- Association lists again
- From values on to syntax

## What is an algebraic law?

A law is an equation.

At least one side, usually both, contains at least one variable, say

*x*.For any value of

*x*in the proper**semantic domain**, the equation holds. And similarly for all other variables.(A semantic domain is a set of values like

*NUM*or*LIST(BOOL)*.)The law justifies

*substitution*of one side for another, which can be used to simplify a formula (math class) or a program (computer-science class)

### Examples of algebraic laws from math class

```
x + 0 = x
(x + y)^2 = x^2 + 2ay + y^2
x * 1 = x
x * 0 = 0
```

### Examples of algebraic laws from computer-science class

```
&a[i] == a + i /* law of C code */
(member? x emptyset) == #f ;; law of uScheme sets
(append (cons x '()) xs) == (cons x xs) ;; append to singleton
```

### Your turn!

Homework asks you to discover a new law. Work with your neighbor to develop four laws involving some combination of `append`

and `reverse`

:

`(append (reverse '()) ys)`

=`(append (reverse (cons z zs)) ys)`

=`(append (reverse xs) '())`

=One new law that you discover:

N.B. There is a **deep trick** behind left-hand sides 1 and 2

## Costs of list reversal

Algebraic laws for list reversal:

```
reverse '() = '()
reverse (x .. xs) = reverse xs .. reverse '(x) = reverse xs .. '(x)
```

And the code?

The `list1`

function maps an atom `x`

to the singleton list containing `x`

.

How many cons cells are allocated? Let’s let `n = |xs|`

.

- Q: How many calls to
`reverse`

? A:`n`

- Q: How many calls to
`append`

? A:`n`

- Q: How long a list is passed to
`reverse`

? A:`n-1`

,`n-2`

, … ,`0`

- Q: How long a list is passed as first argument to
`append`

? A:`n-1`

,`n-2`

, … ,`0`

- Q: How many
`cons`

cells are allocated by call to`list1`

? A: one per call to`reverse`

. - Conclusion:
*O*(*n*^{2}) cons cells allocated. (**We could prove it by induction**.)

## The method of accumulating parameters

Write laws for

`(revapp xs ys) = (append (reverse xs) ys)`

**Who could write the code?**

The cost of this version is linear in the length of the list being reversed.

Parameter `ys`

is the **accumulating parameter**.

(A powerful, general technique.)

## Association lists represent finite maps (code not to be covered in class)

Implementation: list of key-value pairs

`'((k1 v1) (k2 v2) ... (kn vn))`

Picture with spine of cons cells, `car`

, `cdar`

, `caar`

, `cadar`

.

Notes:

- attribute can be a list or any other value
- ‘nil’ stands for ‘not found’

### Algebraic laws of association lists

*μ*Scheme’s new syntax

## An alternative to local variables: `let`

binding

Evaluate `e1`

through `en`

, bind answers to `x1`

, … `xn`

- Name intermediate results (simpler code, less error prone)
Creates new environment for local use only:

`rho {x1 |-> v1, ..., xn |-> vn}`

Also `let*`

(one at a time) and `letrec`

(local recursive functions)

Note that **we would love to have definititions** and it might be easier to read if McCarthy had actually used definition syntax, which you’ll see in ML, Haskell, and other functional languages:

## From Impcore to uScheme: Lambda

Things that should offend you about Impcore:

Look up function vs look up variable requires different interfaces!

To get a variable, must check 2 or 3 environments.

- Can’t create a function without giving it a name:
- High cognitive overhead
- A sign of second-class citizenship

All these problems have one solution: lambda

### Anonymous, first-class functions

From Church’s lambda-calculus:

`(lambda (x) (+ x x))`

“The function that maps x to x plus x”

At top level, like `define`

. (Or more accurately, `define`

is a synonym for `lambda`

that also gives the `lambda`

a name.)

In general, `\x.E`

or `(lambda (x) E)`

`x`

is**bound**in`E`

- other variables are
**free**in`E`

The ability to “capture” free variables is what makes it interesting.

Functions become just like any other value.

### First-class, *nested* functions

`(lambda (x) (+ x y)) ; means what??`

What matters is that `y`

can be a parameter or a let-bound variable of an *enclosing* function.

- Can tell at compile time what is captured.
- To understand why anyone cares, you’ll need examples

**First example**: Finding roots. Given n and k, find an x such that x^n = k.

*Step 1*: Write a function that computes x^n - k.

*Step 2*: Write a function that finds a zero between `lo`

and `hi`

bounds.

Picture of zero-finding function. Algorithm uses binary search over integer interval between `lo`

and `hi`

. Finds point in that interval in which function is closest to zero.

Code that computes *the function* `x^n - k`

given `n`

and `k`

:

The function `to-the-n-minus-k`

is a *higher-order function* because it **returns another (escaping) function as a result**.

General purpose zero-finder that works for any function `f`

:

`findzero-between`

is also a higher-order function because it takes another function as an argument. But nothing escapes; you can do this in C.

Example uses:

### Your turn!!

# 12 Feb 2018: Higher-order functions on lists; currying; tail calls

There are PDF slides for 2/13/2018.

## Last time: conjunction and disjunction

## Today

Plan:

How

`lambda`

worksWhat we can do with it

Working with `lambda`

:

Higher-order functions that consume lists, in three parts:

Manipulating one-argument functions

Using one-argument functions to interrogate and transform lists

Turning two-argument functions into one-argument functions

Tail calls

## How `lambda`

works

It’s not precisely true that rho never changes.

New variables are added when they come into scope.

Old variables are deleted when they go out of scope.

But the location associated with a variable never changes.

### Rule for `lambda`

Key idea: ``every name I can see—remember where it is stored.’’

### Rule for function Application

Questions about ApplyClosure:

What if we used

*σ*instead of*σ*_{0}in evaluation of*e*_{1}?What if we used

*σ*instead of*σ*_{0}in evaluation of arguments?What if we used

*ρ*_{c}instead of*ρ*in evaluation of arguments?What if we did not require ℓ

_{1}, ℓ_{2}∉ dom(*σ*)?What is the relationship between

*ρ*and*σ*?

## Higher-order functions

Preview: in math, what is the following equal to?

`(f o g)(x) == ???`

Another algebraic law, another function:

```
(f o g) (x) = f(g(x))
(f o g) = \x. (f (g (x)))
```

Another example: `(o not null?)`

## Reasoning about functions

### Truth about S-expressions and functions consuming functions

Q: Can you do case analysis on a function?

### Reasoning principles

Recursive function consuming *A* is related to proof about *A*

Q: How to prove two lists are

`equal?`

A: Prove they are both

`'()`

or that they are both`cons`

cells cons-ing equal car’s to equal cdr’sQ: How to prove two

*functions*equal?A: Prove that when applied to equal arguments they produce equal results.

## Currying

*Currying* converts a binary function `f(x,y)`

to a function `f'`

that takes `x`

and returns a function `f''`

that takes `y`

and returns the value `f(x,y)`

.

What is the benefit? Functions like `exists?`

, `all?`

, `map`

, and `filter`

all expect a function of **one** argument. To get there, we use **Currying** and **partial application**.

Curried functions take their arguments “one-at-a-time.”

## Higher-Order Functions on lists

Goal: Start with functions on *elements*, end up with functions on *lists*

- Generalizes to sets, arrays, search trees, hash tables, …

Goal: Capture common **patterns of computation** or **algorithms**

`exists?`

(Ex: Is there a number?)`all?`

(Ex: Is everything a number?)`filter`

(Ex: Take only the numbers)`map`

(Ex: Add 1 to every element)**foldr**(General: can do all of the above.)

Fold also called `reduce`

, `accum`

, a “catamorphism”

### Your turn!!

### List search: `exists?`

Algorithm encapsulated: linear search

Example: Is there an even element in the list?

Algebraic laws:

```
(exists? p? '()) == ???
(exixts? p? '(cons a as)) == ???
(exists? p? '()) == #f
(exixts? p? '(cons a as)) == p? x or exists? p? xs
```

# 14 Feb 2018: List HOFs, tail calls, and continuations

There are PDF slides for 2/15/2018.

### The universal list function: `fold`

`foldr`

takes two arguments:

`zero`

: What to do with the empty list.`plus`

: How to combine next element with running results.

Example: `foldr plus zero '(a b)`

```
cons a (cons b '())
| | |
v v v
plus a (plus b zero)
```

### In-class exercise

### Language design — why?

## Tail calls

Intuition: In a function, a call is in *tail position* if it is the last thing the function does.

A tail call is a *call in tail position*.

Important for optimizations: Can change complexity class.

Anything in tail position is the **last thing executed**!

Key idea is **tail-call optimization**!

Example: `reverse '(1 2)`

Question: How much stack space is used by the call?

Call stack:

```
reverse '()
append
reverse '(2)
append
reverse '(1 2)
```

Answer: Linear in the length of the list

Example: `revapp '(1 2) '()`

Question: How much stack space is used by the call?

Call stack: (each line *replaces* previous one)

revapp ‘(1 2)’() –> revapp ‘(2)’(1) –> revapp ‘()’(2 1)

Answer: Constant

Answer: a **goto**!!

Think of “tail call” as “goto with arguments”

Remember tail calls? Suppose you call a **parameter**!

A **continuation** is code that represents “the rest of the computation.”

- Not a normal function call because continuations never return
- Think “goto with arguments”

### Different coding styles

**Direct style**: Last action of a function is to return a value. (This style is what you are used to.)

**Continuation-passing style (CPS)**: Last action of a function is to “throw” value to a *continuation.*

### Uses of continuations

Compiler representation: Compilers for functional languages often convert direct-style user code to CPS because CPS matches control-flow of assembly.

Some languages provide a construct for

*capturing*the*current continuation*and giving it a name`k`

. Control can be resumed at captured continuation by*throwing*to`k`

.A style of coding that can mimic

*exceptions*Callbacks in GUI frameworks

Even web services!

### Implementation

First-class continuations require compiler support.

We’re going to simulate continuations with function calls in tail position.

## Motivating Example: From existence to witness

Ideas?

Bad choices:

- nil
- special symbol
`'fail`

- run-time error

Good choice:

- exception (not in uScheme)

Question: How much stack space is used by the call?

Answer: Constant

# 21 Feb 2018: Continuation-Passing Style: A SAT Solver

There are PDF slides for 2/22/2018.

Question: How much stack space is used by the call?

Answer: Constant

### Continuations for Search

### Solving a Literal

`start`

carries a partial truth assignment to variables `current`

Box describes how to extend `current`

to make a variable, say `x`

, true.

Case 1: `current(x) = #t`

Call `success`

continuation with `current`

Pass `fail`

as `resume`

continuation (argument to `success`

)

Case 2: `current(x) = #f`

Call `fail`

continuation

Case 3: `x`

not in `current`

Call `success`

continuation with `current{x -> #t}`

Pass `fail`

as `resume`

continuation

### Solving a Negated Literal (Your turn)

`start`

carries a partial truth assignment to variables `current`

Box describes how to extend `current`

to make a negated variable, say `not x`

, true.

Case 1: `current(x) = #f`

Call `success`

continuation with `current`

Pass `fail`

as `resume`

continuation (argument to `success`

)

Case 2: `current(x) = #t`

Call `fail`

continuation

Case 3: `x`

not in `current`

Call `success`

cotinuation with `current{x -> #f}`

Pass `fail`

as `resume`

continuation

### Solving A and B

Solver enters A

If A is solved, newly allocated success continuation starts B

If B succeeds, we’re done! Use

`success`

continuation from context.If B fails, use

`resume`

continuation A passed to B as`fail`

.If A fails, the whole thing fails. Use

`fail`

continuation from context.

### Solving A or B

Solver enters A

If A is solved, we’re good! But what if context doesn’t like solution? It can resume A using the resume continuation passed out as

`fail`

.If A can’t be solved, don’t give up! Try a

**newly allocated failure continuation**to start B.If ever B is started, we’ve given up on A entirely. So B’s success and failure continuations are exactly the ones in the context.

If B succeeds, but the context doesn’t like the answer, the context can resume B.

If B fails, abject failure all around; call the original

`fail`

continuation.

## Bonus content not covered in class: Lisp and Scheme Retrospective

### Common Lisp, Scheme

Advantages:

- High-level data structures
- Cheap, easy recursion
- Automatic memory management (garbage collection!)
- Programs as data!
- Hygenic macros for extending the language
- Big environments, tiny interpreters, everything between
- Sophisticated Interactive Development Environments
- Used in AI applications; ITA; Paul Graham’s company Viaweb

Down sides:

- Hard to talk about data
- Hard to detect errors at compile time

Bottom line: it’s all about `lambda`

- Major win
- Real implementation cost (heap allocation)

## Bonus content: Scheme as it really is

- Macros!
- Cond expressions (solve nesting problem)
- Mutation
- …

### Macros!

### Conditional expressions

### Mutation

# 22 Feb 2018: Solver wrapup, Intro to ML

There are PDF slides for 2/23/2018.

**Board**: pictures of two solvers:

- Make
*either*A or B equal to`b`

(last time) [“or true”, “and false”] - Make
*both*A and B equal to`b`

[“and true”, “or false”]

## Introduction to ML

**Ask the class:** what are the pain points in your *μ*Scheme programming?

Apply your new knowledge in Standard ML:

- You’ve already learned (most of) the ideas
- There will be a lot of new detail
- Good language for implementing language features
- Good language for studying type systems

**Meta**: Not your typical introduction to a new language

- Not definition before use, as in a manual
- Not tutorial, as in Ullman
- Instead, the
**most important**ideas that are**most connected**to your work up to now

### ML Overview

Designed for programs, logic, symbolic data

Theme: Precise ways to describe data

ML = uScheme + pattern matching + static types + exceptions

*μ*Scheme to ML Rosetta stone

```
uScheme SML
(cons x xs) x :: xs
'() []
'() nil
(lambda (x) e) fn x => e
(lambda (x y z) e) fn (x, y, z) => e
|| && andalso orelse
(let* ([x e1]) e2) let val x = e1 in e2 end
(let* ([x1 e1] let val x1 = e1
[x2 e2] val x2 = e2
[x3 e3]) e) val x3 = e3
in e
end
```

### Three new ideas

- Pattern matching is big and important. You will like it. It’s “coding with algebraic laws”
- Exceptions are easy
- Static types get two to three weeks in their own right.

Pattern matching makes code look more like algebraic laws: one pattern for each case

Exceptions solve the problem “I can’t return anything sensible!”

Static types tell us at compile time what the cases are.

And lots of new concrete syntax!

### Examples

The `length`

function.

Algebraic laws:

`length [] = 0 length (x::xs) = 1 + length xs`

The code:

`fun length [] = 0 | length (x::xs) = 1 + length xs`

Things to notice:

No brackets! (I hate the damn parentheses)

Function application by juxtaposition

Function application has

**higher precedence than any infix operator**Compiler checks all the cases (try in the interpreter)

Let’s try another! map, filter, exists, all, take, drop, takewhile, dropwhile

# 26 Feb 2018: Programming with constructed data and types

There are PDF slides for 2/27/2018.

### Announcements

**THE MIDTERM IS COMING**

- Need an accommodation? You have until Wednesday.
- 75 minutes
- Operational semantics, functional programming
- Available March 7
- I’ll be here to answer questions
- But you don’t have to take it in class
- Just return it to CS office two hours after checkout
- There will be a short study guide
- Review the syllabus

ML Learning Guide: note unit testing on page 10

Today’s lecture: lots of info in the notes, but won’t see in class. Because not everybody has a book.

## Foundation: Data

Syntax is always the presenting complaint, but data is what’s always important

- Base types:
`int`

,`real`

,`bool`

,`char`

,`string`

- Functions
**Constructed data**:- Tuples: pairs, triples, etc
- (Records with named fields)
- Lists and other algebraic types

**Deconstruct**using*pattern matching*

“Distinguish one cons cell (or one record) from another”

### Tuple types and arrow types

**Background for datatype review (board):**

if A and B are sets, what is

`A * B`

?if A and B are sets, what is

`A -> B`

?if A, B, and C are sets, what is

`A * B * C`

?

This is all you need to know about the special built-in type constructors (cross and arrow).

### Constructed data: Algebraic data types

Tidbits:

The most important idea in ML!

Originated with Hope (Burstall, MacQueen, Sannella), in the same lab as ML, at the same time (Edinburgh!)

**Board:**

A “suit” is

*constructed*using`HEARTS`

,`DIAMONDS`

,`CLUBS`

, or`SPADES`

A “list of A” is constructed using

`nil`

or`a :: as`

, where`a`

is an A and`as`

is a “list of A”A “heap of A” is either empty or it’s an A and two child heaps

Exegesis (on board):

Notation

`'a`

is a**type variable**- On left-hand side, it is a
**formal type parameter** - On right-hand side it is an ordinary type
- In both cases it represents a single
**unknown type**

- On left-hand side, it is a
Name before

`=`

introduces a new**type constructor**into the**type environment**. Type constructors may be**nullary**.Alternatives separated by bars are

**value constructors**of the typeThey are new and

**hide previous names**(Do not hide built-in names

`nil`

and`list`

from the initial basis!)Value constructors build

**constructed data**Value constructors participate in

**pattern matching****Complete**by themselves:`HEARTS`

,`SPADES`

,`nil`

**Expect parameters**to make a value*or pattern*:`::`

,`HEAP`

`op`

enables an**infix operator**to appear in a**nonfix context****Type application is***postfix*- A list of integer lists is written:
`int list list`

- A list of integer lists is written:
New names into

**two**environments:`suit`

,`list`

,`heap`

stand for new**type constructors**`HEARTS`

,`CLUBS`

,`nil`

,`::`

,`EHEAP`

,`HEAP`

stand for new**value constructors**

Algebraic datatypes are inherently inductive (

`list`

appears in its own definition)—to you, that means**finite trees**`'a * 'a list`

is a**pair type**—*infix operators are always applied to pairs*

## Additional language support for algebraic types: case expressions

## The other form of constructed data: tuples

## Making types work for you

### Types help me, part I: type-directed programming

Common idea in functional programming: “lifting:

`val lift : forall 'a . ('a -> bool) -> ('a list -> bool)`

## Bonus content: Even more algebraic datatypes

Algebraic datatype review:

### Enumerated types

Datatypes can define an enumerated type and associated values.

`datatype suit = HEARTS | DIAMONDS | SPADES | CLUBS`

Here `suit`

is the name of a new type.

The *value constructors* `HEARTS`

, `DIAMONDS`

, `SPADES`

, and `CLUBS`

are the values of type `suit`

.

Value constructors are separated by vertical bars.

### Pattern matching

Datatypes are **deconstructed** using *pattern matching*.

```
fun toString HEARTS = "hearts"
| toString DIAMONDS = "diamonds"
| toString SPADES = "spades"
| toString CLUBS = "clubs"
val suitName = toString HEARTS
```

### But wait, there’s more: Value constructors can take arguments!

`datatype int_tree = LEAF | NODE of int * int_tree * int_tree`

`int_tree`

is the name of a new type.

There are two data constructors: `LEAF`

and `NODE`

.

`NODE`

s take a tuple of three arguments: a value at the node, and left and right subtrees.

The keyword **of** separates the name of the data constructor and the type of its argument.

When fully applied, data constructors have the type of the defining datatype (ie, `int_tree`

).

### Building values with constructors

We build values of type `int_tree`

using the associated constructors: (Draw on board)

```
val tempty = LEAF
val t1 = NODE (1, tempty, tempty)
val t2 = NODE (2, t1, t1)
val t3 = NODE (3, t2, t2)
```

What is the *in-order* traversal of `t3`

?

` [1,2,1,3,1,2,1]`

What is the *pre-order* traversal of `t3`

?

` [3,2,1,1,2,1,1]`

### Deconstruct values with pattern matching

(The `@`

symbol denotes append in ML)

```
fun inOrder LEAF = []
| inOrder (NODE (v, left, right)) =
inOrder left @ [v] @ inOrder right
val il3 = inOrder t3
fun preOrder LEAF = []
| preOrder (NODE (v, left, right)) =
v :: preOrder left @ preOrder right
val pl3 = inOrder t3
```

`int_tree`

is **monomorphic** because it has a single type.

Note though that the `inOrder`

and `preOrder`

functions only cared about the *structure* of the tree, not the payload value at each node.

### But wait, there’s still more: Polymorphic datatypes!

Polymorphic datatypes are written using **type variables** that can be instantiated with *any type*.

`datatype 'a tree = CHILD | PARENT of 'a * 'a tree * 'a tree`

`tree`

is a **type constructor** (written in post-fix notation), which means it produces a type when applied to a type argument.

Examples:

`int tree`

is a tree of integers`bool tree`

is a tree of booleans`char tree`

is a tree of characters`int list tree`

is a tree of a list of integers.

`'a`

is a **type variable**: it can represent any type.

It is introduced on the left-hand of the `=`

sign. References on the right-hand side are types.

`CHILD`

and `PARENT`

are **value constructors**.

`CHILD`

takes no arguments, and so has type `'a tree`

When given a value of type `'a`

and two `'a tree`

s, `PARENT`

produces a `'a tree`

### Constructors build `tree`

values

```
val empty = CHILD
val tint1 = PARENT (1, empty, empty)
val tint2 = PARENT (2, tint1, tint1)
val tint3 = PARENT (3, tint2, tint2)
val tstr1 = PARENT ("a", empty, empty)
val tstr2 = PARENT ("b", tstr1, tstr1)
val tstr3 = PARENT ("c", tstr2, tstr2)
```

### Pattern matching deconstructs `tree`

values

```
fun inOrder CHILD = []
| inOrder (PARENT (v, left, right)) =
(inOrder left) @ [v] @ (inOrder right)
fun preOrder CHILD = []
| preOrder (Parent (v, left, right)) =
v :: (preOrder left) @ (preOrder right)
```

Functions `inOrder`

and `preOrder`

are **polymorphic**: they work on any value of type `'a tree`

. `'a`

is a type variable and can be replaced with any type.

### Environments

Datatype definitions introduce names into:

the type environment:

`suit`

,`int_tree`

,`tree`

the value environment:

`HEART`

,`LEAF`

,`PARENT`

### Inductive

Datatype definitions inherently **inductive**:

the type

`int_tree`

appears in its own definitionthe type

`tree`

appears in its own definition

### Datatype Exercise

## Bonus content: Exceptions — Handling unusual circumstances

### Syntax:

- Definition:
`exception EmptyQueue`

- Introduction:
`raise e`

where`e : exn`

- Elimination:
`e1 handle pat => e2`

### Informal Semantics:

- alternative to normal termination
- can happen to any expression
- tied to function call
- if evaluation of body raises exn, call raises exn

Handler uses pattern matching

e handle pat1 => e1 | pat2 => e2

## Bonus Content: ML traps and pitfalls

## Bonus content (seen in examples)

### Syntactic sugar for lists

## Bonus content: ML from 10,000 feet

### Environments

### Patterns

### Functions

Tuples are “usual and customary.”

### Types

# 28 February 2018: Types

There are PDF slides for 3/1/2018.

Today:

- Revisiting “code from types” idea
- Type system with two types
- Type checking
- Unbounded number of types! (Formation, introduction, elimination)

### Types help me, part I: type-directed programming

Common idea in functional programming: “lifting:

`val lift : forall 'a . ('a -> bool) -> ('a list -> bool)`

### Talking type theory: Introduction and elimination constructs

Part of learning any new field: talk to people in their native vocabulary

**Introduce**means “produce”, “create”, “make”, “define”**Eliminate**means “consume”, “examine”, “observe”, “use”, “mutate”

It’s like knowing what to say when somebody sneezes.

## Type systems

What kind of thing is it?

Slogan: “Types classify terms”

```
n + 1 : int
"hello" ^ "world" : string
(fn n => n * (n - 1)) : int -> int
if p then 1 else 0 : int, provided p : bool
```

Questions type systems can answer:

What kind of value does it evaluate to (if it terminates)?

What is the contract of the function?

Is each function called with the right number of arguments?

(And similar errors)Who has the rights to look at it/change it?

Is the number miles or millimeters?

Questions type systems typically do not answer:

Can it divide by zero?

Can it access an array out of bounds?

Can it take the

`car`

of `’()?Will it terminate?

## Type System and Checker for a Simple Language

**Why do we write a type checker?**

To be educated about programming languages, you must be able to realize inference rules in code. Eventually you should learn to “speak” inference rules like a native. Implementing a type system is a valuable way to build these competencies.

If (when!) you get to do your own language designs, type systems are an area where you are most likely to be able to innovate. The ideas behind type systems apply any time you need to validate user input, for example.

Define an AST for expressions with:

- Simple integer arithmetic operations
- Numeric comparisons
- Conditional
- Numeric literal

### Examples to rule out

Can’t add an integer and a boolean:

```
3 + (3 < 99)
(ARITH(PLUS, LIT 3, CMP (LT, LIT 3, LIT 99)))
```

Can’t compare an integer and a boolean

```
(3 < (4 = 24))
CMP (LT, LIT 3, CMP(EQ (LIT 4, LIT 24)))
```

### Inference rules to define a type system

Form of judgment

*Context*`|-`

*term*`:`

*type*Written

`|- e : tau`

**Contexts vary**between type systems(Right now, the empty context)

Judgment is proved by

**derivation**Derivation made using

*inference rules*Inference rules determine how to code

`val typeof : exp -> ty`

:Given

*e*, find*tau*such that`|- e : tau`

What inference rules do you recommend for this language?

### Rule for arithmetic operators

Informal example:

```
|- 3 : int |- 5 : int
-------------------------
|- 3 + 5 : int
```

Rules out:

```
|- 'a' : char |- 5 : int
---------------------------
|- 'a' + 5 : ???
```

General form:

```
|- e1 : int |- e2 : int
-----------------------------
|- ARITH ( _ , e1, e2) : int
```

### Rule for comparisons

Informal example:

```
|- 7 : int |- 10 : int
-----------------------------
|- 7 < 10 : bool
```

General form:

```
|- e1 : int |- e2 : int
-----------------------------
|- CMP ( _ , e1, e2) : bool
```

### Rule for literals

Informal example:

`|- 14 : int`

General form:

```
--------------------
|- LIT (n) : int
```

### Rule for conditionals:

Informal example:

```
|- true : bool
|- 3 : int
|- 42 : int
--------------------------
|- IF (true, 3, 42) : int
```

General form:

```
|- e : bool
|- e1 : tau1
|- e2 : tau2 tau1 equiv tau2
-----------------------------------
|- IF ( e, e1, e2) : tau1
```

Typing rules let us read off what a type checker needs to do.

input to checker: e

output from checker: tau

### What is a type?

OK: a

*set of values*Better: a

*conservative prediction*about valuesBest: the precise definition:

**classifier for terms**!!The relationship to values becomes a

**proof obligation**.Note: a computation can have a type even if it doesn’t terminate! (Or doesn’t produce a value)

**Source of new language ideas for next 20 years**

Needed if you want to understand advanced designs (or create your own)

## Type checker in ML

```
val typeof : exp -> ty
exception IllTyped
fun typeof (ARITH (_, e1, e2)) =
case (typeof e1, typeof e2)
of (INTTY, INTTY) => INTTY
| _ => raise IllTyped
| typeof (CMP (_, e1, e2)) =
case (typeof e1, typeof e2)
of (INTTY, INTTY) => BOOLTY
| _ => raise IllTyped
| typeof (LIT _) = INTTY
| typeof (IF (e,e1,e2)) =
case (typeof e, typeof e1, typeof e2)
of (BOOLTY, tau1, tau2) =>
if eqType (tau1, tau2)
then tau1 else raise IllTyped
| _ => raise IllTyped
```

An implementor’s trick: If you see *identical* types in a rule,

Give each type a distinct subscript

Introduce equality constraints

Remember to

**be careful using primitive equality**to check types—you are better off with`eqType`

.

# 5 March 2018: Type checking with type constructors

There are PDF slides for 3/6/2018.

**Announcement**: NR extra office hours (needed before spring break):

- 3:30 to 4:30 tomorrow
- 1:00 to 4:00 Wednesday

Review: typing rules for machine expressions

I gave you syntax for simple language

I showed typing rules

Why type checking? Many interesting new ideas begin with type checking.

things that could go wrong:

```
(8 < 10) + 4
(8 == 8) < 9
x + (x :: xs)
let val y = 10 in length y end
```

## Typing Rules: Contexts and Term Variables

**Your turn**:

- What you need for VAR and LET

Things to think about:

Q: What context do we need to *evaluate* an expression?

Q: Do we need all the same context to decide on a type?

Q: What do we need then?

### Rule for var

```
x in dom Gamma tau = Gamma(x)
----------------------------------------
Gamma |- VAR x : tau
```

### Rule for let

```
Gamma |- e : tau
Gamma{x->tau} |- e' : tau'
-------------------------------------
Gamma |- LET x = e in e' : tau'
```

What is the **information flow**?

### Type Checker

Type checker needs Gamma – gives *type* of each “term variable”.

```
val typeof : exp * ty env -> ty
fun typeof (ARITH ..., Gamma ) = <as before>
| typeof (VAR x, Gamma) =
(case maybeFind (x, Gamma)
of SOME tau => tau
| NONE => raise IllTyped)
| typeof (LET (x, e1, e2), Gamma) =
let tau1 = typeof (e1, Gamma)
in typeof (e2, extend Gamma x tau1)
end
```

### Functions

Introduction:

```
Gamma{x->tau1} |- e : tau2
-----------------------------------------
Gamma |- (lambda ([x : tau1]) e) : tau1 -> tau2
```

Elimination:

```
Gamma |- e : tau1 -> tau2
Gamma |- e1 : tau1
-----------------------------
Gamma |- (e e1) : tau2
```

### What’s coming

On the new homework,

You will design new syntax and typing rules for lists

You will extend an existing type checker

You will implement a full type checker from scratch

This is a big chunk of **what language designers do.**

## Type Checking with Type Constructors

Type checking with type constructors

Formation, Introduction, and Elimination

## Where we’ve been and where we’re going

New watershed in the homework

You’ve been developing and polishing programming skills:

**recursion**,**higher-order functions**,**using types to your advantage**. But the problems have been mostly simple problems around simple data structures, mostly lists.We’re now going to shift and spend the next several weeks doing real programming-languages stuff, starting with type systems.

You’ve already seen everything you need to know to implement a basic type checker, and you are almost fully equipped to add array operations and types to Typed Impcore.

What’s next is much more sophisticated type systems, with an infinite number of types. We’ll focus on two questions about type systems:

What is and is not a good type, that is, a classifier for terms?

How shall we represent types?

We’ll look at these questions in two contexts: **monomorphic** and **polymorphic** languages.

## Design and implementation of monomorphic languages

Mechanisms:

Every new variety of type requires

**special syntax**(examples: structs, pointers, arrays)Implementation is a straightforward application of what you already know.

Language designer’s agenda:

What new types do I have (

**formation rules**)?What new syntax do I have to

*create new values with that type*(**introduction rules**)?For

**introduce**think “produce”, “create”, “make”, “define”What new syntax do I have to

*observe terms of a type*(**elimination rules**)?For

**eliminate**think “consume”, “examine”, “interrogate”, “look inside”, or “take apart”, “observe”, “use”, “mutate”

Words “introduce” and “eliminate” are the native vocabulary of type-theoretic language design—it’s like knowing what to say when somebody sneezes.

**Your turn**: If I “add lists” to a language, how many new *types* am I introducing?

### Managing the set of types: Type formation

### Monomorphic type rules

Notice: **one rule for if**!!

## Classic types for data structures

(At run time, identical to `cons`

, `car`

, `cdr`

)

### Typing Rule Exercise

### Coding the arrow-introduction rule

# 12 March 2018: Polymorphic Type Checking; Kinds classify types

There are PDF slides for 3/13/2018.

## Announcements

### Midterm-exam results

```
96 and up: Excellent (14 students)
73 to 95: Very Good (49 students)
58 to 72: Good (19 students)
45 to 57: Fair ( 7 students)
under 45: Poor ( 3 students)
```

### My office hours

About 40% of students have been

Extended illness has cut into time

Deadline for full credit extended to March 30 (not yet posted in course documents).

(I will hope to have extra hours after break. But if my regular hours don’t work for you, send an email proposing three times.)

### Recitation this week

Designed for final stages of homework. Your choice:

- Regression testing your type checker
- Coding in Typed uScheme (You could choose to hold off on problem TD.)

**If** you have submitted your homework, OK to skip—but notify your recitation leader.

### Midterm course evals

Things we cannot fix:

- Cannot get a PDF for you. But will see if some other kind of search is possible.
- Proofs are long and boring—it is the nature of the field. Proofs in PL are interesting only when they are wrong.

Things you already have:

- Every chapter already has a table of contents
- Many chapters also have a summary in the back
- Homework solutions
*are*made available - I have posted locations of office hours

Things we can possibly fix:

- Kitchen too small—“beating the bounds” (resistance to downstairs)
- Summary of algebraic laws is a great idea; we are about done with laws, but I will provide for fall
- Will see if numbered slides are possible
- Model solutions from peers? (We are stretched thin on graders…)
- Code index, immensely challenging—please send bug reports

## Live coding

The sheer tedium of redefining functions like `id`

or `length

The sheer untrustworthiness of the types in the source code

## Today

Last week: Typed Impcore, but in *μ*Scheme syntax

Today: Typed *μ*Scheme

**Recitation this week**: a chance to practice coding in Typed *μ*Scheme. You could choose to hold off on problem TD.

## Limitations of monomorphic type systems

Notes:

**Implementing arrays**on homework**Writing rules for lists**on homework

### Quantified types

## Type formation via kinds

## Polymorphic Type Checking

### Quantified types

Bonus instantiation:

```
-> map
<procedure> :
(forall ('a 'b)
(('a -> 'b) (list 'a) -> (list 'b)))
-> (@ map int bool)
<procedure> :
((int -> bool) (list int) -> (list bool))
```

Two forms of abstraction:

### Type rules for polymorphism

## Type formation through kinds

## Bonus content: a definition manipulates three environments

# 14 March 2018: Type inference

There are PDF slides for 3/15/2018.

### Review

## New topic: Type inference

Questions: where do *explicit types* appear in C?

Where do they appear in Typed *μ*Scheme?

Get rid of all that:

- Guess a type for each formal parameter
- Guess a return type
- Guess a type for each instantiation

**Plan of study**:

Today, I’ll walk through several examples, showing how to

*generate*constraintsAt end of class, you’ll do an example

After break, we’ll

*solve*constraintsAnd for the next homework, you’ll implement both algorithms

#### Let’s do an example on the board

N.B. Book is “constraints first;” lecture will be “type system first.” Use whatever way works for you

`(val-rec double (lambda (x) (+ x x)))`

What do we know?

`double`

has type ′*a*_{1}`x`

has type ′*a*_{2}`+`

has type`int * int -> int`

`(+ x x)`

is an application, what does it require?- ′
*a*2 =`int`

and ′*a*2 =`int`

- ′
Is this possible?

Key idea: *Record the constraint in a typing judgement.*

`'a2 = int /\ 'a2 = int, { double : 'a1, x : 'a2 } |- (+ x x) : int`

Example: `if`

`(if y 1 0)`

`y`

has type ′*a*3,`1`

has type`int`

,`0`

has type`int`

Requires what constraints? (

`int`

=`int`

, ′*a*3 = bool`)

Example:

`(if z z (- 0 z))`

`z`

has type ′*a*3,`0`

has type`int`

,`-`

has type`int * int -> int`

Requires what constraints? (′

*a*3 =`bool`

`/\`

`int`

=`int`

`/\`

′*a*3 =`int`

)Is this possible?

Why not?

## Inferring polymorphic types

```
(val app2 (lambda (f x y)
(begin
(f x)
(f y))))
```

Assume f : ’a_f

Assume x : ’a_x

Assume y : ’a_y

`f x`

implies ’a_f ~ (’a_x -> ’a)

`f y`

implies ‘a_f ~ (’a_y -> ’a’)

Together, these constraints imply ‘a_x = ’a_y and ’a = ’a’

`begin`

implies result of function is ’a

So,

`app2 : (('a_x -> 'a) 'a_x 'a_x -> 'a)`

’a_x and ’a aren’t mentioned anywhere else in program, so

we can generalize to:

`(forall ('a_x 'a) (('a_x -> 'a) 'a_x 'a_x -> 'a))`

which is the same thing as:

`app2 : (forall ('a 'b) (('a -> 'b) 'a 'a -> 'b))`

# 26 March 2018: Making type inference precise

There are PDF slides for 3/27/2018.

### Review

**Board**

The basics:

- For each unknown type, a fresh type variable
- Instead of
`eqType`

, type-equality constraint

The secret sauce:

- Every polymorphic value is instantiated with fresh type variables—a “fresh instance” (e.g.,
`car`

)

Assume nss : ’b

We know car : forall ’a . ’a list -> ’a

=> car_1 : ’a1 list -> ’a1

=> car_2 : ’a2 list -> ’a2

(car_1 nss) => ’b ~ ’a1 list

(car_2 (car_1 nss)) => ’a1 ~ ’a2 list

(car_2 (car_1 nss)) : ’a2

nss : ’b

```
: 'a1 list
: ('a2 list) list
```

So, cc : (’a2 list) list -> ’a2

Because ’a2 is unconstrained, we can generalize:

cc : forall ’a . (’a2 list) list -> ’a

Infer the type of function `two`

:

### Precise inference with Hindley-Milner types

**To code the type-inference algorithm**, replace `eqType`

with constraint generation!

### The inference algorithm, formally

Apply rule: *e*’s type could just be a type variable—we need to force it into the arrow form we need.

### What you know and can do now

# 28 March 2018: Building and using a constraint solver

There are PDF slides for 3/29/2018.

### Announcement

This is the last week you can get full credit for a visit to my office hours. I am offering extended hours at these times:

- Today, Wednesday 28 March, 3:30 to 5:30
- Tomorrow, Thursday 29 March,
- 11:00 to 12:00
- 2:30 to 3:00
- 3:30 to 4:30
- 5:00 to 5:45

- Friday 30 March, 11:00 to 12:00

If you cannot make any of these times, I can book a visit on Friday 30 March between 4:00 and 5:30, if you write to me by the close of business on Thursday.

## Solving constraints

What’s going on with substitutions? We have the informal idea—we just formalize it. It’s a function that behaves a certain way.

Two questions: what’s substitution, and when is a constraint satisfied?

Constraint satisfaction: equal types mean **equal constructors** applied to **equal arguments**—same is in `eqType`

.

### Solving simple type equalities

**Question**: in solving `tau1 ~ tau2`

, how many potential cases are there to consider?

**Question**: how are you going to handle each case?

### Solving conjunctions

### What you can know and do now

Write type inference for everything except VAL, VALREC, and LETX

Write function `solve`

, which, given a constraint C, has one of three outcomes:

Returns the identity substitution in the case where C is trivially satisfied

Returns a non-trivial substitution if C is satisfiable otherwise.

Calls

`unsatisfiableEquality`

in when C cannot be satisfied

## Instantiate and generalize

Moving from type scheme to types (Instantiation)

Moving from types to type scheme (Generalization)

## From Type Scheme to Types

## From Types to Type Scheme

The set *A* above will be useful when some variables in *τ* are mentioned in the environment.

We can’t generalize over those variables.

Applying idea to the type inferred for the function `fst`

:

generalize(’a * ’b -> ’a, emptyset) = forall ’a, ’b. ’a * ’b -> ’a

Note the new judgement form above for type checking a declaration.

On the condition *θ**Γ* = *Γ*: *Γ* is “input”: it can’t be changed.

The condition ensures that *θ* doen’t conflict with *Γ*.

We can’t generalize over free type variables in *Γ*.

Their presence indicates they can be used somewhere else, and hence they aren’t free to be instantiated with any type.

## Type Inference for Lets and Recursive Definitions

Let with constraints, operationally:

`typesof`

: returns*τ*_{1}, …,*τ*_{n}and*C*C-prime from

`map`

,`conjoinConstraints`

,`dom`

,`inter`

,`freetyvarsGamma`

`val theta = solve C'`

`freetyvarsGamma`

,`union`

,`freetyvarsConstraint`

Map anonymous lambda using

`generalize`

, get all the*σ*_{i}Extend the typing environment Gamma (pairfoldr)

Recursive call to type checker, gets

`C_b`

,`\tau`

Return

`(tau, C' /\ C_b)`

Forall things

`val` and `val-rec` |
`let` , `letrec` , … |
`lambda` |
---|---|---|

FORALL contains all variables (because none are free in the context) |
FORALL contains variables not free in the context |
FORALL is empty |

Generalize over all variables (because none are free in the context) |
Generalize over variables not free in the context |
Never generalize |

# 2 April 2018: Lambda Calculus

There are PDF slides for 4/3/2018.

Where have we been and where are we going?

Long tour of expressive power at the level of a function or a group of functions. Type systems considered a significant aid to programmers.

A week of foundations: the test bench for new language features, and the lingua franca of educated people everywhere

To finish the term, language features designed for larger systems: modules and objects

### What is a calculus?

Demonstration of calculus: reduce

`d/dx $(x^2 + y^2)$`

What is a calculus? Manipulation of syntax.

What corresponds to evaluation? “Reduction to normal form”

Calculus examples:

Concurrency | CCS (Robin Milner) |

Security | Ambient calculus (Cardelli and Gordon) |

Distributed computing | pi calculus (Milner) |

Biological networks | stochastic pi calculus (Regev) |

Computation | lambda calculus (Church) |

### Why study lambda calculus?

Theoretical underpinnings for most programming languages (all in this class).

A

*metalanguage*for describing other languages, known to all educated people(

*Church-Turing Thesis*: Any computable operator can be encoded in lambda calculus)*Test bench*for new language features

### The world’s simplest reasonable programming language

Only three syntactic forms:

`M ::= x | \x.M | M M'`

Everything is **programming with functions**

Everything is Curried

Application associates to the left

**Arguments are not evaluated**

First example:

`(\x.\y.x) M N --> (\y.M) N --> M`

Crucial: argument N is never evaluated (could have an infinite loop)

## Programming in Lambda Calculus

Systematic approach to **constructed data**

**Alert to the reading**: Wikipedia is reasonably good on this topic

**EXCEPT**for the way they encode lists, which is bogus (violates abstraction)

Everything is continuation-passing style

Q: Who remembers the boolean-formula solver?

Q: What classes of results could it produce?

Q: How were the results delivered?

Q: How shall we do Booleans?

### Coding Booleans

A Boolean takes **two continuations**:

```
true = \x.\y.x
false = \x.\y.y
if M then N else P = ???
```

### Coding pairs

If you have a pair containing a name and a type, how many

*alternatives*are there?How many continuations?

What information does each expect?

What are the algebraic laws?

Code

`pair`

,`fst`

,`snd`

`pair x y k = k x y fst p = p (\x.\y.x) snd p = p (\x.\y.y) pair = \x.\y.\f.f x y fst = \p.p (\x.\y.x) snd = \p.p (\x.\y.y)`

### Coding lists

How many ways can lists be created?

How many continuations?

What does each continuation expect?

For each creator, what are the laws regarding its continuations?

`cons y ys n c = c y ys nil n c = n car xs = xs error (\y.\ys.y) cdr xs = xs error (\y.\ys.ys) null? xs = xs true (\y.\ys.false)`

What are the definitions?

`cons = \y.\ys.\n.\c.c y ys nil = \n.\c.n car = \xs.xs error (\y.\ys.y) cdr = \xs.xs error (\y.\ys.ys) null? = \xs.xs true (\y.\ys.false)`

What do those second continuations look like? (This is the source of Wikipedia’s terrible hack)

### Coding numbers: Church Numerals

# 4 April 2018: Lambda-calculus semantics; encoding recursion

There are PDF slides for 4/5/2018.

### Today

Lambda:

- Operational semantics
- Beta reduction and capture-avoiding substitution
- Reduction strategies (making deterministic)
- Fixed points and recursion equations

### Announcments

Jeff Foster’s class

Jumbo Code takes teams of about 10 Tufts students and develops software for a non-profit in the Boston area, and we’re looking for students to manage those projects. You are qualified! There will be an event Friday at 5:30 in 111A. With pizza! I am told it s a great resume builder and learning experience, especially if you’re interested in potentially going into project management.

Andrew Hoiberg will answer questions, and there is a Facebook event at https://www.facebook.com/events/162417827707984/.

### Review

Review: Church encodings

**Your turn:** write `and`

Question: **What’s missing from this picture?**

Answer: We’re missing recursive functions.

Astonishing fact: we don’t need `letrec`

or `val-rec`

(to com)

## Operational semantics of lambda calculus

New kind of semantics: **small-step**

New judgment form

`M --> N ("M reduces to N in one step")`

No context!! No turnstile!!

Just pushing terms around == calculus

Board examples:

Are these functions the same?

`\x.\y.x \w.\z.w`

Are these functions the same?

`\x.\y.z \w.\z.z`

Examples of free variables:

```
\x . + x y
\x. \y. x
```

## Beta-reduction

The substitution in the beta rule is the **heart of the lambda calculus**

- It’s hard to get right
- It’s a stupid design for real programming (shell, tex, tcl)
- It’s even hard for theorists!
- But it’s the simplest known thing

Example:

```
(\yes.\no.yes)(\time.no) ->
\z.\time.no
```

and never

`\no.\time.no // WRONG!!!!!!`

Really wrong!

```
(\yes.\no.yes) (\time.no) tuesday
-> WRONG!!!
(\no.\time.no) tuesday
->
\time.tuesday
```

Must **rename the bound variable**:

```
(\yes.\no.yes) (\time.no) tuesday
->
(\yes.\z.yes) (\time.no) tuesday
->
(\z.\time.no) tuesday
->
\time.no
```

Nondeterminism of conversion:

```
A
/ \
V V
B C
```

Now what??

## Normal forms

## Reduction strategies (your homework, part 2)

### Applicative-order reduction

Given a beta-redex

`(\x.M) N`

do the beta-reduction **only if N is in normal form**

- Good model for ML and Scheme, so-called “call by value” languages
- Think “arguments before bodies”

Q: Does applicative order ever prevent you from making progress?

A: No. We can prove it by induction on the number of lambdas in N

### Normal-order reduction

Always choose **leftmost, outermost redex**

**Normalization theorem:**if a normal form exists, this will find itModel for Haskell, Clean

You can try ‘uhaskell’, but if it does anything useful, we’re all surprised and pleased

“Normal-order” stands for **produces a normal form**, *not* for “the normal way of doing things”

**Not** your typical call-by-value semantics!

## Fixed points, recursion

Suppose `g F = F`

. Proof that `F`

is factorial.

For all `n`

, `g F n`

= `n!`

, by induction:

```
F 0 = g F 0 = 1
F n
= { by assumption }
g F n
= { definition of g }
if n = 0 then 1 else n * F (n-1)
= { assumption, n > 0 }
n * F (n-1)
= { induction hypothesis }
n * (n-1)!
= { definitiion of factorial }
n!
```

**Now you do it**

## Fixed-point operators

## Lambda calculus in context

What’s its role in the world of theory?

```
Operational semantics Type theory Denotational Lambda
(Natural deducation style) semantics calculus
-------------------------- ----------- ------------ --------
Interpreters like Python type checkers compilers *models*
```

Why is it “calculus”?

Differential calculus example: d/dx x^n equals what?

What’s going on here?

Answer:

**pure formal manipulation**No understanding of functions required; you could write a program to do it (and many people have)

What’s the role of calculi in computer science:

Lambda calculus:

A

*metalanguage*for describing other languagesA

*starter kit*for experimenting with new features

Process calculus:

Concurrent and parallel programming

Biological processes!

Pi calculus:

- Mobile computing and mobile agents

Ambient calculus:

- Security and protection domains

Why so many calculi? They have **simple metatheory** and proof technique.

# 9 April 2018: Hiding information with abstract data types

There are PDF slides for 4/10/2018.

Where have we been?

- Programming in the small
- Expressive power
Success stories:

- First-class functions
- Algebraic data types and pattern matching
- Polymorphic type systems

What about *big* programs?

An area of agreement and a great divide:

```
INFORMATION HIDING
(especially: mutable data)
/ \
/ \
modular reasoning / \ code reuse
/ \
internal access / \ interoperability
to rep / \ between reps
/ \
MODULES OBJECTS
ABSTRACT TYPES
```

### Why modules?

Unlocking the final door for building large software systems

You have all gotten good at first-class functions, algebraic data types, and polymorphic types

Modules are the last tool you need to build big systems

### Modules overview

Functions of a true module system:

**Hide***representations*,*implementations*, private**names**“Firewall” separately compiled units (promote independent compilation)

Possibly reuse units

Real modules include *separately compilable* **interfaces** and **implementations**

Designers almost always choose static type checking, which should be “modular” (i.e., independent)

C and C++ are cheap imitations

- C doesn’t provide namespaces
- C++ doesn’t provide modular type checking for templates

### Interfaces

Collect *declarations*

- Unlike
*definition*, provides*partial*information about a name (usually*environment*and*type*)

Things typically declared:

Variables or constants (values, mutable or immutable)

Types

Procedures (if different from values)

Exceptions

Key idea: **a declared type can be abstract**

- Just like a primitive type

Terminology: a module is a **client** of the interfaces it depends on

Roles of interfaces in programming:

The unit of

*sharing*and*reuse*Explainer of libraries

Underlie component technology

The best-proven technology for structuring large systems.

### Ways of thinking about interfaces

Means of hiding information (ask “what secret does it hide?”)

A way to

**limit what we have to understand**about a program- Estimated force multiplier x10

A contract between programmers

- Essential for large systems
- Parties might be you and your future self

Interface is the

*specification*or*contract*that a*module*implements- Includes contracts for all declared functions

### Module Implementations

Holds all dynamically executed code (expressions/statements)

May include private names

May depend only on interfaces, or on interfaces and implementations both (max cognitive benefits when all dependency is mediated by interfaces)

Dependencies may be implicit or explicit (

`import`

,`require`

,`use`

)

## Standard ML Modules

The Perl of module languages?

Has all known features

Supports all known styles

**Rejoice**at the expressive power**Weep**at the terminology, the redundancy, the bad design decisions

What we’ve been using so far is the **core language**

Modules are a **separate language** layered on top.

### Signature basics

### ML Modules examples, part I

# 11 April 2018: more ML modules

There are PDF slides for 4/12/2018.

## Abstract data types

## Data abstraction for reuse

## Functors and an Extended SML Example

## Bonus content not covered in class: Error-tracking Interpreter

### Why this example?

Lots of interfaces using ML signatures

Idea of how to compose large systems

Use case for the error summaries from recitation

Some ambitious, very abstract abstractions—it’s almost the last week of class, and you should see something ambitious.

Practice implementing functors

Error modules: *Three common implementations*

Collect

*all*errorsKeep just the

*first*errorKeep the

*most severe*error

Your obligations: two types, three functions, algebraic laws

### Computations Abstraction

Ambitious! (will make your head hurt a bit)

Computations either:

return a value

produce an error

Errors must be threaded through everything :-(

That’s really painful!

We can extend the computation abstraction with sequencing operations to help.

### Example:

```
eval e1 + eval e2
(op +) (eval e1, eval e2)
curry (op +) (eval e1) (eval e2)
curry (op +) <$> eval e1 <*> eval e2
```

The first three versions are not well typed. Why?

The last version will thread errors through the compuation behind the scenes.

Note:

```
eval e1, eval e2 : int comp
curry (op +) : int -> (int -> int)
<$> : (int -> (int -> int)) * (int comp) -> (int -> int) comp
<*> : (int -> int) comp * int comp -> int comp
curry (op +) <$> eval e1 : (int -> int) comp
let pa = curry (op +) <$> eval e1
note by above, pa : (int -> int) comp
pa <*> eval e2 : int comp
```

## ML Module summary

# 18 April 2018: Object-orientation

There are PDF slides for 4/19/2018.

Announcement: **No recitations this week**

Demo: circle, square, triangle, with these methods:

`position:`

*cardinal-point*`set-position:to:`

*cardinal-point**coordinate*`draw`

Instructions to student volunteers

- You have one instance variable, which is a coordinate position.

Messages:

Object 1, adjust your coordinate to place your South control point at (0, 0).

Object 1, what is the coordinate position of your North control point?

Object 2, adjust your coordinate to place your South control point at (0, 2).

Object 2, what is the coordinate position of your North control point?

Object 3, adjust your coordinate to place your Southwest control point at (0, 4).

Object 1, draw yourself on the board

Object 2, draw yourself on the board

Object 3, draw yourself on the board

## Key concepts of object-orientation

### Key mechanisms

**Private instance variables**

- Only object knows its instance variables and can see them
- C++ calls these “members”
- Like the coordinate of the geometric figure
- (This is the information hiding)

**Code attached to objects and classes**

- Code needed to draw the object is associated with the object

**Dynamic dispatch**

- We don’t know what function will be called
- In fact, there is no function; code is a ``method’’
- (This is a species of higher-order programming)

### Key idea

**Protocol** determines **behavioral subtyping**

### Class-based object-orientation

Dynamic dispatch determined by *class definition*

Code reuse by sending messages around like crazy

## Example: list filter

## Blocks and Booleans

`[block (formals) expressions]`

For parameterless blocks (normally continuations),

`{expressions}`

Blocks are **objects**

- You don’t “apply” a block; you “send it the
`value`

message”

Booleans use continuation-passing style

- Blocks delay evaluation

Booleans *implemented* with two classes `True`

and `False`

- one value apiece

### Method dispatch in the Booleans

**Board** - Method dispatch

To answer a message:

Consider the

**class**of the**receiver**Is the method with that name defined?

If so, use it

If not, repeat with the

**superclass**

Run out of superclasses?

“Message not understood”

# 23 April 2018: Inheritance. Numbers and magnitudes

There are PDF slides for 4/24/2018.

## History and overview of objects

### History of objects

We know that mixing code and data can create powerful abstractions (function closures)

Objects are another way to mix code and data

Pioneers were Nygaard and Dahl, who added objects to Algol 60, producing SIMULA-67, the first object-oriented language

Bjarne Stroustrup liked Simula but wanted complete control of costs, so he created C++

James Gosling wanted something a little cleaner and a little more like Simula, created Java

Microsoft funded C#

Objects are everywhere

### What’s an object?

Agglutination containing

Some mutable state (

**instance variables**)Code that can respond to

**messages**(code is called**methods**)

A lot like a closure

### What are objects good at?

Not really useful for building small things

If you build a big, full-featured abstraction, you can easily use inheritance to build another, similar abstraction. Very good at adding new kinds of things that behave similarly to existing things.

Programs that are

*evolving*A particular

*kind*of evolution:*operations*stay the same, but we add new kinds of*things*Example: GUIs (operations are

`paint`

and`respond-to-mouse-click`

)Example: numbers

For your homework, you’ll take a Smalltalk system that has three kinds of numbers, and you’ll add a fourth kind of number.

### What’s hard about objects?

If you do anything at all interesting, your control flow becomes smeared out over half a dozen classes, and your algorithms are nearly impossible to undrstand.

## Smalltalk objects

Why Smalltalk?

- Another Turing Award
- Small, simple, pure objects
- Almost the complete language can be done in a relatively small interpreter
Alive and well today

- At the core of Ruby
- As an extension to C (“Objective C”) for Apple products

The five questions:

**Values**are**objects**(even`true`

, 3,`"hello"`

)Even

*classes*are objects!There are

**no functions**—only methods on objects**Syntax**:mutable variables

**message send**sequential composition of mutations and message sends (side effects)

“blocks” (really closures, objects and closures in one, used as continuations)

No

`if`

or`while`

. These are implemented by**passing continuations to Boolean objects**.

(Smalltalk programmers have been indoctrinated and don’t even notice)

**Environments**Name stands for a mutable cell containing an object:

- Global variables
- “Instance variables” (new idea, not yet defined)

**Types**There is no compile-time type system.

At run time, Smalltalk uses

**behavioral subtyping**, known to Rubyists as “duck typing”**Dynamic semantics**- Main rule is
**method dispatch**(complicated) - The rest is familiar

- Main rule is
The

**initial basis**is*enormous*- Why? To demonstrate the benefits of reuse, you need something big enough to reuse.

### Message passing

Look at `SEND`

- Message identified
**by name**(messages are not values) - Always sent to a
**receiver** - Optional arguments must match
**arity**of message name

(no other static checking)

N.B. `BLOCK`

and `LITERAL`

are special objects.

## Magnitudes and numbers

Key problems on homework

`Natural`

is a`Magnitude`

“Large integer” is a

`Number`

# 25 April 2018: Double dispatch, collections

There are PDF slides for 4/26/2018.

**COURSE EVALUATIONS**: email me your response

### Two topics for today

Information hidden and revealed; three layers

(Focus on extending open systems)

Collections: more OO design, plus useful for homework

### Making open system extensible

## Bonus content not covered in class: Collections

### Why collections?

Goal of objects is **reuse**

Key to successful reuse is a well-designed **class hierarchy**

Killer app: toolkits for building user interfaces

Smalltalk blue book is 90 pages on language, 300 pages on library

Lots of abstract classes

- Define protocols
- Build reusable stuff, just like
`Boolean`

,`Magnitude`

,`Number`

### Implementing Collections

Question: what’s the most efficient way to find the size of a list?

Question: what’s the most efficient way to find the size of an array?

### Subtyping

Key strategy for reuse in object-oriented languages: **subtype polymorphism**

A value of the

*subtype*can be used wherever a value of the*supertype*is expected.Board:

**SUBTYPE != SUBCLASS****SUPERTYPE != SUPERCLASS**

Only crippled languages like C++ identify subtype with subclass

Only the ignorant and uneducated don’t know the difference

### Example collection - Sets

Most subclass methods work by delegating all or part of work to list `members`

N.B. `Set`

is a **client** of `List`

, not a subclass!

**Next example highlight**: class method and `super`

!