# 6 September 2017: Introduction to Comp 105

There are PDF slides for 9/7/2017.

Handout: Experiences of successful 105 students

### Announcements

Recitations start this week (tomorrow!)

First HW due Wednesday, September 13.

## Overview

### Why so many languages?

**Question:** What languages have you programmed in?

There are thousands of programming languages, each unique.

**Question:** Why do you suppose there are so many?

**The right language for the job makes it easier to write programs that really work**

An invaluable skill for software practitioners

Your language can make you or break you.

- Example
- Writing a compiler requires a language that facilitiates maniuplating tree data structures
- Relevant features: algebraic data types, pattern matching, efficient recursion, higher-order functions

The **Blub paradox**

- Essay by Paul Graham on the relative power of programming languages.

### What this course isn’t

- Simula in September
- Objective-C in Ocobter
- Visual Basic in November
- C in December

**Why not?**

- Because you’d spend most of your time learning shallow details like program syntax, tool chains, and library interfaces.

### What this course is:

- Reusable Principles

**Why?**

- Once you know the principles, you’ll be able to
*teach yourself new languages quickly*and improve your coding in*many different languages*.

### What are reusable principles?

What if the course were called “Cooking”?

You’d need to know something about how cooking works (THEORY)

Want to make bread? How does yeast work?

Want to avoid getting sick? Under what conditions do bacteria thrive?

Want to develop flavor? What triggers the Maillard reaction?

You’d need to know something about how to cook effectively (PRACTICE)

French cuisine: mirepoix (onions, carrots, celery cooked in butter)

Base sauces (the 5 “mother sauces” of Western cooking); Know what they are and when to use them.

The same division for programming languages:

How programming languages work (THEORY)

- MATH: logic, semantics, type theory, induction

How to make them effective (PRACTICE)

- What features enable compact, efficient, maintainable CODE?

### What Programming Languages are, technically

The marriage of math and code

Principal tools: Induction and recursion

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

Discover new ways think about programming (in

**many**languages)- For example: master using recursive, higher-order functions

Double your productivity

- By choosing the right language/feature for the job

Become a sophisticated consumer, recognizing familiar features in new languages

Learn new languages quickly

Bonus: Prepare 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 (a la 15)
- They also like math (a la 61, sort of—induction and proofs)
- They work hard

### Great languages begin with great *features*

Language shapes your thinking

There aren’t that many great features, and you will see them

*over*and*over*You’ll

*choose*features, and therefore languages, to fit your needsSome are more powerful than others

Examples: first-class functions, continuations, pattern matching, type inference

In Comp 105,

We

**explode your brain**so you can think differentlyYou’ll know you’re doing it right if at first your head hurts terribly, then you have a breakthrough moment and it all seems pleasant afterwards

### How will we study language features?

Write (lots of!) small programs exercising those features

- High power-to-weight ratio (lots of thought per line)

Learn formal tools to describe language features precisely

Operational Semantics (What do programs mean?)

Typing Rules (What can we prove about all programs without running them?)

Extend language

*implementations*so you understand what is under the hood.Prove properties about various language features

### Common Framework

Sequence of Scheme-based pedagogical languages with increasing power

- Simplest language: ImpCore (IMPerative CORE)

Implementation language:

Start in C

Shift to ML once we have learned that language

Foundation of operational semantics and typing rules

## Course logistics and administration

### Books

You

**must**get Norman’s book (Both Volumes!!!)ML book is optional, but very useful. You won’t need it until October 11.

### 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
- Submit everything electronically
- First homework is
*due a week from today*; designed to get you moving quickly. - 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 anyone else to see your code**.- For some problems larger in scope, you can work in pairs
**Be very careful**to separate your pair work and your individual work. (A mistake could be major violation of academic integrity, with severe penalties.)

Arc of the homework looks something like this:

Assignment | Difficulty |
---|---|

impcore | one star |

opsem | two stars |

scheme | three stars |

hofs | four stars |

And it’s more or less four-star homeworks from there on out.

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

Just as intellectually challenging as COMP 40, but in an entirely different direction.

