# Photos from Lecture

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

# 16 January 2019: Introduction to Comp 105

There are PDF slides for 1/17/2019.

Handout: 105 Tip Sheet

Handout: 105 Syllabus

Handout: Experiences of successful 105 students

Handout: Lessons in program design

Handout: Design checklists

Handout: Homework (photograph, due Jan 22)

Handout: Homework (Impcore, due Jan 29)

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

### Introduction

My pronouns are he, him, his.

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

## Why we are here

• Write code from scratch
• In a language you’ve never seen
• That sails past code review

What it involves:

• Programming practice (emphasize widely used features: functions, types, modules, objects)
• Mathematical description (how things work, see patterns)
(Example: see patterns of recursion in homework)

Today:

• Then a little about experience and expectations

## What is a programming language?

What is a PL? Think. Then pair. Then share.

First three classes: 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

### Value structure: induction again

In-class exercise: inductive definition of natural number

• Again, there is more than one
• What makes it easy to know meaning of numerals?

## Writing code with recursion and induction

Data-driven design process. Connections to design ideas from 1970s, 1980s, 1990s, plus test-driven development (2000s).

Recursive-function problem

Exercise: all-fours?

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

Key design step: form of number

Choose inductive structure for natural numbers:

• Which case analysis do we want?

Step 1: Forms of DECNUMERAL proof system (1st lesson in program design):

• Either a single digit d
• Or 10 × m + d, where m ≠ 0

Example inputs

Step 2:

• Single digits: 4, 9

• Multi-digits: 44, 907, 48

Function’s name and contract

Steps 3 and 4:

Function (all-fours? n) returns nonzero if and only if the decimal representation of n can be written using only the digit 4.

Example results

Step 5: write expected results as unit tests:

(check-assert      (all-fours?  4))
(check-assert (not (all-fours?  9)))
(check-assert      (all-fours? 44))
(check-assert (not (all-fours? 48)))
(check-assert (not (all-fours? 907)))

Algebraic laws

Step 6: Generalize example results to arbitrary forms of data

(all-fours? d) ==  (= d 4)

(all-fours? (+ (* 10 m) d)) ==
(= d 4) && (all-fours? m)

Left-hand sides turn into case analysis

Step 7:

; (all-fours? d) == ...
; (all-fours? (+ (* 10 m) d)) ==  ...

(define all-fours? (n)
(if (< n 10)
... case for n = d ...
... case for n = (+ (* 10 m) d),
so m = (/ n 10) and
d = (mod n 10) ...))

Each right-hand side becomes a result

Step 8:

; (all-fours? d) ==  (= d 4)
; (all-fours? (+ (* 10 m) d)) ==
;           (= d 4) && (all-fours? m)

(define all-fours? (n)
(if (< n 10)
(= n 4)
(and (= 4 (mod n 10))
(all-fours? (/ n 10)))))

Revisit tests:

Step 9:

(check-assert      (all-fours?  4))
(check-assert (not (all-fours?  9)))
(check-assert      (all-fours? 44))
(check-assert (not (all-fours? 907)))

(check-assert (not (all-fours? 48)))

Checklist:

• For each form of data, one true and one false
• One extra corner case (partly fours)
• Tests pass

## Syntax in programming languages

### Concrete Syntax

Programming-languages people are wild about compositionality.

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

• Example: expressions, e1 + e2

### Syntactic structure of Impcore

Watch for syntactic categories, syntactic composition

Our common framework

Goal: eliminate superficial differences

• Makes comparisons easy
• Differences that remain must be important!

No new language ideas.

Imperative programming with an IMPerative CORE:

• Has features found in most languages
(loops and assignment)

• Trivial syntax (from LISP)

Idea of LISP syntax

Parenthesized prefix syntax:

• Names and numerals are basic atoms

• Other constructs bracketed with () or [] (Possible keyword after opening bracket)

Examples:

(+ 2 2)
(if (isbound? x rho) (lookup rho x) (error 99))

(For now, we use just the round brackets)

Impcore structure

Two syntactic categories: expressions, definitions

No statements!—expression-oriented

(if e1 e2 e3)
(while e1 e2)
(set x e)
(begin e1 ... en)
(f e1 ... en)

Evaluating e has value, may have side effects

Functions f named (e.g., + - * / = < > print)

The only type of data is “machine integer” (deliberate oversimplification)

Syntactic structure of Impcore

An Impcore program is a sequence of definitions

(define mod (m n) (- m (* n (/ m n))))

Compare

int mod (int m, int n) {
return m - n * (m / n);
}

Impcore variable definition

Example

(val n 99)

Compare

int n = 99;

Example function shows every form

(define even? (n) (= (mod n 2) 0))

(define 3n+1-sequence (n) ; from Collatz
(begin
(while (!= n 1)
(begin
(println n)
(if (even? n)
(set n (/ n 2))
(set n (+ (* 3 n) 1)))))
n))


### Live coding in Impcore

Try square function. E.g., (square (+ 2 2))

# 23 January 2019: Abstract syntax and operational semantics

There are PDF slides for 1/24/2019.

Handout: 105 Impcore Semantics, Part 1

## Live coding: Impcore

All fours, tests, big literals

square, negated, interactive check-expect

## Review: algebraic laws

(power x 0)       == 1
(power x (+ n 1)) == (* (power x n) x)

(power x 0)             == 1
(power x (+ (* 2 m) 0)) == (square (power x m))
(power x (+ (* 2 m) 1)) == (* x (square (power x m)))

(all-fours? d)              ==  (= d 4), [d is digit]
(all-fours? (+ (* 10 m) d)) ==
(and (= d 4) (all-fours? m)), where m != 0