- Not “How long until this huge pile of code works?”
- Instead “How long until I get the Aha! Moment that makes these 10 lines work?”

**Everyone who takes this class has the ability to master the material; Succeeding just requires digging in.**

We provide lots of resources to help:

Lectures

Readings

Recitations

Office hours

Piazza

We encourage you to form study groups so you have thought partners.

Two two bad habits to avoid:

Working on your own.

Trying to cram the assignments at the last minute.

### The role of lectures

We don’t cover everything in lecture

Lecture is for just the hard parts

We’ll talk very little about the code (just the interesting bits)

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

Course evaluations from previous years: a few students want everything gone over in lecture. That’s not how things work in real life, and that’s not how things work here. 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.
- Count towards class participation.

### Questions and answers on Piazza

- Don’t just ask questions; answer them too.
- Both activities count toward class participation.
- Be super careful that
**any question containing your code must be private**. (This is an issue of academic integrity.)

### Other policies and procedures on the web

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

### What am I called?

Call me “Kathleen,” “Professor Fisher”, or “Profesor.”

## ImpCore: The first language in our common framework

### Exercise: all-fours?

Write a function that takes a natural number n and returns true (1) iff all the digits in n are 4’s.

- Impcore interpretor: > impcore
- Command (use homework/fours.imp); will load file into interpretor
- Syntax: parentheses with keyword or function name to start
- An Impcore program is a sequence of definitions (and expresions)

### Scoping rules for Impcore

Scopes also called “name spaces”; we will call them “environments” because that’s the pointy-headed theory term—and if you want to read some of the exciting papers, pointy-headed theory has to be second nature.

## Recursion: a review

Ways a recursive function could decompose a natural number *n*.

Peel back one (Peano numbers):

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

Split into two pieces:

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

Sequence of decimal digits (see study problems on digits)

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

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

# 11 September 2017: Introduction to Semantics

There are PDF slides for 9/12/2017.

Handout: 105 Impcore Semantics, Part 1

Today: Abstract Syntax and Operational Semantics

Discussion: Two things you learned last class.

## Programming-language semantics

Semantics means 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

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

- You can watch and learn, but a computer can’t.
- “Put the peanut butter on the bread”

### Why bother with precise semantics?

Same reason as other forms of math:

- Distill understanding
- Express it in sharable way
- Prove useful properties. For example:
- private information doesn’t leak
- device driver can’t crash the OS kernel
- compiler optimizations prserve program meaning
- Most important for you:
*things that look different are actually the same*

Plus, needed to build language implementation and tests

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: **The skills you learn in this class will apply**

### Behavior decomposes

We want a *computational* notion of meaning.

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

(Non)-Example of compositionality: Spelling/pronunciation in English

`fish`

vs`ghoti`

- Both composed from letters, but no rules of composition for pronunciation.

*By design, programming languages more orderly than natural language.*

### 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++

**With that as background, we can now dive in to the semantics for Impcore!**

# 13 September 2017: Semantics, Syntactic Proofs, Metatheory

There are PDF slides for 9/14/2017.

Handout: Impcore expression rules

## Announcements

- Impcore homework due tonight
- Opsem homework now available

## Today

- Operational semantics of function application
- How we know what the code is supposed to do at run time:
**valid derivations** - What we know about valid derivations:
**metatheory**

## Last Time

- Compositionality
- Abstract Syntax Trees
- Environments: Globals (
*ξ*), Functions (*ϕ*), Locals (*ρ*) - Abstract machines
- Evaluation judgement
- Operational Semantics
- Correspondance between code and inference rules

Both math and code on homework

You’re good with code—lecture and recitation will focus on math

Questions:

- In what order are the actual parameters evaluated?
- How can you tell?

What happens if the formal parameter names are duplicated?

- How many formal parameters can the body of f access?
- What are their names?

Can changes to formal parameters in the body of f be seen by the code calling f?

Can changes to globals in the body of f be seen by the code calling f?

## Using Operational Semantics

**The big idea**:

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

**Valid derivations, or “How do I know what this program should evaluate to?”**

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

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

?

How do we know it’s right?

## From rules to proofs

What can a proof tell us?

### Example derivation (rules in handout)

### Building derivations

At this point, we’ve now covered derivations and how a single derivation corresponds to evaluating a particular program.

## Proofs about *all* derivations: Metatheory

Cases to try:

- Literal
- GlobalVar
- SetGlobal
- IfTrue
- ApplyUser2

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

# 18 September 2017: Metatheory wrapup. Intro to functional programming

There are PDF slides for 9/19/2017.

## Announcements

- Impcore homework returned via email

## Today

- More induction on derivations (metatheory)
- Introduction to Scheme

## Last Time

- Operational semantics of function application
- A valid derivation defines the execution of a single program.
- Metatheory allows us to prove things about
**all programs**in the language.

## 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 157)

## 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)

### Graphically:

(cons 3 (cons 2 ’()))

### 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”

### S-Expression operators

Like any other abstract data type, S-Expresions have:

**creators**that create new values of the type`'()`

**producers**that make new values from existing values`(cons s s')`

**mutators**that change values of the type (not in uScheme)**observers**that examine values of the type

`number?`

`symbol?`

`boolean?`

`null?`

`pair?`

`car`

`cdr`

N.B. creators + producers = constructors

The symbol ’ is pronounced “tick.”

It indicates that what follows is a literal.

Picture of `(cons c (cons b (cons a '())))`

### Your turn!

- What is the representation of

`'((a b) (c d))`

which can be alternatively written

`cons( (cons a (cons b '()))`