(has-digit? d d)   == 1
(has-digit? d d')  == 0, where d differs from d'
(has-digit? (+ (* 10 m) d) d') ==
(or (= d d') (has-digit? m d')), where m != 0


## Approaching 105

100-level course

Responsibility for your own learning: lecture is the tip of the iceberg

Announcement: Syllabus scavenger hunt (participation grades)

Systematic programming process: we can’t observe process, but it will affect your time spent by a factor of 2, 3, or 4.

Awareness of your own learning: Metacognition

### Office hours

Students: go to office hours! An idle TA is an unhappy TA.

## Review

Short discussion: One thing you learned in the first class

Language: syntax, rules/organization/grammar

Programming language: you can run it (values)

## Preparing for a language you’ve never seen before

You need a vocabulary. It will involve math.

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

Bloom’s taxonomy (Metacognition 10)

Cognitive actions:

1. Remember
2. Understand
3. Apply
4. Analyze
5. Evaluate
6. Create

Operational semantics

Cognitive actions:

1. Remember
2. Understand
3. Apply
4. Analyze
5. Evaluate
6. Create

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

• How many different kinds of things can be composed: syntactic categories
                                C/C++  Impcore

Compute w/ existing names
- value and behavior           exp     exp
- just behavior                stm

- initialized                  def     def
- uninitialized                decl

Example rules of composition:

• C/C++: expressions, definitions, statements

• Impcore

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

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

Concrete syntax for Impcore

Definitions and expressions:

How to define behaviors inductively

Expressions only

Base cases (plural): numerals, names

Inductive steps: compound forms

• To determine behavior of a compound form, look at behaviors of its parts

First, simplify the task of specification

What’s different? What’s the same?

 x = 3;               (set x 3)

while (i * i < n)    (while (< (* i i) n)
i = i + 1;            (set i (+ i 1)))

Abstract away gratuitous differences

(See the bones beneath the flesh)

Abstract syntax

Same inductive structure as BNF grammar
(related to proof system)

More uniform notation

Good representation in computer

Concrete syntax: sequence of symbols

Abstract syntax: ???

The abstraction is a tree

The abstract-syntax tree (AST):

Exp = LITERAL (Value)
| VAR     (Name)
| SET     (Name name, Exp exp)
| IFX     (Exp cond, Exp true, Exp false)
| WHILEX  (Exp cond, Exp exp)
| BEGIN   (Explist)
| APPLY   (Name name, Explist actuals)

One kind of “application” for both user-defined and primitive functions.

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

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

In C, trees are fiddly

typedef struct Exp *Exp;
typedef enum {
LITERAL, VAR, SET, IFX, WHILEX, BEGIN, APPLY
} Expalt;        /* which alternative is it? */

struct Exp {  // only two fields: 'alt' and 'u'!
Expalt alt;
union {
Value literal;
Name var;
struct { Name name; Exp exp; } set;
struct { Exp cond; Exp true; Exp false; } ifx;
struct { Exp cond; Exp exp; } whilex;
Explist begin;
struct { Name name; Explist actuals; } apply;
} u;
};

Let’s picture some trees

An expression:

  (f x (* y 3))

(Representation uses Explist)

A definition:

  (define abs (n)
(if (< n 0) (- 0 n) n))

## Key question: names (review)

### From ASTs to behaviors

Behaviors of ASTs, part I: Atomic forms

Numeral: stands for a value

Name: stands for what?

Environment’’ is pointy-headed theory

You may also hear:

• Symbol table
• Name space

Influence of environment is “scope rules”

• In what part of code does environment govern?

Find behavior using environment

Recall

  (* y 3)   ;; what does it mean?

Impcore uses three environments

Global variables ξ

Functions ϕ

Formal parameters ρ

There are no local variables

• Just like awk; if you need temps, use extra formal parameters
• For homework, you’ll add local variables

Function environment ϕ not shared with variables—just like Perl

# 28 January 2019: Judgments and Rules

There are PDF slides for 1/29/2019.

Students: Take a blank white card

Handout: Redacted Impcore rules

Today:

1. How do we know what happens when we run the code?

• Judgment
• Rules
• Valid derivations
2. What can we prove about it?

• Metatheory

## Review: environments

Find behavior using environment

Recall

  (* y 3)   ;; what does it mean?

Impcore uses three environments

Global variables ξ (“ksee”)

Functions ϕ (“fee”)

Formal parameters ρ (“roe”)

There are no local variables

• Just like awk; if you need temps, use extra formal parameters
• For homework, you’ll add local variables

Function environment ϕ not shared with variables—just like Perl

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

Which correctly describes what happens at run time?

1. (+ 2 2), ξ, ϕ, ρ⟩ ⇓ ⟨4, ξ, ϕ, ρ

2. (+ 2 2), ξ, ϕ, ρ⟩ ⇓ ⟨99, ξ, ϕ, ρ

3. (+ 2 2), ξ, ϕ, ρ⟩ ⇓ ⟨0, ξ, ϕ, ρ

4. (while 1 0), ξ, ϕ, ρ⟩ ⇓ ⟨77, ξ, ϕ, ρ

5. (begin (set n (+ n 1)) 17)ξ, ϕ, ρ
⇓ ⟨17, ξ, ϕ, ρ

To know for sure, we need a proof

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

1. In the body of digit?, what expressions are evaluated in what order?

2. As a function application, the body matches template (f e1 e2). In this example,

• What is f?
• What is e1?
• What is e2?

Let’s develop the ApplyUser rule for the special case of two arguments: APPLY(f, e1, e2), ξ, ϕ, ρ⟩ ⇓ ?

What is the result of (digit? 7)?

How do we know it’s right?

## From rules to proofs

Judgment speaks truth when derivable’’

Special kind of proof: derivation

• It’s a data structure (derivation tree)
• Made inductively, by composing rules
• Valid derivation matches rules (by substitution)
• Spacelike representation of timelike behavior (think flip-book animation)

A form of “syntactic proof”

Recursive evaluator travels inductive proof

Root of derivation at the bottom (surprise!)

Build

• Start on the left, go up
• Cross the
• Finish on the right, go down

The Tony Hawk’’ algorithm

First let’s see a movie

# 30 January 2019: Derivations, metatheory, better semantics

There are PDF slides for 1/31/2019.

## Review: Derivations

Judgment speaks truth when derivable’’

Special kind of proof: derivation

• It’s a data structure (derivation tree)
• Made inductively, by composing rules
• Valid derivation matches rules (by substitution)
• Spacelike representation of timelike behavior (think flip-book animation)

A form of “syntactic proof”

Valid derivation

Initial state partially or fully known

Final state determined by initial state (homework)

Every node in tree is an instance of some rule

No primes!

• Substitute known subexpressions for e1, …
• Substitute known results for ξ, ρ

Recursive evaluator travels inductive proof

Root of derivation at the bottom (surprise!)

Build

• Start on the left, go up
• Cross the
• Finish on the right, go down

The Tony Hawk’’ algorithm

First let’s see a movie

### Building derivations

Syntactic proofs empower meta reasoning

Proof 𝒟 is a data structure

Got a fact about all proofs?

• It’s a fact about all terminating evaluations
• They are 1 to 1

Prove facts by structural induction over derivations

• (Or “induction on height of derivation tree”)

Example: evaluating an expression doesn’t create or destroy any global variables (the set of defined global variables is invariant)

Metatheorems often help implementors

More example metatheorems:

• OK to mutate environments if you use a stack
• Interactive browser doesn’t leak space (POPL 2012)
• Device driver can’t harm kernel (Microsoft Singularity)

Metatheorems are proved by induction

Induction over structure (or height) of derivation trees 𝒟

These are “math-class proofs” (not derivations)

Proof

• Has one case for each rule

• Has multiple cases for some syntactic forms

• Assumes the induction hypothesis for any proper sub-derivation (derivation of a premise)

Let’s try it!

Cases to try:

• Literal
• GlobalVar
• SetGlobal
• IfTrue
• ApplyUser2

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

# 4 February 2019: Scheme

There are PDF slides for 2/5/2019.

### Announcements

Note: course not graded on a curve

Scheme homework:

• ramp-up
• not frightfully hard concepts, but…

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

Today: programming with lists and S-expressions (around laws)

## For a new language, five powerful questions

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

1. What is the abstract syntax? What are the syntactic categories, and what are the forms in each category?

2. What are the values? What do expressions/terms evaluate to?

3. What environments are there? That is, what can names stand for?

4. How are terms evaluated? What are the judgments? What are the evaluation rules?

5. What’s in the initial basis? Primitives and otherwise, what is built in?

(Initial basis for μScheme on page 159)

## Introduction to Scheme

Two new kinds of data:

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

• Pointer to automatically managed cons cell (mother of civilization)

### Scheme Values

Most values are S-expressions.

An fully general S-expression is one of

• a symbol 'Halligan 'tufts

• a literal integer 0 77

• a literal Boolean #t #f

• (cons v1 v2), where v1 and v2 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 vs), where v is an S-expression and vs is a list of S-expressions

We say “an S-expression followed by a list of S-expressions”

## Programming with lists and S-expressions

### Lists: A 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)

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?

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

### Programming example: lists of numbers

Problem-solving: students pose problem on list of numbers

Lists generalized: S-expressions

An ordinary S-expression is one of:

• An atom (symbol, number, Boolean)
• A list of ordinary S-expressions

Can write literally in source, with quote

## μScheme’s new syntax

### Immutable data structures

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

### List-design shortcuts

Three forms of “followed by”

• Given: Element .. list of values = (cons x xs)

• Define: List of values .. list of values = (append xs ys)

• Ignore: List of values .. element = (snoc xs y)
Or (append xs (list1 y))

Two lists? Four cases!

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

Equations and function for append

(append '()         ys) == ys

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

(define append (xs ys)

(if (null? xs)

ys

(cons (car xs) (append (cdr xs) 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:

1. IH (’())

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

## Costs of list reversal

Algebraic laws for list reversal:

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

And the code?

Naive list reversal

(define reverse (xs)
(if (null? xs)
'()
(append (reverse (cdr xs))
(list1 (car xs)))))


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(n2) 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?

Reversal by accumulating parameters

(define revapp (xs ys)
; return (append (reverse xs) ys)
(if (null? xs)
ys
(revapp (cdr xs)
(cons (car xs) ys))))

(define reverse (xs) (revapp xs '()))


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.

A-list example

    -> (find 'Building
'((Course 105) (Building Barnum)
(Instructor Ramsey)))
Barnum
-> (val nr (bind 'Office 'Halligan-222
(bind 'Courses '(105 150TW)
(Courses (105 150TW))
(Office Halligan-222))
-> (find 'Office nr)
Halligan-222
-> (find 'Favorite-food nr)
()


Notes:

• attribute can be a list or any other value

### Algebraic laws of association lists

Laws of association lists

(find k (bind k  v a-l)) = v
(find k (bind k' v a-l)) = (find k a-l), provided k != k'
(find k '()) =  '() --- bogus!


# 6 Feb 2019: First-class and higher-order functions

There are PDF slides for 2/7/2019.

## Skills refresh

Refresh: Complete these laws

(append '()         zs) == ...
(append (cons y ys) zs) == ...

(reverse '())         == ...
(reverse (cons y ys)) == ...


Refresh: Complete these laws

Waiting…

Refresh: Complete these laws

(append '()         zs) == zs
(append (cons y ys) zs) == (cons y (append ys zs))

(reverse '())         == '()
(reverse (cons y ys)) == (append (reverse ys)
(list1 y))


## Where we’ve been and where we’re going: Functional programming

Last time: new data forms (lists, S-expressions)

Today: New syntax, its rules and values

Context: Techniques and features we’re learning fit under functional programming.

• Idea: reuse more code because of “better glue”

Already doing it: immutable data (append)

• Always safe to share data (I can’t mess up things for you)
• Perfect for parallel/distributed (think Erlang)
• Perfect for web (JSON, XML)

Next up: better ways of gluing functions together

## μScheme’s semantics

Impcore: Things that should offend you

Look up function vs look up variable:

• Different interfaces!

To get variable, check multiple environments

Create a function? Must give it a name

• A sign of second-class citizenship

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.

### New syntax exploits semantics

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:

So let’s see that semantics!

Key idea: don’t worry about memory

## From Impcore to uScheme: 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:

Function escapes!

-> (define to-the-n-minus-k (n k)
(let
([x-to-the-n-minus-k (lambda (x)
(- (exp x n) k))])
x-to-the-n-minus-k))
-> (val x-cubed-minus-27 (to-the-n-minus-k 3 27))
-> (x-cubed-minus-27 2)
-19


The function to-the-n-minus-k is a higher-order function because it returns another (escaping) function as a result.

No need to name the escaping function

-> (define to-the-n-minus-k (n k)
(lambda (x) (- (exp x n) k)))

-> (val x-cubed-minus-27 (to-the-n-minus-k 3 27))
-> (x-cubed-minus-27 2)
-19


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

The zero-finder

(define findzero-between (f lo hi)
; binary search
(if (>= (+ lo 1) hi)
hi
(let ([mid (/ (+ lo hi) 2)])
(if (< (f mid) 0)
(findzero-between f mid hi)
(findzero-between f lo mid)))))
(define findzero (f) (findzero-between f 0 100))


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:

Cube root of 27 and square root of 16

-> (findzero (to-the-n-minus-k 3 27))
3
-> (findzero (to-the-n-minus-k 2 16))
4


Lambda questions

(define combine (p? q?)
(lambda (x) (if (p? x) (q? x) #f)))

(define divvy (p? q?)
(lambda (x) (if (p? x) #t (q? x))))

(val c-p-e (combine prime? even?))
(val d-p-o (divvy   prime? odd?))

(c-p-e 9) == ?            (d-p-o 9) == ?
(c-p-e 8) == ?            (d-p-o 8) == ?
(c-p-e 7) == ?            (d-p-o 7) == ?


(define combine (p? q?)
(lambda (x) (if (p? x) (q? x) #f)))

(define divvy (p? q?)
(lambda (x) (if (p? x) #t (q? x))))

(val c-p-e (combine prime? even?))
(val d-p-o (divvy   prime? odd?))

(c-p-e 9) == #f           (d-p-o 9) == #t
(c-p-e 8) == #f           (d-p-o 8) == #f
(c-p-e 7) == #f           (d-p-o 7) == #t


## How lambda works

### Rule for lambda

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

### Rule for function Application

• What if we used σ instead of σ0 in evaluation of e1?

• 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 σ?

# 11 Feb 2019: Vocabulary building: List HOFs, the function factory

There are PDF slides for 2/12/2019.

Today: Using lambda to enlarge your vocabulary

• List computations
• Cheap functions from other functions

## Higher-Order Functions on lists

Today: both functions and lists

Algorithms on linked lists (or arrays in sequence):

• Search for an element
• What else?

Predefined list algorithms

Some classics:

• exists? (Example: Is there a number?)
• all?    (Example: Is everything a number?)
• filter  (Example: Select only the numbers)
• map     (Example: Add 1 to every element)
• foldr   (Visit every element)

Fold also called reduce, accum, a “catamorphism”

Live coding interlude

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

Defining exists?

; (exists? p? '())         = #f
; (exists? p? (cons y ys)) = #t,          if (p? y)
; (exists? p? (cons y ys)) = (exists? p? ys),
otherwise
-> (define exists? (p? xs)
(if (null? xs)
#f
(if (p? (car xs))
#t
(exists? p? (cdr xs)))))
-> (exists? symbol? '(1 2 zoo))
#t
-> (exists? symbol? '(1 2 (zoo)))
#f


### List selection: filter

Defining filter

; (filter p? '()) == '()
; (filter p? (cons y ys)) ==
;         (cons y (filter p? ys)), when (p? y)
; (filter p? (cons y ys)) ==
;         (filter p? ys), when (not (p? y))

-> (define filter (p? xs)
(if (null? xs)
'()
(if (p? (car xs))
(cons (car xs) (filter p? (cdr xs)))
(filter p? (cdr xs)))))


Running filter

-> (filter (lambda (n) (>  n 0)) '(1 2 -3 -4 5 6))
(1 2 5 6)
-> (filter (lambda (n) (<= n 0)) '(1 2 -3 -4 5 6))
(-3 -4)
-> (filter ((curry <)  0) '(1 2 -3 -4 5 6))
(1 2 5 6)
-> (filter ((curry >=) 0) '(1 2 -3 -4 5 6))
(-3 -4)


### “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     add3 '(1 2 3 4 5))
(4 5 6 7 8)

;; (map f '())         =
;; (map f (cons y ys)) =



-> (map     add3 '(1 2 3 4 5))
(4 5 6 7 8)

; (map f '())         ==  '()
; (map f (cons y ys)) ==  (cons (f y) (map f ys))


Defining and running map

; (map f '())         == '()
; (map f (cons y ys)) == (cons (f y) (map f ys))
-> (define map (f xs)
(if (null? xs)
'()
(cons (f (car xs)) (map f (cdr xs)))))
-> (map number? '(3 a b (5 6)))
(#t #f #f #f)
-> (map *100 '(5 6 7))
(500 600 700)


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

## One-argument functions: Curry and compose

Build one-argument functions from two-argument functions

The idea of currying

-> (map     ((curry +) 3) '(1 2 3 4 5))
; add 3 to each element

-> (exists? ((curry =) 3) '(1 2 3 4 5))
; is there an element equal to 3?

-> (filter  ((curry >) 3) '(1 2 3 4 5))
; keep elements that 3 is greater then


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.

To get one-argument functions: Curry

-> (val positive? (lambda (y) (< 0 y)))
-> (positive? 3)
#t
-> (val <-c (lambda (x) (lambda (y) (< x y))))
-> (val positive? (<-c 0)) ; "partial application"
-> (positive? 0)
#f


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

### Currying and list HOFs

-> (map     ((curry +) 3) '(1 2 3 4 5))
???
-> (exists? ((curry =) 3) '(1 2 3 4 5))
???
-> (filter  ((curry >) 3) '(1 2 3 4 5))
???                        ; tricky


-> (map     ((curry +) 3) '(1 2 3 4 5))
(4 5 6 7 8)
-> (exists? ((curry =) 3) '(1 2 3 4 5))
#t
-> (filter  ((curry >) 3) '(1 2 3 4 5))
(1 2)


### One-argument functions compose

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

One-argument functions compose

-> (define o (f g) (lambda (x) (f (g x))))
-> (define even? (n) (= 0 (mod n 2)))
-> (val odd? (o not even?))
-> (odd? 3)
#t
-> (odd? 4)
#f


Another example: (o not null?)

# 13 Feb 2019: Tail calls and continuations

There are PDF slides for 2/14/2019.

Announcement: late homework

• 2, 3, 4 hours late == unfair

Announcement: recitations next week

• Thursday is Monday schedule, will have lecture
• Opportunity for make-up recitation Wednesday, Saturday

Where have we been, where are we going: functions

Today: proofs, costs, control flow

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’s

• Q: How to prove two functions equal?

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

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

What is tail position?

Tail position is defined inductively:

• The body of a function is in tail position
• When (if e1 e2 e3) is in tail position, so are e2 and e3
• When (let (...) e) is in tail position, so is e, and similary for letrec and let*.
• When (begin e1 ... en) is in tail position, so is en.

Idea: The last thing that happens

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

## Tail calls and the method of accumulating parameters

Write laws for

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

Reversal by accumulating parameters

Moves recursive call to tail position

Contract:

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

Laws:

  (revapp '()         ys) == ys
(revapp (cons z zs) ys) ==
(revapp zs (cons z ys))

Who could write the code?

Reversal by accumulating parameters

; laws: (revapp '()         ys) = ys
;       (revapp (cons z zs) ys) =
;                     (revapp zs (cons z ys))

(define revapp (xs ys)
; return (append (reverse xs) ys)
(if (null? xs)
ys
(revapp (cdr xs)
(cons (car xs) ys))))

(define reverse (xs) (revapp xs '()))


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

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)

Are tail calls familiar?

In your past, what did you call a construct that

1. Transfers control to a point in the code?

2. Uses no stack space?

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

But goto is limited to labels named in the code.

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”

## Continuations

### 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. For us, tail call to a parameter.

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

• Event loops in game programming and other concurrent settings

• Even web services!

### Implementation

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

• First-class continuations require compiler support: primitive function that materializes “current continuation” into a variable. (Missing chapter number 3.)

## Motivating Example: From existence to witness

Ideas?

• nil
• special symbol 'fail
• run-time error

Good choice:

• exception (not in uScheme)

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

Example Use: Instructor Lookup

-> (val 2016f '((Fisher 105)(Hescott 170)(Chow 116)))
-> (instructor-info 'Fisher 2016f)
(Fisher teaches 105)
-> (instructor-info 'Chow 2016f)
(Chow teaches 116)
-> (instructor-info 'Souvaine 2016f)
(Souvaine is-not-on-the-list)


# 20 Feb 2019: Continuations for backtracking

There are PDF slides for 2/21/2019.

Expressions to avoid

(if <p> #t #f)  ; worst

(append (list1 <x>) <ys>) ; most common

(cons <x> (cons <y> '())) ; prefer list2

Functions list-of, formula?

• Can be passed any value

• Must handle all cases (Figure 2.1, page 95)

Homework: Solving Boolean formulas

A formula is one of these:

In context of:

(val f1 (make-and (list4 'x 'y 'z (make-not 'x))))
; x /\ y /\ z /\ !x

(val f2 (make-not (make-or (list2 'x 'y))))
; !(x \/ y)

(val f3 (make-not (make-and (list3 'x 'y 'z))))
; !(x /\ y /\ z)


Satisfying assignments

(val f1 (make-and (list4 'x 'y 'z (make-not 'x))))
; x /\ y /\ z /\ !x  ;; NONE

(val f2 (make-not (make-or (list2 'x 'y))))
; !(x \/ y)          ;; { x |-> #f, y |-> #f }

(val f3 (make-not (make-and (list3 'x 'y 'z))))
; !(x /\ y /\ z)     ;; { x |-> #f, ... }


### Search demo

Finding a satisfying assignment

Example formula:

  (x \/ y) /\ (!x /\ z)

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

; (satisfy-literal-true x current succ fail) =
;   (succ current fail), when x is bound to #t in cur
;   (fail),              when x is bound to #f in cur
;   (succ (bind x #t current) fail), x unbound in cur

(define satisfy-literal-true (x current succ fail)
(if (bound? x current)
(if (find x current)
(succ current fail)
(fail))
(succ (bind x #t current) fail)))


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

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

1. Solver enters A

2. If A is solved, newly allocated success continuation starts B

3. If B succeeds, we’re done! Use success continuation from context.

4. If B fails, use resume continuation A passed to B as fail.

5. If A fails, the whole thing fails. Use fail continuation from context.

### Solving A or B

1. Solver enters A

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

3. If A can’t be solved, don’t give up! Try a newly allocated failure continuation to start B.

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

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

6. If B fails, abject failure all around; call the original fail continuation.

## Lisp and Scheme Retrospective

Five powerful questions

1. What is the abstract syntax?
Syntactic categories? Terms in each category?

2. What are the values?
What do expressions/terms evaluate to?

3. What environments are there?
What can names stand for?

4. How are terms evaluated?
Judgments? Evaluation rules?

5. What’s in the initial basis?
Primitives and predefined, what is built in?

### Common Lisp, Scheme

• 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

1. Macros!
2. Cond expressions (solve nesting problem)
3. Mutation

### Macros!

Full Scheme: Macros

A Scheme program is just another S-expression

• Function define-syntax manipulates syntax at compile time

• Macros are hygienic—name clashes impossible

• let, &&, record, others implemented as macros

(See book sections 2.16, 2.17.4)

### Conditional expressions

Full Scheme: Conditionals

(cond [c1 e1]    ; if c1 then e1
[c2 e2]    ; else if c2 then e2
...            ...
[cn en])   ; else if cn then en

; Syntactic sugar---'if' is a macro:
(if e1 e2 e3) == (cond [e1 e2]
[#t e3])


### Mutation

Full Scheme: Mutation

Not only variables can be mutated.

Mutate heap-allocated cons cell:

(set-car! '(a b c) 'd)  => (d b c)

Circular lists, sharing, avoids allocation

• still for specialists only

# 21 Feb 2019: Introduction to ML

There are PDF slides for 2/22/2019.

Handout: Learning Standard ML

1. Remember
2. Understand
3. Apply
4. Analyze
5. Evaluate
6. Create

Ask the class: what are the strengths you found in μScheme programming? What are the pain points?

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

### ML forms of data

Live coding:

bool
string
int
list of int
list of bool
ill-typed list
pair
triple
function

More live coding:

sum of list of int (fold)
reverse (with fold)

Still more live coding? (New forms of data)

Ordinary S-expression
Binary tree of integers

Live coding memories:

(* list selection *)

fun nth ([],      0) = raise Subscript
| nth (y :: ys, 0) = y
| nth ([],      n) = raise Subscript
| nth (y :: ys, n) = nth (ys, n - 1)

(* better version: *)

fun nth ([],      _) = raise Subscript
| nth (y :: ys, 0) = y
| nth (y :: ys, n) = nth (ys, n - 1)

(* binary trees of integers *)
datatype itree
= LEAF
| NODE of itree * int * itree

(* val root : itree -> int option *)
(* if tree is not empty, returns value at root *)
fun root LEAF = NONE
| root (NODE (left, n, right)) = SOME n

(* testing code *)

(* val singleton : int -> itree
singleton n returns tree with n as its only node *)
fun singleton n = NODE (LEAF, n, LEAF)

val t35 = NODE (singleton 3, 5, LEAF)

val () =
Unit.checkExpectWith (Unit.optionString Int.toString)
"root of t35"
(fn () => root t35) (SOME 5)

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

1. Pattern matching is big and important. You will like it. It’s “coding with algebraic laws”
2. Exceptions are easy
3. 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

Length

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

val res = length [1,2,3]


Map

fun map f []      = []
| map f (x::xs) = (f x) :: (map f xs)

val res1 =
map length [[], [1], [1,2], [1,2,3]]


Map, without redundant parentheses

fun map f []      = []
| map f (x::xs) =  f x  ::  map f xs

val res1 =
map length [[], [1], [1,2], [1,2,3]]


Filter

fun filter pred []      = []
| filter pred (x::xs) =  (* no 'pred?' *)
let val rest = filter pred xs
in  if pred x then
(x :: rest)
else
rest
end

val res2 =
filter (fn x => (x mod 2) = 0) [1,2,3,4]


Filter, without redundant parentheses

fun filter pred []      = []
| filter pred (x::xs) =  (* no 'pred?' *)
let val rest = filter pred xs
in  if pred x then
x :: rest
else
rest
end

val res2 =
filter (fn x => (x mod 2) = 0) [1,2,3,4]


Exists

fun exists pred []      = false
| exists pred (x::xs) =
(pred x) orelse (exists pred xs)

val res3 =
exists (fn x => (x mod 2) = 1) [1,2,3,4]
(* Note: fn x => e is syntax for lambda *)


Exists, without redundant parentheses

fun exists pred []      = false
| exists pred (x::xs) =
pred x  orelse  exists pred xs

val res3 =
exists (fn x => (x mod 2) = 1) [1,2,3,4]
(* Note: fn x => e is syntax for lambda *)


All

fun all pred []      = true
| all pred (x::xs) =
(pred x) andalso (all pred xs)

val res4 = all (fn x => (x >= 0)) [1,2,3,4]


All, without redundant parentheses

fun all pred []      = true
| all pred (x::xs) =
pred x  andalso  all pred xs

val res4 = all (fn x => (x >= 0)) [1,2,3,4]


Take

exception TooShort
fun take 0 _       = []  (* wildcard! *)
| take n []      = raise TooShort
| take n (x::xs) = x :: (take (n-1) xs)

val res5 = take 2 [1,2,3,4]
val res6 = take 3 [1]
handle TooShort =>
(print "List too short!"; [])

(* Note use of exceptions. *)


Take, without redundant parentheses

exception TooShort
fun take 0 _       = []  (* wildcard! *)
| take n []      = raise TooShort
| take n (x::xs) = x ::  take (n-1) xs

val res5 = take 2 [1,2,3,4]
val res6 = take 3 [1]
handle TooShort =>
(print "List too short!"; [])

(* Note use of exceptions. *)


Drop

fun drop 0 zs      = zs
| drop n []      = raise TooShort
| drop n (x::xs) = drop (n-1) xs

val res7 = drop 2 [1,2,3,4]
val res8 = drop 3 [1]
handle TooShort =>
(print "List too short!"; [])


Takewhile

fun takewhile p [] = []
| takewhile p (x::xs) =
if p x then (x :: (takewhile p xs))
else []

fun even x = (x mod 2 = 0)
val res8 = takewhile even [2,4,5,7]
val res9 = takewhile even [3,4,6,8]


Takewhile, without redundant parentheses

fun takewhile p [] = []
| takewhile p (x::xs) =
if p x then  x ::  takewhile p xs
else []

fun even x = (x mod 2 = 0)
val res8 = takewhile even [2,4,5,7]
val res9 = takewhile even [3,4,6,8]


Dropwhile

fun dropwhile p []              = []
| dropwhile p (zs as (x::xs)) =
if p x then (dropwhile p xs) else zs
val res10 = dropwhile even [2,4,5,7]
val res11 = dropwhile even [3,4,6,8]

(* fancy pattern form: zs as (x::xs) *)


Dropwhile, without redundant parentheses

fun dropwhile p []              = []
| dropwhile p (zs as (x::xs)) =
if p x then  dropwhile p xs  else zs
val res10 = dropwhile even [2,4,5,7]
val res11 = dropwhile even [3,4,6,8]

(* fancy pattern form: zs as (x::xs) *)


Folds

fun foldr p zero []      = zero
| foldr p zero (x::xs) = p (x, (foldr p zero xs))

fun foldl p zero []      = zero
| foldl p zero (x::xs) = foldl p (p (x, zero)) xs

val res12 = foldr (op +)  0 [1,2,3,4]
val res13 = foldl (op * ) 1 [1,2,3,4]

(* Note 'op' to use infix operator as a value *)


Folds, without redundant parentheses

fun foldr p zero []      = zero
| foldr p zero (x::xs) = p (x,  foldr p zero xs )

fun foldl p zero []      = zero
| foldl p zero (x::xs) = foldl p (p (x, zero)) xs

val res12 = foldr (op +)  0 [1,2,3,4]
val res13 = foldl (op * ) 1 [1,2,3,4]

(* Note 'op' to use infix operator as a value *)


ML—Five Questions

Values: num/string/bool, constructed data

Syntax: definitions, expressions, patterns, types

Environments: names stand for values (and types)

Evaluation: uScheme + case and pattern matching

Initial Basis: medium size; emphasizes lists

(Question Six: type system—a coming attraction)

Ullman is easy to digest

Ullman costs money but saves time

Ullman is clueless about good style

Suggestion:

• Learn the syntax from Ullman
• Learn style from Ramsey, Harper, & Tofte

Details in course guide Learning Standard ML

# 25 Feb 2019: Programming with constructed data and types

There are PDF slides for 2/26/2019.

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

## Improving on Scheme

Scheme problems

Unsolved:

• Printf debugging

Solved:

• Need switch or similar
(Clausal definition, case expression)
• Only cons for data
(Define as many forms as you like: datatype)
• Wrong number of arguments (typecheck)
• car or cdr of non-list (typecheck)
• car or cdr of empty list (pattern match)

New vocabulary

Data:

• Constructed data
• Value constructor

Code:

• Pattern
• Pattern matching
• Clausal definition
• Clause

Types:

• Type variable (’a)

Today’s plan: programming with types

1. Mechanisms to know:

• Define a type
• Create value
• Observe a value
2. Making types work for you: from types, code

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

“Language support for forms of data”

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

Notes:

• 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

Mechanisms to know

• Define a type
• Create value (“introduction”)
• Observe a value (“elimination”)

For functions,

All you can do with a function is apply it

For constructed data,

“How were you made & from what parts?”

Datatype definitions

datatype  suit    = HEARTS | DIAMONDS | CLUBS | SPADES

datatype 'a list  = nil           (* copy me NOT! *)
| op :: of 'a * 'a list

datatype 'a heap  = EHEAP
| HEAP of 'a * 'a heap * 'a heap

type suit          val HEARTS : suit, ...
type 'a list       val nil   : forall 'a . 'a list
val op :: : forall 'a .
'a * 'a list -> 'a list
type 'a heap
val EHEAP: forall 'a.                          'a heap
val HEAP : forall 'a.'a * 'a heap * 'a heap -> 'a heap


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
• 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 type

• They 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

• Every val on this slide is a value constructor

• 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
• 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 typeinfix operators are always applied to pairs

Structure of algebraic types

An algebraic data type is a collection of alternatives

• Each alternative must have a name

The thing named is the value constructor

(Also called “datatype constructor”)

An ordinary S-expression is one of

• A symbol (string)
• A number (int)
• A Boolean (bool)
• A list of ordinary S-expressions

Two steps:

1. For each form, choose a value constructor
2. Write the datatype definition

datatype sx
= SYMBOL of string
| NUMBER of int
| BOOL   of bool
| SXLIST of sx list

## The other form of constructed data: tuples

Other constructed data: Tuples

Always only one way to form

• Expressions (e1, e2, …, en)

• Patterns (p1, p2, …, pn)

Example:

let val (left, right) = splitList xs
in  if abs (length left - length right) < 1
then
NONE
else
SOME "not nearly equal"
end

## Additional language support for algebraic types: case expressions

“Eliminate” values of algebraic types

New language construct case (an expression)

fun length xs =
case xs
of []      => 0
| (x::xs) => 1 + length xs

Clausal definition is preferred
(sugar for val rec, fn, case)

works for any datatype

 fun toStr t =
case t
of EHEAP => "empty heap"
| HEAP (v, left, right) =>
"nonempty heap"

But often a clausal definition is better style:

 fun toStr' EHEAP = "empty heap"
| toStr' (HEAP (v,left,right)) =
"nonempty heap"

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

Potential bonus content: inorder traversal of binary tree.

val find : forall 'a . ('a -> bool) -> ('a list -> 'a option)

Bonus content

The rest of this slide deck is “bonus content”
(intended primarily for those without books)

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

NODEs 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 trees, 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:

1. the type environment: suit, int_tree, tree

2. the value environment: HEART, LEAF, PARENT

### Inductive

Datatype definitions inherently inductive:

• the type int_tree appears in its own definition

• the type tree appears in its own definition

### Datatype Exercise

Wait for it …

datatype sx1 = ATOM1 of atom
| LIST1 of sx1 list

datatype sx2 = ATOM2 of atom
| PAIR2 of sx2 * sx2


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

Exception handling in action

loop (evaldef (reader (), rho, echo))
handle EOF            => finish ()
| Div               => continue "Division by zero"
| Overflow          => continue "Arith overflow"
| RuntimeError msg  => continue ("error: " ^ msg)
| IO.Io {name, ...} => continue ("I/O error: " ^
name)
| SyntaxError msg   => continue ("error: " ^ msg)


## Bonus Content: ML traps and pitfalls

Order of clauses matters


fun take n (x::xs) = x :: take (n-1) xs
| take 0 xs      = []
| take n []      = []

(* what goes wrong? *)


- fun plus x y = x + y;
> val plus = fn : int -> int -> int
- fun plus x y = x + y : real;
> val plus = fn : real -> real -> real


Gotcha — parentheses

Put parentheses around anything with |

case, handle, fn

Function application has higher precedence than any infix operator

## Bonus content (seen in examples)

### Syntactic sugar for lists

Syntactic sugar for lists

- 1 :: 2 :: 3 :: 4 :: nil; (* :: associates to the right *)
> val it = [1, 2, 3, 4] : int list

- "the" :: "ML" :: "follies" :: [];
> val it = ["the", "ML", "follies"] : string list

> concat it;
val it = "theMLfollies" : string


## Bonus content: ML from 10,000 feet

### Environments

The value environment

Names bound to immutable values

Immutable ref and array values point to mutable locations

ML has no binding-changing assignment

Definitions add new bindings (hide old ones):

val pattern = exp
val rec pattern = exp
fun ident patterns = exp
datatype … = …

Nesting environments

At top level, definitions

Definitions contain expressions:

def ::= val pattern = exp

Expressions contain definitions:

exp ::= let defs in exp end

Sequence of defs has let-star semantics

### Patterns

What is a pattern?

pattern ::= variable
| wildcard
| value-constructor [pattern]
| tuple-pattern
| record-pattern
| integer-literal
| list-pattern

Design bug: no lexical distinction between

• VALUE CONSTRUCTORS
• variables

Workaround: programming convention

### Functions

Function pecularities: 1 argument

Each function takes 1 argument, returns 1 result

For “multiple arguments,” use tuples!

 fun factorial n =
let fun f (i, prod) =
if i > n then prod else f (i+1, i*prod)
in  f (1, 1)
end

fun factorial n =  (* you can also Curry *)
let fun f i prod =
if i > n then prod else f (i+1) (i*prod)
in  f 1 1
end

Tuples are “usual and customary.”

# 27 Feb 2019: Types

There are PDF slides for 2/28/2019.

Notes on slide:

• Guide: What have I got? What holes am I trying to fill?

Type systems

What they do:

• Guide coding
• Document code (checked by compiler!)
• Rule out certain errors

How they work

• Predict values at run time

World’s most widely deployed static analysis

Where type systems are found:

• C#, Swift, Go
• Java, Scala, Rust (polymorphism)

Trajectory:

• Formalize familiar, monomorphic type systems (like C)
• Learn polymorphic type systems
• Eventually, infer polymorphic types

Monomorphic types systems are the past.
Inference and polymorphism are the present and future.
(Visible trend just like lambda.)

Today:

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

## Type systems

What kind of thing is it?

Types classify terms’’

“Term” is theory word for “syntax”:

n + 1  : int

"hello" ^ "world"  : string

(fn n => n * (n - 1))  : int -> int

if p then 1 else 0 : int, provided  p : bool

• 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 systems designed to solve a problem

• Confirm behavior
• Help the compiler

## 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. This is the highest level of cognitive task: creation of new things.

• Also your introduction to static analysis. Used in code improvement, security.

Define an AST for expressions with:

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

Type soundness

Key theorem: prediction is accurate

• Will state more precisely next week

• Best explanation for how/why type system works

• Proof beyond the scope of 105

Type-system example

Simple language of machine-level expressions

Two types:

• word predicts a machine word
(in a general-purpose register)

• flag predicts a single bit
(in a flags register)

Type this: Language of expressions

Words and flags:

datatype exp = ARITH of arithop * exp * exp
| CMP   of relop   * exp * exp
| LIT   of int
| IF    of exp     * exp * exp
and      arithop = PLUS | MINUS | TIMES | ...
and      relop   = EQ | NE | LT | LE | GT | GE

datatype ty = WORDTY | FLAGTY

(Looks a lot like int and bool)

### Examples to rule out

Can’t add a word and a flag:

3 + (3 < 99)

(ARITH(PLUS, LIT 3, CMP (LT, LIT 3, LIT 99)))

Can’t compare a word and a flag

(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 : word    |- 5 : word
-------------------------
|- 3 + 5 : word

Rules out:

|- 'a' : char    |- 5 : word
---------------------------
|- 'a' + 5 : ???

General form:

|- e1 : word    |- e2 : word
-----------------------------
|- ARITH ( _ , e1, e2) : word

### Rule for comparisons

Informal example:

|- 7 : word    |- 10 : word
-----------------------------
|- 7 < 10 : flag

General form:

|- e1 : word    |- e2 : word
-----------------------------
|- CMP ( _ , e1, e2) : flag

### Rule for literals

Informal example:

|- 14 : word

General form:

--------------------
|- LIT (n) : word

### Rule for conditionals:

Informal example:

|- true : flag
|- 3    : word
|- 42   : word
--------------------------
|- IF (true, 3, 42) : word

General form:

|- e : flag
|- 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 types can rule out

things that could go wrong:

(8 < 10) + 4

(8 == 8) < 9

x + (x :: xs)

let val y = 10 in length y end

### What is a type?

• Weak: a set of values

• Better: a conservative prediction about values

• Best: 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 (WORDTY, WORDTY) => WORDTY
| _              => raise IllTyped
| typeof (CMP (_, e1, e2)) =
case (typeof e1, typeof e2)
of (WORDTY, WORDTY) => FLAGTY
| _              => raise IllTyped
| typeof (LIT _) = WORDTY
| typeof (IF (e,e1,e2)) =
case (typeof e, typeof e1, typeof e2)
of (FLAGTY, 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.

    datatype exp = ARITH of arithop * exp * exp
| CMP   of relop   * exp * exp
| LIT   of int
| IF    of exp     * exp * exp
| VAR   of name
| LET   of name    * exp * exp
and      arithop = PLUS | MINUS | TIMES | ...
and      relop   = EQ | NE | LT | LE | GT | GE

datatype ty = WORDTY | FLAGTY


## Typing Rules: Contexts and Term Variables

• What you need for VAR and LET

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

Type checking for variables

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 

# 4 March 2019: Type checking with type constructors

There are PDF slides for 3/5/2019.

### Approaching types as programmers

Understanding language design

Questions about types never seen before:

• What types can I make?
• What syntax goes with each form?
• What functions?

Examples: pointer, struct, function, record

Talking type theory

Formation: make new types

Introduction: make new values

Elimination: observe (“take apart”) existing values

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

Review:

• Types classify terms
• Types serve a purpose (guide compiler, prevent bugs)
• Type system with two types
• Types relate to syntax (Introduction, Elimination)
• Typing rules

Upcoming (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.

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

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

Examples: Not yet types, or not types at all

These types in waiting’’ These are

Type-formation rules

We need a way to classify type expressions into:

• types that classify terms

• type constructors that build types

• nonsense that doesn’t mean anything

Type judgments for monomorphic system

Two judgments:

• The familiar typing judgment Γ ⊢ e : τ
• Today’s judgment “τ is a type”

### Monomorphic type rules

Notice: one rule for if!!

## Classic types for data structures

(At run time, identical to cons, car, cdr)

Typical syntactic support for types

Explicit types on lambda and define:

• For lambda, argument types:

(lambda ([n : int] [m : int]) (+ (* n n) (* m m)))
• For define, argument and result types:

(define int max ([x : int] [y : int])
(if (< x y) y x))

Abstract syntax:

datatype exp = ...
| LAMBDA of (name * tyex) list * exp
...
datatype def = ...
| DEFINE of name * tyex * ((name * tyex) list * exp)
...

Wait for it …

### Coding the arrow-introduction rule

Type-checking LAMBDA

datatype exp = LAMBDA of (name * tyex) list * exp
...
fun ty (Gamma, LAMBDA (formals, body)) =
let val Gamma' = (* body gets new env *)
foldl (fn ((x, ty), g) => bind (x, ty, g))
Gamma formals
val bodytype = ty (Gamma', body)
val formaltypes =
map (fn (x, ty) => ty) formals
in  FUNTY (formaltypes, bodytype)
end


# 6 March 2019: Polymorphic Type Checking; Kinds classify types

There are PDF slides for 3/7/2019.

### Today

In class:

• Type-checking review
• Burdens of monomorphism
• On designers and implementors
• On programmers
• Lift burden with quantified types
• Extensible type formation

Language targets: Java, Scala, C# (with “generics”)

Wait for it …

## Limitations of monomorphic type systems

New types are expensive

Closed world

• Only a designer can add a new type constructor

A new type constructor (“array”) requires

• Special syntax
• New type rules
• New internal representation (type formation)
• New code in type checker (intro, elim)
• New or revised proof of soundness

Notes:

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

Expense for programmers

User-defined functions are monomorphic:

(check-function-type swap
([array bool] int int -> unit))
(define unit swap ([a : (array bool)]
[i : int]
[j : int])
(begin
(set tmp       (array-at a i))
(array-put a i (array-at a j))
(array-put a j tmp)
(begin)))

## Quantified types

Idea: Do it all with functions

• No new syntax
• No new internal representation
• No new type rules
• One proof of soundness
• Programmers can add new types

Requires: more expressive function types

Better type for a swap function

(check-type
swap
(forall ('a) ([array 'a] int int -> unit)))

## Polymorphic Type Checking

### Quantified types

Representing quantified types

Two new alternatives for tyex:

datatype tyex
= TYCON  of name                // int
| CONAPP of tyex * tyex list    // (list bool)
| FUNTY  of tyex list * tyex    // (int int -> bool)
| TYVAR  of name                // 'a
| FORALL of name list * tyex    // (forall ('a) ...)

Programming with quantified types

Substitute for quantified variables: “instantiate”

-> length
<procedure> : (forall ('a) ((list 'a) -> int))
-> [@ length int]
<procedure> : ((list int) -> int)
-> (length '(1 2 3))
type error: function is polymorphic; instantiate before applying
-> ([@ length int] '(1 2 3))
3 : int

Substitute what you like

-> length
: (forall ('a) ((list 'a) -> int))
-> [@ length bool]
: ((list bool) -> int)
-> ([@ length bool] '(#t #f))
2 : int


More instantiations

-> (val length-int [@ length int])
length-int : ((list int) -> int)
-> (val cons-bool [@ cons bool])
cons-bool : ((bool (list bool)) -> (list bool))
-> (val cdr-sym [@ cdr sym])
cdr-sym : ((list sym) -> (list sym))
-> (val empty-int [@ '() int])
() : (list int)


Bonus instantiation:

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

Polymorphic array swap

(check-type swap
(forall ('a) ([array 'a] int int -> unit)))

(val swap
(type-lambda ('a)
(lambda ([a : (array 'a)]
[i : int]
[j : int])
(let ([tmp ([@ Array.at 'a] a i)])
(begin
([@ Array.put 'a] a i ([@ Array.at 'a] a j))
([@ Array.put 'a] a j tmp))))))


Two forms of abstraction:

Power comes at notational cost

Function composition

-> (val o (type-lambda ['a 'b 'c]
(lambda ([f : ('b -> 'c)]
[g : ('a -> 'b)])
(lambda ([x : 'a]) (f (g x))))))

o : (forall ('a 'b 'c)
(('b -> 'c) ('a -> 'b) -> ('a -> 'c)))

Aka o :

## Type formation through kinds

What have we gained?

No more introduction rules:

No more elimination rules:

But, we still need formation rules

You can’t trust code

User’s types not blindly trusted:

-> (lambda ([a : array]) (Array.size a))
type error: used type constructor array' as a type
-> (lambda ([x : (bool int)]) x)
type error: tried to apply type bool as type constructor
-> (@ car list)
type error: instantiated at type constructor list', which is not a type

How can we know which types are OK?

Designer’s burden reduced

To extend Typed Impcore:

• New syntax
• New type rules
• New internal representation
• New code
• New soundness proof

To extend Typed μScheme, none of the above! Just

• New functions
• New primitive type constructor in Δ

You’ll do arrays both ways

## Opening the closed world

Typed Impcore:

• Closed world (no new types)

• Simple formation rules

Typed μScheme:

• Semi-closed world (new type variables)

• How are types formed (from other types)?

Standard ML:

• Open world (programmers create new types)

• How are types formed (from other types)?

# 13 March 2019: Introduction to type inference

There are PDF slides for 3/14/2019.

## Announcements

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

### Extra office hours

• Tomorrow
• Maybe Friday
• Week after break

(And you’ll get an email)

## Today

How does the compiler know?

fun append (x::xs) ys = x :: append xs ys
| append []      ys = ys

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

What type inference accomplishes

-> (define     double (x)       (+ x x))
double                         ;; uScheme
-> (define int double ([x : int]) (+ x x))
double : (int -> int)          ;; Typed uSch.
-> (define     double (x)       (+ x x))
double : (int -> int)          ;; nML


What else type inference accomplishes

-> ([@ cons bool] #t ([@ cons bool] #f [@ '() bool]))
(#t #f) : (list bool)    ;; typed uScheme
-> (   cons       #t (   cons       #f    '()      ))
(#t #f) : (list bool)    ;; nML


How it works

1. For each unknown type, a fresh type variable

2. Every typing rule adds equality constraints

3. Instantiate every variable automatically

4. Introduce polymorphism at let/val bindings

Plan of study:

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

• At end of class, you’ll do an example

• After break, we’ll solve constraints

• And 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 a1

• x has type a2

• + has type int * int -> int

• (+ x x) is an application, what does it require?

• a2 = int and a2 = 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 a3, 1 has type int, 0 has type int

• Requires what constraints? (int = int, a3 = bool)

Example:

• (if z z (- 0 z))

• z has type a3, 0 has type int, - has type int * int -> int

• Requires what constraints? (a3 = bool /\ int = int /\ a3 = 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))

# 25 March 2019: Making type inference precise

There are PDF slides for 3/26/2019.

### Announcements

#### Office hours

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

• Today after class (booked, maybe some walk-ins)
• Tomorrow, March 26, 1:00 to 3:00 (booked, room for 9 walk-ins)
• Wednesday, March 27, 11:00 to 12:00 (booked, room for 4 walk-ins)
• Thursday, March 28, 11:00 to 12:00, 2:00 to 5:00 (many slots open)
• Friday, March 29, 11:00 to 12:00 (3 slots open, 4 walk-ins)
• Friday, March 29, 3:30 to 4:30 (1 slots open, 4 walk-ins)

Book a slot at https://www.cs.tufts.edu/~nr/cgi-bin/meeting.cgi?meeting=105.

#### Exam results:

  67 and up: Very Good (34 students)
50 to 67:  Good      (66 students)
29 to 50:  Fair      (17 students)
under 29:  Poor      ( 1 student)

## Review

Type inference: Review of the basics

1. For each unknown type, a fresh type variable

2. Instantiate every variable automatically

3. Every typing rule adds equality constraints

4. Solve constraints to get substitution

5. Apply substitution to constraints and types

6. Introduce polymorphism at let/val bindings

Review: Using polymorphic names


-> (val cc (lambda (nss) (car (car nss))))



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

Using polymorphic names


-> (val cc (lambda (nss) (car (car nss))))

cc : (forall ('a) ((list (list 'a)) -> 'a))


Given

  empty : (forall ['a] (list 'a))
cons  : (forall ['a] ('a (list 'a) -> (list 'a)))

For

  (cons empty empty)

You fill in:

1. Fresh instances
2. Constraints
3. Final type

### Bonus examples

Bonus example

-> (val second (lambda (xs) (car (cdr xs))))
second : ...
-> (val two    (lambda (f) (lambda (x) (f (f x)))))
two : ...


Bonus example solved

-> (val second (lambda (xs) (car (cdr xs))))
second : (forall ('a) ((list 'a) -> 'a))
-> (val two    (lambda (f) (lambda (x) (f (f x)))))
two :    (forall ('a) (('a -> 'a) -> ('a -> 'a)))


Infer the type of function two:

## Precise inference with Hindley-Milner types

Making Type Inference Precise

• Type inference for polymorphism is undecidable

Solution:

• Each formal parameter has a monomorphic type

Consequences:

• The argument to a higher-order function cannot be mandated to be polymorphic
• forall appears only outermost in types

Representing Hindley-Milner types

type tyvar = name
datatype ty
= TYVAR  of tyvar
| TYCON  of name
| CONAPP of ty * ty list

datatype type_scheme
= FORALL of tyvar list * ty

fun funtype (args, result) =
CONAPP (TYCON "function",
[CONAPP (TYCON "arguments", args),
result])


To code the type-inference algorithm, replace eqType with constraint generation!

All the pieces

1. Hindley-Milner types
2. Bound names : σ, expressions : τ
3. Type inference yields type-equality constraint
4. Constraint solving produces substitution
5. Substitution refines types
6. Call solver, introduce polytypes at val
7. Call solver, introduce polytypes at all let forms

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

You can complete typeof

• Takes e and Γ, returns τ and C

(Except for let forms.)

Next up: solving constraints

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.

# 27 March 2019: Building and using a constraint solver

There are PDF slides for 3/28/2019.

Announcement: exam hard copy (no markup), my office hours

Responses to midterm evals:

• Walk-in recitations Wednesdays 6pm
• 574 Boston Ave. rooms 310 and 316
• “Nobody goes there any more; it’s too crowded”
• The queue:

• It’s not meant to be first come, first served. Groups go before individuals.

• Not everybody gets the same number of minutes. The goal is long-term fairness: everybody gets the help they need.

• Break between homework releases: if I define a break, there are at least 20 students it works badly for. Define your own break.

• We know we need to do better on proofs. Working on it for next year.

• More to come

Today:

• Solving constraints
• Final inference rules:
• Generalize at VAL, LET, and LETREC

## Solving constraints

Representing Constraints

datatype con = ~   of ty  * ty
| /\  of con * con
| TRIVIAL
infix 4 ~
infix 3 /\


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.

{Examples}

Which have solutions?

 1. int           ~ bool
2. (list int)    ~ (list bool)
3. 'a            ~ int
4. 'a            ~ (list int)
5. 'a            ~ ((args int) -> int)
6. 'a            ~ 'a
7. (args 'a int) ~ (args bool 'b)
8. (args 'a int) ~ ((args bool) -> 'b)
9. 'a            ~ (pair 'a int)
10. 'a            ~ tau    // arbitrary tau

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

Revisit a rule:

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

(lambda (ys)  ; OK
(let ([s (lambda (x) (cons x '()))])
(pair (s 1) (s #t))))

(lambda (ys)  ; Oops!
(let ([extend (lambda (x) (cons x ys))])
(pair (extend 1) (extend #t))))

(lambda (ys)  ; OK
(let ([extend (lambda (x) (cons x ys))])
(extend 1)))


Let with constraints, operationally:

1. typesof: returns τ1, …, τn and C

2. val theta = solve C

3. C-prime from map, conjoinConstraints, dom, inter, freetyvarsGamma

4. freetyvarsGamma, union, freetyvarsConstraint

5. Map anonymous lambda using generalize, get all the σi

6. Extend the typing environment Gamma (pairfoldr)

7. Recursive call to type checker, gets C_b, \tau

8. Return (tau, C' /\ C_b)

Forall things

Managing Quantified types
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

# 1 April 2019: Hiding information with abstract data types

There are PDF slides for 4/2/2019.

Announcements

• Hiring TAs for fall
• Midterm course evals:
• Experimental Wednesday night recitation continues this week
• Photo is not deleted from server, but access is locked down. (Same policy as SIS.)
• Review of homework solutions: when??
• Exercises deemed redundant or repetitive; busy work: I may ask on Piazza (Note varied skills on recursion.)
• Questions in lecture: I’ll try to keep on point
• Moving images (soccer games and others): back row only

Plan for April:

• Programming at scale: modules and objects
• Lambda calculus (connections to modules and to Smalltalk)

Today’s learning objectives:

• Ideas found in language designs
• Terminology
• Understanding interfaces in Standard ML

## Data abstraction

Where have we been?

• Programming in the small
• Expressive power
• Success stories:

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

• Immersion in pile of interpreter code: not fun

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

Example interface with declarations

signature ILIST = sig
type 'a ilist  (* nonempty; one element indicated *)
val singletonOf    : 'a -> 'a ilist
val indicated      : 'a ilist -> 'a
val indicatorLeft  : 'a ilist -> 'a ilist
val indicatorRight : 'a ilist -> 'a ilist
val deleteLeft  : 'a ilist -> 'a ilist
val deleteRight : 'a ilist -> 'a ilist
val insertLeft  : 'a * 'a ilist -> 'a ilist
val insertRight : 'a * 'a ilist -> 'a ilist
val ifoldl : ('a * 'b -> 'b) -> 'b -> 'a ilist -> 'b
val ifoldr : ('a * 'b -> 'b) -> 'b -> 'a ilist -> 'b
end


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

Design choice: placing interfaces

Interface “projected” from implementation:

• No separate interface
• Compiler extracts from implementation
• When code changes, must extract again
• Few cognitive benefits

Full interfaces:

• Distinct file, separately compiled
• Implementations can change independently
• Full cognitive benefits

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

ML module terminology

Interface is a signature

Implementation is a structure

Generic module is a functor

• A compile-time function over structures

• The point: reuse without violating abstraction

Structures and functors match signature

Analogy: Signatures are the types’’ of structures.

### Signature basics

Signature says what’s in a structure

Specify types (w/kind), values (w/type), exceptions

Ordinary type examples:

    type t        // abstract type, kind *
eqtype t
type t = ...  // 'manifest' type
datatype t = ...

Type constructors work too

    type 'a t     // abstract, kind * => *
eqtype 'a t
type 'a t = ...
datatype 'a t = ...

### ML Modules examples, part I

Signature example: Ordering


signature ORDERED = sig
type t
val lt : t * t -> bool
val eq : t * t -> bool
end



Signature example: Integers

signature INTEGER = sig
eqtype int             (* <-- ABSTRACT type *)
val ~   : int -> int
val +   : int * int -> int
val -   : int * int -> int
val *   : int * int -> int
val div : int * int -> int
val mod : int * int -> int
val >   : int * int -> bool
val >=  : int * int -> bool
val <   : int * int -> bool
val <=  : int * int -> bool
val compare : int * int -> order
val toString   : int    -> string
val fromString : string -> int option
end


Implementations of integers

A selection…

structure Int    :> INTEGER
structure Int31  :> INTEGER  (* optional *)
structure Int32  :> INTEGER  (* optional *)
structure Int64  :> INTEGER  (* optional *)
structure IntInf :> INTEGER  (* optional *)

Homework: natural numbers

signature NATURAL = sig
type nat   (* abstract, NOT 'eqtype' *)
exception Negative

val ofInt   : int -> nat
val /+/     : nat * nat -> nat
val /-/     : nat * nat -> nat
val /*/     : nat * nat -> nat
val sdiv    : nat * int ->
{ quotient : nat, remainder : int }
val compare : nat * nat -> order
val decimal : nat -> int list
end

Homework: integers

signature BIGNUM = sig
type bigint

val ofInt    : int -> bigint
val negated  : bigint -> bigint
val <+>      : bigint * bigint -> bigint
val <->      : bigint * bigint -> bigint
val <*>      : bigint * bigint -> bigint
val sdiv : bigint * int ->
{ quotient : bigint, remainder : int }
val compare  : bigint * bigint -> order
val toString : bigint -> string
end

# 3 April 2019: more ML modules

There are PDF slides for 4/4/2019.

Signature review: collect

signature QUEUE = sig
type 'a queue    (* another abstract type *)
exception Empty

val empty : 'a queue
val put : 'a * 'a queue -> 'a queue
val get : 'a queue -> 'a * 'a queue   (* raises Empty *)

(* LAWS:  get(put(a, empty))     ==  (a, empty)
...
*)
end


Structure: collect definitions

structure Queue :> QUEUE = struct   (* opaque seal *)
type 'a queue = 'a list
exception Empty

val empty = []
fun put (x,q) = q @ [x]
fun get [] = raise Empty
| get (x :: xs) = (x, xs)

(* LAWS:  get(put(a, empty))     ==  (a, empty)
...
*)
end


Dot notation to access components

fun single x = Queue.put (Queue.empty, x)
val _ = single : 'a -> 'a Queue.queue


What interface with what implementation?

Maybe mixed together, extracted by compiler!

Maybe matched by name:

Best: any interface with any implementation:

• Java, Standard ML

But: not “any”—only some matches are OK

Signature Matching

Well-formed

 structure Queue :> QUEUE = QueueImpl

if principal signature of QueueImpl matches ascribed signature QUEUE:

• Every type in QUEUE is in QueueImpl

• Every exception in QUEUE is in QueueImpl

• Every value in QUEUE is in QueueImp
(type could be more polymorphic)

• Every substructure matches, too (none here)

Signature Ascription

Ascription attaches signature to structure

• Transparent Ascription: types are revealed

structure strid : sig_exp = struct_exp

This method is stupid and broken (legacy)
(But it’s awfully convenient)

• Opaque Ascription: types are hidden (“sealing”)

structure strid :> sig_exp = struct_exp

This method respects abstraction
(And when you need to expose, can be tiresome)

Slogan: “use the beak”

Opaque Ascription

Recommended

Example:

 structure Queue :> QUEUE = struct
type 'a queue = 'a list
exception Empty

val empty = []
fun put (x, q) = q @ [x]
fun get [] = raise Empty
| get (x :: xs) = (x, xs)
end

Not exposed: type ’a Queue.queue = ’a list

• Respects abstraction

## Abstract data types

How opaque ascription works

• Protects invariants
• Allows software to evolve
• Type system limits interoperability

• Every function sees rep of every argument
• Key distinction abstract type vs object

Abstract data types and your homework

Natural numbers

• Funs/+/,/-/,/*/ see both representations

• Makes arithmetic relatively easy

• But type nat works only with type nat
(no “mixed” arithmetic)

## Data abstraction for reuse

Abstract data types and your homework

Two-player games:

• Abstraction not as crisp as “number” or “queue”

Problems abstraction must solve:

• Interact with human player via strings
(accept moves, visualize state)

• Know whose turn it is

• Handle special features like “extra moves”

• Provide API for computer player

Result: a wide interface

Testing code with abstract types

Test properties of observed data:

• If player X has won, the game is over

• If the game is over, there are no legal moves

• If there are no legal moves, the game is over

Same story with numbers:

• negated (negated i) equals i

• (i <+> j) <-> i equals j

Abstraction design: Computer player

Computer player should work with any game, provided

• Up to two players
• Complete information
• Always terminates

Brute force: exhaustive search

Your turn! What does computer player need?

• Types?
• Exceptions?
• Functions?

Our computer player: AGS

Any game has two key types:

  type state
structure Move : MOVE  (* exports move *)

Key functions use both types:

  val legalmoves : state -> Move.move list
val makemove   : state -> Move.move -> state

Multiple games with different state, move?

Yes! Using key feature of ML: functor

A is a generic module

A new form of parametric polymorphism:

• lambda and type-lambda in one mechanism

• Introduction form is functor (definition form)

• Actually pleasant to use

“Generics” found across language landscape
(wherever large systems are built)

## Functors and an Extended SML Example

Game interoperability with functors

functor AgsFun (structure Game : GAME) :> sig
structure Game : GAME
Game.state ->
{ recommendation  : Game.Move.move option
, expectedOutcome : Player.outcome
}
end
where type Game.Move.move = Game.Move.move
and   type Game.state     = Game.state
= struct
structure Game = Game
... definitions of helpers, advice ...
end


Functors: baby steps

A functor abstracts over a module

Formal parameters are declarations:

functor MkSingle(structure Q:QUEUE) =
struct
structure Queue = Q
fun single x = Q.put (Q.empty, x)
end

Combines familiar ideas:

• Higher-order functions (value parameter Q.put)
• type-lambda (type parameter Q.queue)

Using Functors

Functor applications are evaluated at compile time.

functor MkSingle(structure Q:QUEUE) =
struct
structure Queue = Q
fun single x = Q.put (Q.empty, x)
end

Actual parameters are definitions

structure QueueS  = MkSingle(structure Q = Queue)
structure EQueueS = MkSingle(structure Q = EQueue)

where EQueue is a more efficient implementation

Separate compilation:

• Unit tests for natural numbers, without an implementation of natural numbers

Code reuse with type abstraction

• Abstract Game Solver
(any representation of game state, move)

ML module summary

New syntactic category: declaration

• Of type, value, exception, or module

Signature groups declarations: interface

Structure groups definitions: implementation

Functor enables reuse:

• Formal parameter: declarations
• Actual parameter: definitions

Opaque ascription hides information

• Enforces abstraction

## Extended example: Error-tracking Interpreter

Reusable Abstractions: Extended Example

Error-tracking interpreter for a toy language

### Why this example?

• Lots of interfaces using ML signatures

• Idea of how to compose large systems

• Some ambitious, very abstract abstractions—it’s toward the end of term, and you should see something ambitious.

• Practice implementing functors

Error modules: Three common implementations

• Collect all errors

• Keep just the first error

• Keep the most severe error

Your obligations: two types, three functions, algebraic laws

Classic accumulator’’ for errors

signature ERROR = sig
type error   (* a single error *)
type summary (* summary of what errors occurred *)

val nothing : summary                  (* no errors *)
val <+> : summary * summary -> summary (* combine *)

val oneError : error -> summary

(* laws:   nothing <+> s == s
s <+> nothing == s
s1 <+> (s2 <+> s3) == (s1 <+> s2) <+> s3
// associativity
*)
end


First Error: Implementation

structure FirstError :>
ERROR where type error = string
and type summary = string option =
struct
type error   = string
type summary = string option

val nothing = NONE
fun <+> (NONE,   s) = s
| <+> (SOME e, _) = SOME e

val oneError = SOME
end


All Errors: Implementation

structure AllErrors :>
ERROR where type error   = string
and type summary = string list =
struct
type error   = string
type summary = error list

val nothing = []
val <+> = op @
fun oneError e = [e]
end


### Computations Abstraction

Computations either:

• return a value

• produce an error

Errors must be threaded through everything :-(

Exercise: Simple arithmetic interpreter

(* Given: *)
datatype 'a comp = OK of 'a | ERR of AllErrors.summary

datatype exp = LIT  of int
| PLUS of exp * exp
| DIV  of exp * exp

(* Write an evaluation function that tracks errors. *)

val eval : exp -> int comp = ...



Exercise: LIT and PLUS cases

fun eval (LIT n) = OK n
| eval (PLUS (e1, e2)) =
(case eval e1
of OK v1 =>
(case eval e2
of OK  v2 => OK (v1 + v2)
| ERR s2 => ERR s2)
| ERR s1 =>
(case eval e2
of OK  _  => ERR s1
| ERR s2 => ERR (AllErrors.<+> (s1, s2))))



Exercise: DIV case

  | eval (DIV (e1, e2)) =
(case eval e1
of OK v1 =>
(case eval e2
of OK   0 => ERR (AllErrors.oneError "Div 0")
| OK  v2 => OK  (v1 div v2)
| ERR s2 => ERR s2)
| ERR s1 =>
(case eval e2
of OK  v2 => ERR s1
| ERR s2 => ERR (AllErrors.<+> (s1, s2)))


That’s really painful!

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

Combining generic computations

signature COMPUTATION = sig
type 'a comp    (* Computation! When run, results in
value of type 'a or error summary. *)

(* A computation without errors always succeeds. *)
val succeeds : 'a -> 'a comp

(* Apply a pure function to a computation. *)
val <$> : ('a -> 'b) * 'a comp -> 'b comp (* Application inside computations. *) val <*> : ('a -> 'b) comp * 'a comp -> 'b comp (* Computation followed by continuation. *) val >>= : 'a comp * ('a -> 'b comp) -> 'b comp end  ### 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 {Buckets of algebraic laws}  succeeds a >>= k == k a // identity comp >>= succeeds == comp // identity comp >>= (fn x => k x >>= h) == (comp >>= k) >>= h // associativity succeeds f <*> succeeds x == succeeds (f x) // success ...  Environments using computation’’ signature COMPENV = sig type 'a env (* environment mapping strings to values of type 'a *) type 'a comp (* computation of 'a or an error summary *) val lookup : string * 'a env -> 'a comp end  Payoff! functor InterpFn(structure Error : ERROR structure Comp : COMPUTATION structure Env : COMPENV val zerodivide : Error.error val error : Error.error -> 'a Comp.comp sharing type Comp.comp = Env.comp) = struct val (<*>, <$>, >>=) = (Comp.<*>, Comp.<$>, Comp.>>=) (* Definition of Interpreter *) end  Definition of intepreter, continued datatype exp = LIT of int | VAR of string | PLUS of exp * exp | DIV of exp * exp fun eval (e, rho) = let fun ev(LIT n) = Comp.succeeds n | ev(VAR x) = Env.lookup (x, rho) | ev(PLUS (e1, e2)) = curry op + <$> ev e1 <*> ev e2
| ev(DIV (e1, e2))  = ev e1 >>= (fn n1 =>
ev e2 >>= (fn n2 =>
case n2
of 0 => error zerodivide
| _ => Comp.succeeds
(n1 div n2)))
in  ev e
end


{Extend a signature with }

signature ERRORCOMP = sig
include COMPUTATION
structure Error : ERROR
datatype 'a result = OK  of 'a
| ERR of Error.summary
val run : 'a comp -> 'a result
val error : Error.error -> 'a comp
end


{Let’s build }

functor ErrorCompFn(structure Error : ERROR) :>
ERRORCOMP where type Error.error   = Error.error
and type Error.summary = Error.summary =
struct
structure Error = Error
datatype 'a result = OK  of 'a
| ERR of Error.summary

type 'a comp = 'a result
fun run comp = comp

fun error e = ERR (Error.oneError e)
fun succeeds = OK
...
end


## ML Module summary

ML module summary

New syntactic category: declaration

• Of type, value, exception, or module

Signature groups declarations: interface

Structure groups definitions: implementation

Functor enables reuse:

• Formal parameter: declarations
• Actual parameter: definitions

Opaque ascription hides information

• Enforces abstraction

# 8 April 2019: Lambda Calculus

There are PDF slides for 4/9/2019.

Handouts:

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)

Substitution examples:

• bash
• tcl/tk
• TeX/LaTeX

### What is a calculus?

Demonstration of differential calculus: reduce

d/dx (x + y)2

Rules:

d/dx k = 0
d/dx x = 1
d/dx y = 0 where y is different from x
d/dx (u + v) = d/dx u + d/dx v
d/dx (u * v) = u * d/dx v + v * d/dx u
d/dx (e^n)   = n * e^(n-1) * d/dx e

So

d/dx (x + y)2

2 ⋅ (x + y) ⋅ d/dx(x + y)

2 ⋅ (x + y) ⋅ (d/dxx + d/dxy)

2 ⋅ (x + y) ⋅ (1 + d/dxy)

2 ⋅ (x + y) ⋅ (1 + 0)

2 ⋅ (x + y) ⋅ 1

2 ⋅ (x + y)

What is a calculus? Manipulation of syntax.

What corresponds to evaluation? “Reduction to normal form”

### Why study lambda calculus?

• 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

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

### The world’s simplest reasonable programming language

Just application, abstraction, variables

• Living without let, while
• Living without if
• Living without recursive define
• Coding data structures
• Coding natural numbers

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

Absolute minimum of code forms: no set, while, begin, but also no if and no define!

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

• Instead, use my handout “Coding in Lambda Calculus”

Systematic approach to constructed data:
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 and if expressions

A Boolean takes two continuations.

Laws:

true  s f = s
false s f = f

Code:

true  = \x.\y.x
false = \x.\y.y

Coding the if expression, laws:

if true  then N else P = N
if false then N else P = P

Therefore, code is:

if M then N else P = ???

Your turn: implement not

• Laws for not: what are the forms of the input data?

• Code for not

## Coding data structures

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

fst (pair x y) = x
snd (pair x y) = y
• 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

• List laws

null? nil         = true
null? (cons x xs) = false
car (cons x xs)   = x
cdr (cons x xs)   = xs
• 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

Church Numerals to machine integers

; uscheme or possibly uhaskell
-> (val add1 ((curry +) 1))
-> (define to-int (n)
-> (to-int three)
3
-> (to-int ((times three) four))
12


Church Numerals in λ

<0>   = \f.\x.x;
succ  = \n.\f.\x.f (n f x);
plus  = \n.\m.n succ m;
times = \n.\m.n (plus m) <0>;
...
-> <4>;
\f.\x.f (f (f (f x)))
-> <3>;
\f.\x.f (f (f x))
-> times <4> <3>;
\f.\x.f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))


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

## Normal forms

Idea: normal form

A term is a normal form if

It cannot be reduced

What do you suppose it means to say

• A term has no normal form?

• A term has a normal form?

Idea: normal form

A term is a normal form if

It cannot be reduced

A term has a normal form if

There exists a sequence of reductions that terminates (in a normal form)

A term has no normal form if

It always reduces forever
(This term diverges)

# 10 April 2019: Lambda-calculus semantics; encoding recursion

There are PDF slides for 4/11/2019.

### Today

Lambda:

• Operational semantics
• Beta reduction and capture-avoiding substitution
• Reduction strategies (making deterministic)
• Recursion and the Y combinator

## Review: Church encodings

Review: Church Numerals

<0>   = \f.\x.x;
succ  = \n.\f.\x.f (n f x);
plus  = \n.\m.n succ m;
times = \n.\m.n (plus m) <0>;
...
-> <4>;
\f.\x.f (f (f (f x)))
-> <3>;
\f.\x.f (f (f x))
-> times <4> <3>;
\f.\x.f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))


Almost all of programming

Data:

• Functions
• Constructed data
• Numbers
• Missing: pointers

Code:

• Function definition & application
• Conditionals
• Missing: ???

Question: What’s missing from this picture?

Astonishing fact: we don’t need letrec or val-rec (to com)

To see how it works, first, the semantics

## Beta-reduction (homework, part 2)

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

Board examples:

1. Are these functions the same?

\x.\y.x
\w.\z.w
2. Are these functions the same?

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

Examples of free variables:

\x . + x y

\x. \y. x

What are the free variables in each expression?

  \x.\y. y z
\x.x (\y.x)
\x.\y.\x.x y
\x.\y.x (\z.y w)
y (\x.z)
(\x.\y.x y) y        

What are the free variables in each expression?

  \x.\y. y z           - z
\x.x (\y.x)          - nothing
\x.\y.\x.x y         - nothing
\x.\y.x (\z.y w)     - w
y (\x.z)             - y z
(\x.\y.x y) y        - y

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

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

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

## Coding recursion

Recursion!

Coded by “successive approximations”

Factorial in lambda calculus

Wish for:

fact = \n.(zero? n) <1> (times n (fact (pred n)));

But: on right-hand side, fact is not defined.

Successive approximations

Function bot always goes into an infinite loop.

What are these?

fact0 = \n.(zero? n) <1> (times n (bot   (pred n)));

fact1 = \n.(zero? n) <1> (times n (fact0 (pred n)));

fact2 = \n.(zero? n) <1> (times n (fact1 (pred n)));

cessive approximations (manufactur

g = \f.\n.(zero? n) <1> (times n (f (pred n)));

fact0 = g bot;

fact1 = g fact0;       // = g (g bot)

fact2 = g fact1;      // = g (g (g bot))

fact3 = g fact2;      // = g (g (g (g bot)))

...

Fixed point

Suppose f = g f. I claim f n is n factorial!

Proof by induction on n.

Fixed-point combinator

What if

fix g = g (fix g)

Then fix g n is n factorial!

fix g = g (fix g)
= g (g (fix g))
= g (g (g (fix g)))
= ...

Expand as much as you need to.

### Using fixed points

Now you do it

Conversion to fixed point


length = \xs.null? xs <0> (+ <1> (length (cdr xs)))

lg = \lf.\xs.null? xs <0> (+ <1> (lf (cdr xs)))


Example recursion equations

Is there a solution? Is it unique? If so, what is it?

f1 = \n.\m.(eq? n m) n
(plus n (f1 (succ n) m));

f2 = \n.f2 (zero? n <100> (pred n));

f3 = \xs.xs nil (\z.\zs.cons <0> (f3 zs));

f4 = \xs.\ys.f4 ys xs;

Example recursion equations

f1 = \n.\m.(eq? n m) n
(plus n (f1 (succ n) m));
; sigma (sum from n to m)

f2 = \n.f2 (zero? n <100> (pred n));
; no unique solution (any constant f2)

f3 = \xs.xs nil (\z.\zs.cons <0> (f3 zs));
; map (const 0)

f4 = \xs.\ys. f4 xs ys;
; not unique: constant funs, commutative ops

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

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 languages

• A 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.

# 17 April 2019: Object-orientation

There are PDF slides for 4/18/2019.

Languages: JavaScript, Ruby, Java, C++, Python, …

• Encapsulation
• Higher-order programming
• Dynamic dispatch
• (Inheritance)

In common with modules, lambda calculus: you can’t touch things directly.

### Object-oriented demo

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:

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

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

6. Object 1, draw yourself on the board

7. Object 2, draw yourself on the board

8. Object 3, draw yourself on the board

## Key concepts of object-orientation

### Key mechanisms

Encapsulate: 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)

Higher-order: Code attached to objects and classes

• Code needed to draw the object is associated with the object
(A species of higher-order programming)

Dynamic dispatch (NEW)

• We don’t know what function will be called
• In fact, there is no function; code is a method’’

### Key idea

Protocol determines behavioral subtyping

### Class-based object-orientation

Dynamic dispatch determined by class definition

Code reuse by sending messages around like crazy

### What’s hard

• Encapsulation: abstraction function and invariant
• Higher-order programming: everything is higher order
• Dynamic dispatch: every call is to an unknown function (trust the contract)
• Inheritance: big vocabulary, hard to work one function in isolation

Net effect: algorithms “smeared out” over many methods

### What’s great

• Cooperating-objects model
• Reuse, reuse, reuse

## Example: list filter

Example: list filter

-> (val ns (new List))
List( )
-> (addAll: ns '(1 2 3 4 5 6))
List( 1 2 3 4 5 6 )
-> (select: ns [block (n) (= 0 (mod: n 2))])
List( 2 4 6 )


Example: iteration

-> (val ms (select: ns [block (n) (= 0 (mod: n 2))]))
List( 2 4 6 )
-> (do: ms [block (m) (print 'element) (print space)
(print 'is) (print space)
(println m)])
element is 2
element is 4
element is 6
nil
->


Functional code: forms of data

(define app (f xs)
(if (null? xs)
'do-nothing
(begin
(f (car xs))
(app f (cdr xs)))))

Replace interrogation: dynamic dispatch

Design process still works:

1. Each method defined on a class

2. Class determines

• How object is formed (class method)
• From what parts (instance variables)

Each form of data gets its own method!

Object-oriented code: dynamic dispatch

Instead of (app f xs), we have

(do: xs f-block)

What happens if we send “do f” to the empty list?

What happens if we send “do f” to a cons cell?

Dynamic dispatch revealed

Sending do: to the empty list:

  (method do: (aBlock) nil)
; nil is a global object

Sending do: to a cons cell:

  (method do: (aBlock)
; car and cdr are "instance variables"
(value aBlock car)
(do: cdr aBlock))

What’s missing? if!

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

Block Examples

-> (val twice [block (n) (+ n n)])

-> (value twice 3)
6
-> (val delayed {(println 'hello) 42})

-> delayed

-> (value delayed)
hello
42


Booleans use continuation-passing style

• Blocks delay evaluation

Boolean example: minimum

-> (val x 10)
-> (val y 20)
-> (ifTrue:ifFalse: (<= x y) {x} {y})
10


Booleans implemented with two classes True and False

• one value apiece

### Method dispatch in the Booleans

Board - Method dispatch

1. Consider the class of the receiver

2. Is the method with that name defined?

3. If so, use it

4. If not, repeat with the superclass

Run out of superclasses?

“Message not understood”

Dispatching to

(class True Boolean
[]
(method ifTrue:ifFalse: (trueBlock falseBlock)
(value trueBlock))
; all other methods are inherited
)


Each class has one of two roles

Abstract class

• Meant to be inherited from

• Some ( > 0) subclassResponsibility methods

• Examples: Boolean, Shape, Collection

Regular (“concrete”) class

• Meant to be instantiated

• No subclassResponsibility methods

• Examples: True, Triangle, List

# 22 April 2019: Inheritance. Dispatch. Numbers and magnitudes

There are PDF slides for 4/23/2019.

White cards: AMA (emphasize programming languages past, present, and future)

Final course evaluations:

• Submit screen shot
• Submit course.png and recitation.png using submit105-evals

### Plan for the week

#### Object-oriented mechanisms

Key mechanisms

• Dynamic dispatch
• Private instance variables

#### Object-oriented design

Key ideas (today, context for understanding, start h/w):

• Big protocols on small foundations
• Two roles of classes

Key ideas (next time, build on today):

• Power of dynamic dispatch
• Behavioral subtyping (“duck typing”, protocols)

Case studies related to the homework.

## Method dispatch in the Booleans

Booleans implemented with two classes True and False

• one value apiece

Board - Method dispatch

1. Consider the class of the receiver

2. Is the method with that name defined?

3. If so, use it

4. If not, repeat with the superclass

Run out of superclasses?

“Message not understood”

Dispatching to

(class True Boolean
[]
(method ifTrue:ifFalse: (trueBlock falseBlock)
(value trueBlock))
; all other methods are inherited
)


Each class has one of two roles

Abstract class

• Meant to be inherited from

• Some ( > 0) subclassResponsibility methods

• Examples: Boolean, Shape, Collection

Regular (“concrete”) class

• Meant to be instantiated

• No subclassResponsibility methods

• Examples: True, Triangle, List

## Smalltalk syntax and values

Values first:
Every value is an object.
Every class is an object!

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)

## Case study: Magnitudes and numbers

Key problems on homework

• Natural is a Magnitude

• “Large integer” is a Number

Implementation of

(class Magnitude Object
[] ; abstract class
(method =  (x) (subclassResponsibility self))
; may not inherit = from Object
(method <  (x) (subclassResponsibility self))
(method >  (y) (< y self))
(method <= (x) (not (> self x)))
(method >= (x) (not (< self x)))
(method min: (aMagnitude)
(if (< self aMagnitude) {self} {aMagnitude}))
(method max: (aMagnitude)
(if (> self aMagnitude) {self} {aMagnitude}))
)


Number methods

(method -   (y) (+ self (negated  y)))
(method abs ()  (ifTrue:IfFalse (negative self)
{(negated  self)}
{self}))
(method /   (y) (* self (reciprocal y)))

(method negative     () (<  self (coerce: self 0)))
(method nonnegative  () (>= self (coerce: self 0)))
(method strictlyPositive ()
(>  self (coerce: self 0)))


## Bonus case study 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?

# 24 April 2019: Double dispatch, collections

There are PDF slides for 4/25/2019.

More AMA’s

COURSE EVALUATIONS: upload a screen shot

Advertising: COMP 150 PLD (small class!)

• Programming-language design

### Two topics for today

• Initialization and invariants

• Information hidden and revealed; three layers

(Focus on extending open systems)

## Initialization and invariants

Example class : initialization

(class Fraction Number
[num den] ;; representation (concrete!)
;; invariants by signReduce, divReduce
(class-method num:den: (a b)
(initNum:den: (new self) a b))
(method initNum:den: (a b) ; private
(setNum:den: self a b)
(signReduce self)
(divReduce self))
(method setNum:den: (a b)
(set num a) (set den b) self) ; private
.. other methods of class Fraction ...
)


### Making open system extensible

Extra: Dealing with overflow

New law for multiplication:

(* small-1 small-2) =
(mulSmall:withOverflow:
small-1
small-2
{(* (asLargeInteger small-1) small-2)})

Block is exception block run on overflow

Method is primitive, defined with

  (method mulSmall:withOverflow:
primitive mul:withOverflow:)

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

## Bonus case study 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?

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