` `(cons (cons c (cons d '())) '()))``

- What is the representation of

`cons('a 'b)`

Contrast this representation with the one for

`cons('a '())`

Both of these expressions are S-expressions, but only `cons('a '())`

is a list.

# 20 September 2017: More Scheme

There are PDF slides for 9/21/2017.

## Announcements

- OpSem Homework due tonight
- Scheme I: Recursive Programming with Lists Homework now available.

## Today

- Lists
- Algebraic Laws for writing functions
- The
`cons`

cost model - The method of accumulating parameters

## Last Time

- Wrapped up induction on derivations
- Introduction to Scheme
- S-expressions and cons cells

## 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. Instead of mutating, build a new one. Supports composition, backtracking, parallelism, shared state.

### Review: 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 to create laws.

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`

.

### Example: Append

- 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(Z)

Suppose I can prove two things:

IH (’())

Whenever z in Z and also IH(zs), then IH (cons z zs)

then I can conclude

Forall zs in List(Z), IH(zs)

### Example: The cost of `append`

*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, so the cost is zero.

`(length xs)`

is also zero.Therefore, cost =

`(length xs)`

.

Inductive case: xs = (cons z zs)

I am 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.

### Example: 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

The function `revapp`

takes two list arguments `xs`

and `ys`

.

It reverses `xs`

and appends the result to `ys`

:

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

Write algebraic laws for `revapp`

involving different possible forms for `xs`

.

**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.)

### Linear reverse, graphically

We call `reverse`

on the list `'(1 2 3)`

:

Function `reverse`

calls the helper function `revapp`

with `'()`

as the `ys`

argument:

The `xs`

parameter isn’t `'()`

, so we recursively call `revapp`

with the `cdr`

of `xs`

and the result of `cons`

ing the `car`

of `xs`

onto `ys`

:

The `xs`

parameter still isn’t `'()`

, so we again call `revapp`

recursively:

Still not `'()`

, so we recurse again:

This time `xs`

is `'()`

, so now we just return `ys`

, which now contains the original list, reversed!

# 25 September 2017: Let and Lambda

There are PDF slides for 9/26/2017.

## Announcements

- Scheme I HW due 9/27

## Last Time

- Inductive definitions: List of Z
- List functions (
`'()`

,`cons`

,`car`

,`cdr`

,`null?`

) - Cost model: number of
`cons`

allocations - Accumulating parameters:
`revapp`

## Today

- Association lists [Not covered in class]
- Let construct
- Anonymous functions

## Association lists represent finite maps [Not covered in class]

Implementation: List of key-value pairs

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

Picture with spine of cons cells

Functions `car`

, `cdar`

, `caar`

, `cadar`

can help navigate.

`car`

: Contents of the address register`caar`

: Contents of the address then address register`cdar`

: Contents of the address then data register`cadar`

: Contents of the address then data then address registers

Recall that the left box in a `cons`

cell is the *address* and the right box is the *data*. Read the `a`

as “address” and the `d`

as “data” from right to left.

In association lists, these operations correspond to

`car`

: First key value pair, e.g.,`'(k1 v1)`

`caar`

: Key of first key value pair, e.g.`'k1`

`cdar`

: List of values of first key value pair, e.g.`'(v1)`

`cadar`

: Contents of the address then data then address registers, e.g.`'v1`

Notes:

- An attribute can be a list or any other value.
`'()`

stands for ‘not found’

### Algebraic laws of association lists

## Handy new feature of Scheme: `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 have definititions in the language** 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

Things that should offend you about Impcore:

Looking up a function and looking up a variable require different interfaces! (

`isvalbound`

and`isfunbound`

)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!!

### Escaping functions

“Escape” means “outlive the function in which the `lambda`

was evaluated.”

Typically returned

More rarely, stored in a global variable or a heap-allocated data structure

We have already seen an example:

Where are `n`

and `k`

stored???

**Values that escape have to be allocated on the heap**C programmers use

`malloc`

to explicitly manage such values.In a language with first-class, nested functions, storage of escaping values is part of the semantics of

`lambda`

.

Picture of activation record for `to-the-n-minus-k`

with `n`

and `k`

being popped.

An example:

### 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?)`

### 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)`

.

As we study higher-order functions in more detail, you will see why currying is useful.

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

### Your turn!!

## Bonus content: Lambda as an abstraction barrier

**Q**: What’s the problem with this approach?

**A**: The `seed`

is exposed to the end user, who can break the abstraction of the `rand`

function.

# 27 September 2017: Higher-order functions

There are PDF slides for 9/28/2017.

## Announcements

- Instructor Office Visits on Saturday (see Piazza)
- Scheme I HW due tonight
- Scheme II HW (HOFS) due 10/4

## Last Time

- Association lists [bonus]
- Let construct
- Anonymous functions

## Today

- Reasoning about Functions
- Useful Higher-Order Functions
- Tail Calls

## Reasoning about code

### Reasoning principle for lists

Recursive function that consumes *A* has the same structure as a 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’s

### Reasoning principle for functions

Q: Can you do case analysis on a function?

A: No!

Q: So what can you do then?

A: Apply it!

Q: How to prove two

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

## Higher-Order Functions

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`

, or a “catamorphism”

### List search: `exists?`

Algorithm encapsulated: linear search

Example: Is there a 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
```

### Your turn: Does everything match: `all?`

Example: Is every element in a list even?

Algebraic laws:

```
(all? p? '()) == ???
(all? p? '(cons a as)) == ???
(all? p? '()) == #t
(all? p? '(cons a as)) == p? x and all? p? xs
```

### List selection: `filter`

Algorithm encapsulated: Linear filtering

Example: Given a list of numbers, return only the even ones.

Algebraic laws:

```
(filter p? '()) == ???
(filter p? '(cons m ms)) == ???
(filter p? '()) == '()
(filter p? '(cons m ms)) == if (p? m)
(cons m (filter p? ms))
(filter p? ms)
```

### “Lifting” functions to lists: `map`

Algorithm encapsulated: Transform every element

Example: **Square every element of a list.**

Algebraic laws:

```
(map f '()) == ???
(map f (cons n ns)) == ???
(map f '()) == '()
(map f (cons n ns)) == cons (f n) (map f ns)
```

### 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: Folding `combine?`

## Tail calls

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

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

Question: Why can’t we do this same optimization on `reverse`

?

Answer: `reverse`

has to do further computation with results of recursive calls, so can’t eliminate the stack frame until later.

Answer: a **goto**!!

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

# 2 October 2017: Continuations

There are PDF slides for 10/3/2017.

## Last Time

- Reasoning about functions

- Higher-order functions
`exists?`

`all?`

`filter`

`map`

`fold`

- Tail calls

## Announcements

- Scheme II HW (HOFs) due Wednesday 10/4

## Today

- Continuations

## Continuations

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” a value to a *continuation.*

### Uses of continuations

Call-backs in GUI frameworks

A style of coding that can mimic

*exceptions*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`

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

### 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

## Extended Example: A SAT Solver

### 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`

cotinuation 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

These diagrams (and the corresponding code) **compose**!

### 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.

# 4 October 2017: Scheme Semantics

There are PDF slides for 10/5/2017.

## Announcements

If you can, bring your laptop to this week’s recitation.

Scheme HW II (hofs) due tonight.

Scheme HW III (continuations and semantics) due on

**Monday 10/16**.

## Today

Scheme Semantics

Stores

Lambdas evaluate to closures

Application

## Last Time

- Continuations
- “gotos with arguments”
- Example: Handling missing values (association list)
- Example: Structuring a search (SAT solver)

## New Syntax, Values, Environments, and Evaluation Rules

First four of five questions: Syntax, Values, Environments, Evaluation

Key changes from Impcore:

- New constructs:
**let**,**lambda**,**application**(not just named functions)

New values:

`cons`

cells and*functions*(closures)A

**single**kind of environmentEnvironment maps names to mutable

*locations*, not values.A

**store**maps locations to values.Environments get

**copied**(in closures).

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.

The book includes all rules for uScheme. Here we will discuss on key rules.

### Variables

Board: Picture of environment pointing to store.

Questions about Assign:

What changes are captured in

*σ*′?What changes are captured in

*σ*′{ℓ↦*v*}?What would happen if we used

*σ*instead of*σ*′What would happen if we used a fresh ℓ?

Some other ℓ in the range of

*ρ*?

### Lambdas

### Function Application

**Question:** Which `even`

is referenced when `f`

is called?

**Answer:** With static scoping, it’s the predicate. With dynamic scoping it’s the one bound to 3.

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}, …, ℓ_{n}∉ dom(*σ*)?What is the relationship between

*ρ*and*σ*?

Picture of environment and store that results from executing above program.

Closure Optimizations

- Major issue in making functional programs efficient
- Keep closures on the stack
- Share closures
- Eliminate closures (when functions don’t escape)

# 11 October 2017: Scheme Wrap-up; ML Intro

There are PDF slides for 10/12/2017.

## Announcements

## Today

- Scheme Wrap-up
- Intro to ML

## Last Time

Scheme semantics

Single kind of environment that maps names to locations.

A

*store*maps locations to values.Functions & Closures

Application

### Lets

Which `let`

is which and why?

Three versions of `let`

:

`let`

puts the new bindings in scope only for the body expression.`let*`

adds each binding one at a time, so each binding is in scope for the later ones.`letrec`

considers all the bindings to be mutually recursive.

## 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

## Introduction to ML

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

Lectures on ML:

- Algebraic types and pattern matching
- Exceptions
- An introduction to types

**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 + exceptions + static types

### uScheme -> 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.
- 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.

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

# 16 Oct 2017: Programming with constructed data and types

There are PDF slides for 10/17/2017.

## Announcements

Continuations HW due tonight

ML homework is now available. Due 10/25.

## Today

- Datatypes
- Types, Patterns, Exceptions
- ML Traps & Pitfalls

## Last Time

Semantics of let

Scheme wrap up

Introduction to ML: functions and patterns

## 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 data types

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

## Algebraic Datatypes

### Enumerated types

Datatypes can define an enumerated type and associated values.

`datatype suit = heart | diamond | spade | club`

Here `suit`

is the name of a new type.

The data constructors `heart`

, `dimaond`

, `spade`

, and `club`

are the values of type `suit`

.

Data constructors are separated by vertical bars.

### Pattern matching

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

```
fun toString heart = "heart"
| toString diamond = "diamond"
| toString spade = "spade"
| toString club = "club"
val suitName = toString heart
```

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

`datatype IntTree = Leaf | Node of int * IntTree * IntTree`

`IntTree`

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, `IntTree`

).

### Building values with constructors

We build values of type `IntTree`

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 = preOrder t3
```

`IntTree`

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 **data 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.

## Things to notice about datatypes

### Environments

Datatype declarations introduce names into:

the type environment:

`suit`

,`IntTree`

,`tree`

the value environment:

`heart`

,`Leaf`

,`Parent`

### Inductive

Datatype declarations are inherently **inductive**:

the type

`IntTree`

appears in its own definitionthe type

`tree`

appears in its own definition

### Datatype Exercise

## Case expressions: How we use datatypes

## Bonus: 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”

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

## Tuple Pattern Matching

```
val (x,y) = (1,2)
val (left, pivot, right) = split xs
val (n,xs) = (3, [1,2,3])
val (x::xs) = [1,2,3]
val (_::xs) = [1,2,3]
```

## Exceptions: Handling unusual circumstances

### Syntax:

- Declaration:
`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

# 18 October 2017: Types

There are PDF slides for 10/19/2017.

## Announcements

- Handout (slides from today)

## Today

Type systems

Typing rules for a simple language

Type checker for a simple language

Adding environments

## Type systems

What kind of value do we have?

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 that 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 generally cannot answer:

Will my program contain a division by zero?

Will my program contain an array bounds error?

Will my program take the

`car`

of `’()?Will my program terminate?

### Decidability and Type Checking

Suppose L is a “Turing-Complete” Language.

TP is the set of programs in L that terminate.

Wish: a type system to statically classify terminating programs:

Expression e in L has type T (e : T) iff e terminates.

But: Undecideable!

We can prove no such type system exists.

Choices:

Allow type checker to run forever.

Don’t use type system to track termination.

### Static vs. Dynamic Type Checking

Most languages use a combination of **static** and **dynamic** checks

Static: “for all inputs”

input independent

efficient at run-time

approximate : rules out some programs that won’t trigger errors example:

`(if false then 2 else "hi") ^ "there"`

Dynamic: “for some inputs”

depends on input

run-time overhead

precise

## Type System and Checker for a Simple Language

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)

Inference rules determine how to write type checker

`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
```

Experience shows it is better to test two types for equivalence than to write rule with same type appearing twice.

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?

Working definition: a

*set of values*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)

## 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`

.

## Typing Rules: Contexts and Term Variables

Add variables and `let`

binding to our language, what happens?

What could go wrong with a variable?

Used inconsistently:

;; x can’t be both an integer and a list

x + x @ x

;; y can’t be both an integer and a string

let y = 10 in y ^ “hello” end

Need to track variable use to ensure consistency

Key idea: **Type environment** (Gamma) tracks the types of variables.

### Rule for var

```
x in domain 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'
```

### Type Checker

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

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

Review

I gave you syntax for simple language

You came up with typing rules

I showed you how to implement the type checker.

Then on your 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.**

# 23 October 2017: Type Checking with Type Constructors

There are PDF slides for 10/24/2017.

## Announcements

Continuation HW returned

Midterm: Wednesday Nov. 1 in class; 1-page self-prepared sheet of notes

## Last Time

What are types?

Undecideability

Static vs. Dynamic types

Typing Rules

Type Checker

Type environment

## Today

Type checking with type constructors

Formation, Introduction, and Elimination Rules

## Functions

Introduction:

```
Gamma{x->tau1} |- e : tau2
------------------------------------------------------------
Gamma |- fn x : tau1 => e : tau1 -> tau2
```

Elimination:

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

## 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.

## Monomorphic vs Polymorphic Types

Monomorphic types have “one shape.”

- Examples:
`int`

,`bool`

,`int -> bool`

,`int * int`

Polymorphic types have “many shapes.”

- Examples:
`'a list`

,`'a list -> 'a list`

,`('a * int)`

## Design and implementation of monomorphic languages

Mechanisms:

Every new variety of type requires

**special syntax**Implementation is a straightforward application of what you already know.

Language designer’s process when adding new kinds of types:

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.

Question: 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`

)