Lecture notes for COMP 105 (Programming Languages)

Table of Contents

25 Jan 2016: Introduction to Comp 105

Handout: 105 Tip Sheet

Why so many languages?

Topic of study: the stuff software is made of

Conclusion: make it easier to write programs that really work

Your language can make you or break you. - Compiler assignments at Princeton

Optional reading

Cultural enrichment: Paul Graham, especially the "Blub paradox"

What this course isn't

Reusable Principles

What if the course were called "Cooking"?

The same thing for programming languages:

What this course is

What can you get out of Comp 105?

If you're going to enjoy the course,

How will it work?

Intellectual tools you need to understand, evaluate, and use languages effectively

Notations of the trade (source of precision, further study)

Learn by doing:

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

Great languages begin with great features

Language shapes your thinking

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

You'll choose features, and therefore languages, to fit your needs

Some are more powerful than others

In Comp 105,

What are the great ideas?

To say more with less (expressive power):

To promote reliability and reuse:

Describing it all precisely:

Course logistics and administration

You must get Norman's book (both volumes)

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


Homework will be frequent and challenging:

Both individual and pair work:

Arc of the homework looks something like this:

Assignment Difficulty
impcore one star
opsem two stars
scheme three stars
hofs four stars

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

Lesson: don't make decisions based on the first couple of homeworks!

The role of lectures

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


Questions and answers on Piazza

Other policies and procedures on the web

What am I called?

Call me "Kathleen," "Professor Fisher", or "Profesor."

Introducing our common framework

Goal: eliminate superficial differences

Imperative programming with an IMPerative CORE:

Exercise: all-fours?

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

Code Note

Impcore variable definition


(val n 99)


int n = 99;

Also, expressions at top level (definition of it)

Impcore expressions

No statements means expression-oriented:

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

Each one has a value and may have side effects!

Functions are primitive (+ - * / = < > print)
or defined with (define f ...).

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

Scoping rules for Impcore

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

Names known in "environments"

Ways to talk about meanings of names:

Impcore vars in 2 environments: globals, formals

There are no local variables

Functions live in their own environment (not shared with variables)

Environmental abuse

Abuse of separate name spaces:

-> (val f 33)
-> (define f (x) (+ x x))
-> (f f)

Recursion: a review

Ways a recursive function could decompose a natural number n.

  1. Peel back one (Peano numbers):

    n = 0
    n = m + 1,    m is also a natural number
  2. Split into two pieces:

    n = 0
    n = k + (n - k)    0 < k < n   (everything gets smaller)
  3. Sequence of decimal digits (see study problems on digits)

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

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

27 Jan 2016: Introduction to Semantics

Handout: 105 Impcore Semantics, Part 1

Discussion: Two things you learned last class.


Question: How do we define the meaning of a program?

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

Answer: Inductively


Programming-languages people are wild about compositionality.

Example of compositionality: syntax (grammar)

Programming languages more orderly than natural language.

Example of non-compositionality


Question: What do we assign meaning to?

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

Question: How can we represent all while loops?

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


As a data structure:

ASTs, Environments, and Operational Semantics

Norman Ramsey and Geoff Mainland put together some Beamer slides explaining operational semantics for Impcore.

1 Feb 2016: Semantics Review and Metatheory

Handout: 105 Impcore Semantics, Part 2

Review operational semantics of function application and work through a simple derivation using the Beamer slides on operational semantics.


We'll use some Beamer slides on Metatheory that Norman Ramsey put together.

Examples of using metatheory

TeX slide


TeX slide

Formalizing when an expression contain set

We can just look at the syntax, or we can make a proof system:

TeX slide

and also

TeX slide

Notice that set is the only construct that changes the environment.

3 Feb 2016: Intro to Scheme

Where have we been?

A new way of thinking about recursion

Structure of the input drives the structure of the code.

To discover recursive functions, write algebraic laws:

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

Which direction gets smaller?


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

Another example:

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

Can you find a direction in which something gets smaller?


(define exp (x n) 
  (if (= n 0) 
      (* x (exp x (- n 1)))))

Lots of new math

No new programming-language ideas

Programming with assignments etc

Where are we going?

Recursion and composition:

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

Introduction to Scheme

Question 2: what are the values?

Two new kinds of data:

Picture of a cons cell: (cons 3 (cons ( 2 '())))

Scheme Values

Values are S-expressions.

An S-expression is either

A list of S-expressions is either

S-Expression operators

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

N.B. creators + producers = constructors

Examples of S-Expression operators

(cons 'a '()) also written '(a)

(cons 'b '(a))

(cons 'c '(b a))

(null? '(c b a)) equals #f

(cdr '(c b a) equals '(b a)

(car '(c b a) equals 'c

The symbol ' is pronounced "tick." It indicates that what follows is a literal.

Your turn!

What is the representation of

'((a b) (c d))

which can be alternatively written

cons( (cons a (cons b '())) cons( (cons c (cons d '())) '())

What is the representation of

cons('a 'b)

Contrast this representation with the one for

cons('a '())

Both of these expressions are S-expressions, but only cons('a '()) is a list.

8 Feb 2016: More Scheme


Homework 1 grades have been mailed out. See Jerett or Jared if you have questions about grading.

Homework 2 is due tonight at midnight.

Homework 3 is available on the website. It is due Wed, Feb 17 at 6pm.


Subset of S-Expressions.

Can be defined via inference rules:

TeX slide

TeX slide

Constructors: '(),cons

Observers: null?, pair?, car, cdr (also known as "first" and "rest", "head" and "tail", and many other names)

Why are lists useful?

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

Algebraic laws of lists:

(null? '()) == #t
(null? (cons v vs)) == #f
(car (cons v vs)) == v
(cdr (cons v vs)) == vs

Combine creators/producers with observers

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

Recursive functions for recursive types

Any list is therefore constructed with '() or with cons applied to an atom and a smaller list.

Example: length

Algebraic Laws for length

length '() = 0
length (cons x xs) = 1 + length xs


(define length (x)
    (if (null? x)
        (+ 1 (length (cdr x)))))

Algebraic laws to design list functions

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

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

The underlying operations are append, cons, and snoc. Which ..'s are which?

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)


  1. IH ('())

  2. If a in A and IH(as) then IH (cons a as)


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

Claim: Cost (append xs ys) = |xs|

Proof: By induction on the structure of xs.

Base case: xs = '()

 (append '() ys) returns ys with 0 allocated cons cells. 

Induction case: xs = (cons z zs)

 car xs = z  and  cdr xs = zs and |xs| = 1 + |zs|
 cost (append (cons z zs) ys)) = 
 cost (cons z (append zs ys)) = 
 1 + cost (append zs ys) = 
    By IH, cost (append zs ys) = |zs|
 1 + |zs| =

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

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

The method of accumulating parameters

Let's try a new algebraic law:

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

The code

          *** Reversal by accumulating parameters ***
(define revapp (xs zs)
   (if (null? xs) zs
       (revapp (cdr xs) 
               (cons (car xs) zs))))

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

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

Parameter zs 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 Braker) 
               (Instructor Fisher)))
    -> (val ksf (bind 'Office 'Halligan-205
                (bind 'Courses '(105)
                (bind 'Email 'comp105-staff '()))))
    ((Email comp105-staff) 
     (Courses (105)) 
     (Office Halligan-205))
    -> (find 'Office ksf) 
    -> (find 'Favorite-food ksf)


Algebraic laws of association lists

          *** Laws of assocation lists ***
(find k (bind k v l)) = v
(find k (bind k' v l)) = (find k l), provided k != k'
(find k '()) =  '() --- bogus!

10 Feb 2016: Let and Lambda


Handy new feature of Scheme: let binding

          *** Introduce local names into environment ***
    (let ((x1 e1)
          (xn en))

Evaluate e1 through en, bind answers to x1, ... xn

Also let* (one at a time) and letrec (local recursive functions)

Note that we really 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:

          *** What McCarthy should have done ***
(let ((val x1 e1)
      (val xn en))

From Impcore to uScheme

Things that should offend you about Impcore:

All these problems have one solution: lambda

Anonymous, first-class functions

From Church's lambda-calculus:

(lambda (x) (+ x x))

"The function that maps x to x plus x"

At top level, like define. (Or more accurately, define is a synonym for lambda that also gives the lambda a name.)

In general, \x.E or (lambda (x) E)

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

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.

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)
        ((x-to-the-n-minus-k (lambda (x) 
                                (- (exp x n) k))))
-> (val x-cubed-minus-27 (to-the-n-minus-k 3 27))
-> (x-cubed-minus-27 2)

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)

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)
       (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))                                    
-> (findzero (to-the-n-minus-k 2 16))

Your turn!!

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

          *** Lambda answers ***
(define conjoin (p? q?)
   (lambda (x) (if (p? x) (q? x) #f)))

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

(val c-p-e (conjoin prime? even?))
(val d-p-o (disjoin 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

Escaping functions

"Escape" means "outlive the function in which the lambda was evaluated."

We have already seen an example:

          *** An ``escaping'' function ***
-> (define to-the-n-minus-k (n k)
      (lambda (x) (- (exp x n) k)))

Where are n and k stored???

Picture of activation record for to-the-n-minus-k with n and k being popped.

Closures represent escaping functions:
TeX slide

An example:

          *** What's the closure for conjunction? ***
(define conjoin (p? q?)
   (lambda (x) (if (p? x) (q? x) #f)))

Closure for conjunction:
TeX slide

Higher-order functions!

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

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

Another algebraic law, another function:

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

          *** Functions create new functions ***
-> (define o (f g) (lambda (x) (f (g x))))
-> (define even? (n) (= 0 (mod n 2)))
-> (val odd? (o not even?))
-> (odd? 3)
-> (odd? 4)

Another example: (o not null?)


Currying converts a binary function f(x,y) to a function f' that takes x and returns a function f'' that takes y and returns the value f(x,y).

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

          *** Classic functional technique: Currying ***
-> (val positive? (lambda (y) (< 0 y)))
-> (positive? 3)
-> (val <-c (lambda (x) (lambda (y) (< x y))))
-> (val positive? (<-c 0)) ; "partial application"
-> (positive? 0)

Curried functions take their arguments "one-at-a-time."

          *** What's the algebraic law for `curry`? ***

     ...   (curry f) ...    =  ... f ...

     Keep in mind: 
     All you can do with a function is apply it!

     (((curry f) x) y) = f (x, y)

No need to Curry by hand!:
TeX slide

Your turn!!

          *** Exercises ***
-> (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

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

Bonus content: Lambda as an abstraction barrier

          *** Bonus content: vulnerable variables? ***
-> (val seed 1)
-> (val rand (lambda ()
      (set seed (mod (+ (* seed 9) 5) 1024)))))
-> (rand)
-> (rand)
-> (set seed 1)
-> (rand)

Q: What's the problem with this approach?

A: The seed is exposed to the end user, who can break the abstraction of the rand function.

          *** Bonus: Lambda as abstraction barrier! ***
-> (val mk-rand (lambda (seed)
     (lambda ()
       (set seed (mod (+ (* seed 9) 5) 1024))))))
-> (val rand (mk-rand 1))
-> (rand)
-> (rand)
-> (set seed 1)
error: set unbound variable seed
-> (rand)

17 February 2016: Higher-order functions


Opsem grades have been mailed

Scheme homework due tonight at 6pm

HOFs homework due Sunday, Feb 28 at 11:59pm


Reasoning about Functions

Useful Higher-Order Functions

Tail Calls

Reasoning about functions

Truth about S-expressions and functions consuming functions

Q: Can you do case analysis on a function?

A: No!

Q: So what can you do then?

A: Apply it!

Reasoning principles

Recursive function consuming A is related to proof about A

Higher-Order Functions

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

Goal: Capture common patterns of computation or algorithms

Fold also called reduce, accum, a "catamorphism"

List search: exists?

Algorithm encapsulated: linear search

Example: Is there a even element in the list?

Algebraic laws:

(exists? p? '())          == ???
(exixts? p? '(cons a as)) == ???

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

          *** Defining exists? ***
-> (define exists? (p? xs)
      (if (null? xs)
          (if (p? (car xs)) 
              (exists? p? (cdr xs)))))
-> (exists? pair? '(1 2 3))
-> (exists? pair? '(1 2 (3)))
-> (exists? ((curry =) 0) '(1 2 3))
-> (exists? ((curry =) 0) '(0 1 2 3))

TeX slide

List selection: filter

Algorithm encapsulated: Linear filtering

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

Algebraic laws:

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

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

          *** Defining filter ***
-> (define filter (p? xs)
     (if (null? xs)
       (if (p? (car xs))
         (cons (car xs) (filter p? (cdr xs)))
         (filter p? (cdr xs)))))
-> (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)

          *** Composition Revisited: List Filtering ***
-> (val positive? ((curry <) 0))
-> (filter positive?         '(1 2 -3 -4 5 6))
(1 2 5 6)
-> (filter (o not positive?) '(1 2 -3 -4 5 6))
(-3 -4)

TeX slide

"Lifting" functions to lists: map

Algorithm encapsulated: Transform every element

Example: Square every element of a list.

Algebraic laws:

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

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

          *** Defining map ***
-> (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 ((curry *) 100) '(5 6 7))
(500 600 700)
-> (val square* ((curry map) (lambda (n) (* n n))))
-> (square* '(1 2 3 4 5))
(1 4 9 16 25)

TeX slide

The universal list function: fold

Algebraic laws for foldr:
TeX slide

foldr takes two arguments:

Example: foldr plus zero '(a b)

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

Code for foldr:
TeX slide

Another view of operator folding:
TeX slide

In-class exercise

TeX slide

Wait for it:
TeX slide

TeX slide

Tail calls

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

A tail call is a call in tail position.

Important for optimizations: Can change complexity class.

What is tail position?

Tail position is defined inductively:

Idea: The last thing that happens

Anything in tail position is the last thing executed!

Key idea is tail-call optimization!

Tail-call optimization:
TeX slide

Example of tail position:
TeX slide

Example of tail position:
TeX slide

Example: reverse '(1 2)

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

Call stack:

reverse '() 
reverse '(2)
reverse '(1 2)

Answer: Linear in the length of the list

Another example of tail position:
TeX slide

Another example of tail position:
TeX slide

Example: revapp '(1 2) '()

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

Call stack: (each line replaces previous one)

revapp '(1 2) '() --> revapp '(2) '(1) --> revapp '() '(2 1)

Answer: Constant

TeX slide

Answer: a goto!!

Think of "tail call" as "goto with arguments"

18 Feb 2016: Continuations


A continuation is code that represents "the rest of the computation."

Different coding styles

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

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

Uses of continuations


How functions finish:
TeX slide

Motivating Example: From existence to witness

Design Problem: Missing Value:
TeX slide


Bad choices:

Good choice:

Solution: A New Interface:
TeX slide

          *** Coding \lit{witness} with continuations ***
(define witness-cps (p? xs succ fail)
   (if (null? xs)
       (let ((x (car xs)))
         (if (p? x)
             (succ x)
             (witness-cps p? (cdr xs) succ fail)))))

``Continuation-Passing Style'':
TeX slide

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

Answer: Constant

          *** Example Use: Instructor Lookup ***
-> (val 2016s '((Fisher 105)(Hescott 170)(Chow 116)))
-> (instructor-info 'Fisher 2016s)
(Fisher teaches 105)
-> (instructor-info 'Chow 2016s)
(Chow teaches 116)
-> (instructor-info 'Souvaine 2016s)
(Souvaine is-not-on-the-list)

Instructor Lookup: The Code:
TeX slide

Instructor Lookup: The Code:
TeX slide

Instructor Lookup: The Code:
TeX slide

Instructor Lookup: The Code:
TeX slide

Extended Example: A SAT Solver

          *** Exercise: Find a satisfying assignment if one exists ***
(val f1 '(and x y z w p q (not x)))

(val f2 '(not (or x y)))

(val f3 '(not (and x y z)))

(val f4 '(and (or x y z) 
              (or (not x) (not y) (not z))))

Wait for it ...:
TeX slide

          *** Satisfying assignments ***
(val f1 '(and x y z w p q (not x))) ; NONE

(val f2 '(not (or x y))) 
                  ; { x |-> #f, y |-> #f }

(val f3 '(not (and x y z))) 
                  ; { x |-> #f, ... }
(val f4 '(and (or x y z) 
              (or (not x) (not y) (not z))))
              ; { x |-> #f, y |-> #t, ... }

Solving a Literal

start carries a partial truth assignment to variables current

Box describes how to extend current to make a variable, say x, true.

Case 1: current(x) = #t

Call success continuation with current

Pass fail as resume continuation (argument to success)

Case 2: current(x) = #f

Call fail continuation

Case 3: x not in current

Call success cotinuation with current{x -> #t}

Pass fail as resume continuation

Solving a Negated Literal (Your turn)

start carries a partial truth assignment to variables current

Box describes how to extend current to make a negated variable, say not x, true.

Case 1: current(x) = #f

Call success continuation with current

Pass fail as resume continuation (argument to success)

Case 2: current(x) = #t

Call fail continuation

Case 3: x not in current

Call success cotinuation with current{x -> #f}

Pass fail as resume continuation

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.

22 Feb 2016: Scheme Semantics and Wrap-up Discussion


Scheme grades have been mailed

HOFs homework due Sunday, Feb 28 at 11:59pm


Scheme Semantics

Scheme as it really is

New Syntax, New Values, New Environment, New Semantics

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

Key changes from Impcore:

{New Abstract Syntax}:
TeX slide

{New Evaluation Judgment}:
TeX slide

It's not precisely true that rho never changes.
New variables are added when they come into scope.
Old variables are deleted when they go out of scope.
But the location associated with a variable never changes.

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


{New Evaluation Rules}:
TeX slide

Board: Picture of environment pointing to store.

Questions about Assign:


{Semantics of Lambda}:
TeX slide

Function Application

{Applying Closures}:
TeX slide

Questions about ApplyClosure:

{Locations in Closures}:
TeX slide

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

Closure Optimizations


Which let is which and why?

Handout: Which let is which?

24 Feb 2016: Scheme Wrap-up; ML Intro


Midterm: Wednesday, March 2, in-class. You may bring one-page of notes.

Monday's Class: Midterm Review. Bring Questions! In-class evaluations.


Scheme Wrap-up

Intro to ML

Lisp and Scheme Retrospective

{uscheme and the Five Questions}:
TeX slide

Common Lisp, Scheme


Down sides:

Bottom line: it's all about lambda

Bonus content: Scheme as it really is

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


Real Scheme: Macros

A Scheme program is just another S-expression

Conditional expressions

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


Real 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

Introduction to ML

Apply your new knowledge in Standard ML:

Lectures on ML:

  1. Algebraic types and pattern matching
  2. Exceptions
  3. An introduction to types

Meta: Not your typical introduction to a new language

ML Overview

Designed for programs, logic, symbolic data

Theme: Precise ways to describe data

ML = uScheme + pattern matching + exceptions + static types

uScheme -> ML


(cons x xs)


(lambda (x) e)

or and

#t #f

(let (x e1) e2)


x :: xs

[] or nil

fn x => e

orelse andalso

true false

let val x = e1 in e2 end

Three new ideas

  1. Pattern matching is big and important. You will like it.
  2. Exceptions are easy
  3. Static types get two to three weeks in their own right.

Pattern matching facilitates case analysis.

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

And lots of new concrete syntax!


The length function.

ML---The Five Questions

Syntax: definitions, expressions, patterns, types

Values: num/string/bool, record/tuple, algebraic data

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)

A note about books

Ullman is easy to digest

Ullman is clueless about good style


Algebraic data types


Defining algebraic types


Exegesis (on board):

29 Feb 2016: Midterm Review



Midterm Review

Plan on:

Recursion and Induction

Understanding a language: Key Questions

  1. What is the abstract syntax?

  2. What are the values?

  3. What are the environments?

  4. How does evaluation happen?

  5. What is the initial basis?

  6. What are the types?

First-class functions

Local bindings

Data structures and associated operations

Cost Models and Optimizations

Operational semantics

7 Mar 2016: Algebraic Data Types; Case Statements; Exceptions

pdf slides

Algebraic Datatypes

Enumerated types

Datatypes can define an enumerated type and associated values.

datatype suit = heart | diamond | spade | club

Here suit is the name of a new type.

The data constructors heart, dimaond, spade, and club are the values of type suit.

Data constructors are separated by vertical bars.

Pattern matching

Datatypes are deconstructed using pattern matching.

fun toString heart = "heart"
  | toString diamond = "diamond"
  | toString spade = "spade"
  | toString club = "club"

val suitName = toString heart

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

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

IntTree is the name of a new type.

There are two data constructors: Leaf and Node.

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

Building values with constructors

We build values of type IntTree using the associated constructors: (Draw on board)

 val tempty = Leaf
 val t1 = Node (1, tempty, tempty)
 val t2 = Node (2, t1, t1)
 val t3 = Node (3, t2, t2)

What is the in-order traversal of t3?


What is the pre-order traversal of t3?


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

IntTree is monomorphic because it has a single type.

Note though that the inOrder and preOrder functions only cared about the structure of the tree, not the payload value at each node.

But wait, there's still more: Polymorphic datatypes!

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

datatype 'a tree = Child | Parent of 'a * 'a tree * 'a tree

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


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

It is introduced on the left-hand of the = sign. References on the right-hand side are types.

Child and Parent are data constructors.

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

When given a value of type 'a and two 'a 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.


Datatype declarations introduce names into:

  1. the type environment: suit, IntTree, tree

  2. the value environment: heart, Leaf, Parent


Datatype declarations are inherently inductive:

Datatype Exercise

TeX slide

Wait for it ...

          *** Exercise answers ***
datatype sx1 = ATOM1 of atom
             | LIST1 of sx1 list

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

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

At top level, fun better than case

When possible, write

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

case works for any datatype

 fun toStr t = 
     case t 
       of Leaf => "Leaf"
        | Node(v,left,right) => "Node"

But often pattern matching is better style:

 fun toStr' Leaf = "Leaf"
   | toStr' (Node (v,left,right)) = "Node"

Talking type theory: Introduction and elimination constructs

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

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

Types and their uses:
Type Produce Consume
Introduce Eliminate
arrow (function) Function definition or Lambda (fn) Application
algebraic datatype Apply constructor Case or Pattern match
tuple (e1, ..., en) Case or Pattern match!

Tuple Pattern Matching

val (x,y) = (1,2)

val (left, pivot, right) = split xs

val (n,xs) = (3, [1,2,3])

val (x::xs) = [1,2,3]

val (_::xs) = [1,2,3]

Exceptions: Handling unusual circumstances


Informal Semantics:

Bonus Content: ML traps and pitfalls

ML Traps and pitfalls:
TeX slide

          *** Order of clauses matters ***

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

(* what goes wrong? *)

          *** Gotcha --- overloading ***
- 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 --- equality types:
TeX slide

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

ML from 10,000 feet:
TeX slide


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


What is a pattern?

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

Design bug: no lexical distinction between

Workaround: programming convention


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)

 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

Tuples are "usual and customary."

Mutual recursion:
TeX slide


Syntax of ML types:
TeX slide

Syntax of ML types:
TeX slide

Polymorphic types:
TeX slide

Old and new friends:
TeX slide

9 Mar 2016: Types

pdf slides



Type systems

What kind of value do we have?

Type systems classify values.

 n + 1

 "hello" ^ "world"

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

 if p then 1 else 0

Questions type systems can answer:

Questions type systems generally cannot answer:

Decidability and Type Checking

Suppose L is a Turing-Complete Language.

TP is the set of programs in L that terminate.

Wish: a type system to statically classify terminating programs:

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

But: Undecideable!

We can prove no such type system exists.


Static vs. Dynamic Type Checking

Most languages use a combination of static and dynamic checks



What is a type?

Source of new language ideas for next 20 years

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

Type System and Checker for a Simple Language

Define an AST for expressions with:

Language of expressions

Numbers and Booleans:

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 = INTTY | BOOLTY

Examples to rule out

Can't add an integer and a boolean:

3 + (3 < 99)


Can't compare an integer and a boolean

(3 < (4 = 24))

CMP (LT, LIT 3, CMP(EQ (LIT 4, LIT 24)))

Inference rules to define a type system

Rule for arithmetic operators

Informal example:

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

General form:

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

Rule for comparisons

Informal example:

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

General form:

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

Rule for literals

Informal example:

|- 14 : int

General form:

|- LIT (n) : int

Rule for conditionals:

Informal example:

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

General form:

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

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

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

Type checker in ML

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

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

Typing Rules: Contexts and Term Variables

Add variables and let binding to our language, what happens?

Extended language of expressions

Numbers and Booleans:

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 = INTTY | BOOLTY

What could go wrong with a variable?

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

Rule for var

x in domain Gamma        tau = Gamma(x) 
Gamma |- VAR x : tau

Rule for let

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

Type Checker

Type checker needs Gamma -- gives type of each "term variable".

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



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


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


This is a big chunk of what language designers do.

14 Mar 2016: Type Checking with Type Constructors

pdf slides



Where we've been and where we're going

New watershed in the homework

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

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

Monomorphic vs Polymorphic Types

Monomorphic types have "one shape."

Polymorphic types have "many shapes."

Design and implementation of monomorphic languages

Language designer's agenda:

Here's how it works:

  1. Every new variety of type requires special syntax

  2. We get three kinds of typing rules: formation, introduction, and elimination

  3. Implementation is a straightforward application of what you already know.

Question: If I add lists to a language, how many new types am I introducing?

Type formation

Examples: Well-formed types

These are types:

Examples: Not yet types, or not types at all

These "types in waiting" don't classify any terms

These are utter nonsense

Type formation rules

We need a way to classify type expressions into:

Type constructors

Technical name for "types in waiting"

Given zero or more arguments, produce a type:

More complex type constructors:

What's a good type?:
TeX slide

Type judgments for monomorphic system

Two judgments:

Monomorphic type rules

Type rules for variables:
TeX slide

Type rules for control:
TeX slide

Notice: one rule for if!!

Classic types for data structures

Product types: Both x and y:
TeX slide

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

Arrow types: Function from x to y:
TeX slide

Arrow types: Function from x to y:
TeX slide

Typical syntactic support for types

Explicit types on lambda and define:

Abstract syntax:

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

Array types: Array of x:
TeX slide

Array types continued:
TeX slide

Typing Rule Exercise

References (similar to C/C++ pointers):
TeX slide

Wait for it ...

Reference Types:
TeX slide

Coding the arrow-introduction rule

TeX slide

          *** 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 ((n, ty), g) => bind (n, ty, g))
              Gamma formals
      val bodytype = ty(Gamma', body)
      val formaltypes = 
        map (fn (n, ty) => ty) formals
  in  funtype (formaltypes, bodytype)

16 Mar 2016: Polymorphic Type Checking

pdf slides


Type System homework due Tuesday, March 29.


Monday: Typed Impcore

Today: TypedUScheme

Polymorphic Type Checking

Type formation: Composing types

Typed Impcore:

Standard ML:

Can't add new syntactic forms and new type formation rules for every new type.

Representing type constructors generically:
TeX slide

Question: How would you represent an array of pairs of booleans?:
TeX slide

Question: How would you represent an array of pairs of booleans?:
TeX slide

Well-formed types

We still need to classify type expressions into:


Type formation through kinds

Type formation through kinds:
TeX slide

Use kinds to give arities:
TeX slide

The kinding judgment:
TeX slide

Kinding rules for types:
TeX slide

Limitations of monomorphic type systems

Monomorphic types are limiting

Each new type constructor requires

Monomorphism hurts programmers too

Monomorphism leads to code duplication

User-defined functions are monomorphic:

(define int lengthI ((list int) l)
   (if (null? l) 0 (+ 1 (lengthI (cdr l)))))
(define int lengthB ((list bool) l)
   (if (null? l) 0 (+ 1 (lengthB (cdr l)))))
(define int lengthS ((list sym) l)
   (if (null? l) 0 (+ 1 (lengthS (cdr l)))))

Quantified types

Quantified types:
TeX slide

Representing quantified types

Two new alternatives for tyex:

datatype tyex
  = TYCON  of name
  | CONAPP of tyex * tyex list 
  | FORALL of name list * tyex
  | TYVAR  of name

Kinding rules for quantified types:
TeX slide

          *** Programming with these types ***

Substitute for quantified variables

-> length
<proc> : (forall ('a) (function ((list 'a)) int))
-> (@ length int)
<proc> : (function ((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
<proc> : (forall ('a) (function ((list 'a)) int))
-> (@ length bool)
<proc> : (function ((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
<proc> : 
  (forall ('a 'b) 
      (function ((function ('a) 'b) 
                 (list 'a)) 
           (list 'b)))
-> (@ map int bool)
<proc> : (function ((function (int) bool) 
                    (list int)) 
              (list bool))

Create your own!

Abstract over unknown type using type-lambda

  -> (val id (type-lambda ('a)
                (lambda (('a x)) x)))
  id : (forall ('a) ('a -> 'a)) 

'a is type parameter (an unknown type)

This feature is parametric polymorphism

Two forms of abstraction:

term type
lambda function (arrow)
type-lambda forall

Power comes at notational cost

Function composition

-> val o (type-lambda ('a 'b 'c)                                                                         

   (lambda ((('b -> 'c) f)                                                                            
            (('a -> 'b) g))                                                                           
     (lambda (('a x)) (f (g x))))))                                                                   

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

Aka o :

Type rules for polymorphism

Instantiate by substitution:
TeX slide

Generalize with type-lambda:
TeX slide

          *** A phase distinction embodied in code ***

-> (val x 3)
3 : int
-> (val y (+ x x))
6 : int

fun checkThenEval (d, (delta, gamma, rho)) =
  let val (gamma', tystring)  = elabdef (d, gamma, delta)
      val (rho',   valstring) = evaldef (d, rho)
      val _ = print (valstring ^ " : " ^ tystring)
  in  (delta, gamma', rho')

Three environments --- what happens?:
TeX slide

Three environments revealed:
TeX slide

Exercise: Three environments:
TeX slide

28 Mar 2016: Type Inference

pdf slides



Type Inference Intuition



Key Ideas:

Why Study?

New topic: Type inference:
TeX slide

          *** What type inference accomplishes ***
-> (define     double (x)       (+ x x))
double                         ;; uScheme
-> (define int double ((int x)) (+ 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) : bool list      ;; nML

Key ideas:

  1. For each unknown type, introduce a fresh type variable

  2. Enforce equality constraints

  3. Introduce type-lambda at let/val bindings

TeX slide

Let's do an example on the board

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

What do we know?

Key idea: Record the constraint in a typing judgement.

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

Example: if


Inferring polymorphic types

let val app2 = (lambda (f x y)
                    (f x)
                    (f y)))

          *** Exercise: Give the type of cc ***

let val cc = (lambda (nss) (car (car nss)))

          *** Exercise: Give the type of cc ***

let val cc = (lambda (nss) (car (car nss)))

forall 'a . 'a list list -> 'a

Formalizing Type Inference

Formalizing Type Inference

Sad news: Full type inference for polymorphism is not decidable.

Solution: Parameters have monomorphic types.

Consequence: Polymorphic functions are not first class.

          *** Hindley-Milner types ***
datatype ty
  = TYCON  of name        
  | CONAPP of ty * ty list
  | TYVAR  of name        

datatype type_scheme
  = FORALL of name list * ty

Key ideas:
TeX slide

Key ideas repeated:
TeX slide

{Type inference}:
TeX slide

{Apply rule}:
TeX slide

{Exercise: Begin Rule}:
TeX slide

{Exercise: Begin Rule}:
TeX slide

{Type inference, operationally}:
TeX slide

Writing the constraint solver

          *** Solve these constraints! ***
datatype con = ~   of ty  * ty
             | /\  of con * con
             | TRIVIAL
infix 4 ~
infix 3 /\

{Solving Constraints}:
TeX slide

When is a constraint satisfied?:
TeX slide

TeX slide

Board: which of these have solutions?

int ~ bool
int list ~ bool list
'a ~ int
'a ~ int list
'a ~ int -> int
'a ~ 'a
'a * int ~ bool * 'b
'a * int ~ bool -> 'b
'a ~ ('a, int)
'a ~ tau        (arbitrary tau)

Question: in solving tau1 ~ tau2, how many potential cases are there to consider?

Question: how are you going to handle each case?

{Solving Constraint Conjunctions}:
TeX slide

What you know and can do after this lecture

So far

After this lecture, you can write solve, a function which, given a constraint C, has one of three outcomes:

You can also write a type inferencer ty for everything except let forms. (Coming Wednesday)

30 Mar 2016: Instantiation and Generalization

pdf slides


Type Inference Homework due Wednesday, April 6.

Next Week: Kathleen at Royal Society meeting in London


Type inference, continued

Moving from type schema to types (Instantiation)

Moving from types to type schema (Generalization)

Type Inference:
TeX slide

Key Idea:
TeX slide

Judgement forms:
TeX slide

Formalizing Type Inference:
TeX slide

From Type Schema to Types

Moving between type schema and types:
TeX slide

From Type Schema to Types:
TeX slide

Why the freshness requirement?


Gamma = {fst : forall 'a 'b. 'a * 'b -> 'a, y : 'ay}

??, Gamma |- if (y, fst 2 3, 4) : ??

Imagine we ignore the freshness constraint when instantiating fst:

fst : 'ay * 'b -> 'ay

From if, we get the constraints:

'ay ~ bool

'ay ~ int

which aren't satisfiable. Which means this code would be erroneously flagged as an error.

Correct typing:

 'ay ~ bool, Gamma |- if (y, fst 2 3, 4) : int

Why the distinctnes requirement?

fst : 'a * 'a -> 'a

Gamma |- fst 2 #t

Application rule yields constraints:

'a ~ int

'a ~ bool

which aren't satisfiable. Which means this code would also be erroneously flagged as an error.

Correct typing:

Gamma |- fst 2 #t : int

From Types to Type Schema

From Types to Type Schema:
TeX slide

Generalize Function:
TeX slide

First Candidate VAL rule:
TeX slide

TeX slide

Second Candidate VAL rule:
TeX slide

VAL rule:
TeX slide

          *** Let Examples ***
(lambda (ys)
   (let ((s (lambda (x) (cons x '()))))
      (pair (s 1) (s #t))))

(lambda (ys)
   (let ((extend (lambda (x) (cons x ys))))
      (pair (extend 1) (extend #t))))

(lambda (ys)
    (let ((extend (lambda (x) (cons x ys))))
       (extend 1)))

TeX slide

TeX slide

VAL-REC rule:
TeX slide

TeX slide

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

4 Apr 2016: Object-Orientation and Smalltalk

pdf slides


Last time



Where have we been?

What about big programs?

An area of agreement and a great divide:

                      INFORMATION HIDING
                          /         \
                         /           \
                  reuse /             \ modular reasoning
                       /               \
                      /                 \
                   OBJECTS            MODULES

Two kinds of reuse:

Don't conflate them!

History of objects

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

Objects are another way to mix code and data

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

What's an object?

Agglutination containing

A lot like a closure

What is a class?

A class is a way to define objects. It provides a recipe for object construction, defining the methods (code) and specifying how to initialize the instance variables (state) via constructors.

What are objects good at?

Not really useful for building small things

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

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

What's hard about objects?

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


Why Smalltalk?

The Six Questions

Impcore syntax:
TeX slide

Smalltalk syntax:
TeX slide

Smalltalk syntax:
TeX slide

Message passing

Look at SEND

N.B. BLOCK and LITERAL are special objects.

          *** Example: A bank account ***

-> (use finance.smt)
<class FinancialHistory>
<class DeductibleHistory>
-> (val account (initialBalance: FinancialHistory 1000))
-> (deposit:from: account 400 #salary)
-> (withdraw:for: account 50 #plumber)
-> (cashOnHand account)

Protocol --- the interface to an object

Protocol is Smalltalk term of art:

Ruby dialect "duck typing" is a statement about protocols

Protocol is determined by the class of which an object is an instance

TeX slide


Every object gets not just the protocol but the implementations from its class. And a class can inherit from its superclass (more undefined terms) all the way up to class Object.

          *** Simple examples ***
-> true
-> True
<class True>
-> Object
<class Object>
-> (isNil 3)
-> (isNil nil)
-> (println nil)

6 Apr 2016: Object-orientation and Smalltalk

pdf slides


Last time


Smalltalk's Initial Basis

Blocks and Booleans

Blocks are closures

Blocks are objects

Booleans use continuation-passing style

Protocol for Booleans:
TeX slide

Booleans implemented with two classes True and False

Classes True and False:
TeX slide

Method dispatch in the Booleans

Protocol for Booleans:
TeX slide

Board - Method dispatch

To answer a message:

  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"

{ message dispatched to class }:
TeX slide


          *** Blocks manage loops ***
-> (val x 10)
-> (val y 20)
-> (whileTrue: [(<= x (* 10 y))]
      [(set x (* x 3))])
-> x

Protocol for blocks:
TeX slide


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

Subtyping mathematically:
TeX slide

Subtyping is not inheritance:
TeX slide

Double Dispatch

Typical object-orientation:

What if you need to choose code based on both receiver and argument?

Solution: method name encodes both operation and type of argument



In class Float:

(method + (anInteger) (addFloatTo: anInteger self))

In class Integer:

(method addFloatTo: (aFloat) (<<code to add an Integer and a Float>>)

Consider evaluation of:

(+ 5.5 3)

Sends + message to object 5.5 with argument 3

Sends addFloatTo: message to 3 with argument 5.5

Code to add an Integer and a Float is executed.


                        Object ===> Object's metaclass
                          /              /
                         /              /
                   Collection ===> Collection's metaclass
                       /              /
                      /              /
     students ====> Set ========> Set's metaclass
                    /              /
                   /              /
 alphanum ====> CharSet ====> CharSet's metaclass

Things of note in Smalltalk

  1. Wide interfaces, reused

  2. Algorithms smeared out over multiple classes

  3. Behavioral subtyping, aka "Duck typing"

  4. Old wine in new bottles

    • Exceptions (usage of blocks)

    • Higher-order methods

    • Polymorphic methods

  5. Initialization

  6. Double dispatch

Information Hiding and Module Systems

11 Apr 2016: Smalltalk Collections; ML Modules

pdf slides



Smalltalk collection classes

SML's Module System


Goal of objects is reuse

Key to successful reuse is a well-designed class hierarchy

``Collection hierarchy'':
TeX slide

``Collections hierarchy'':
TeX slide

Collection mutators:
TeX slide

Collection observers:
TeX slide

Collection iterators:
TeX slide

Implementing Collections

Implementing collections:
TeX slide

Reusable methods:
TeX slide

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?

Question: The addAll: method shows that the Collection class relies on subclass implementation of do: What happens if a subclass implements do: incorrectly?

{species method}:
TeX slide

{The four crucial Collection methods}:
TeX slide

Example collection - Sets

TeX slide

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!

TeX slide

{Information Hiding in Smalltalk}:
TeX slide

Information hiding using objects


(Other object-oriented languages have elaborate controls for public/private)

Information hiding, really?

Problem: inheritance violates abstraction and modularity

13 Apr 2016: ML Modules

pdf slides



Modules and separate compilation

Why modules?

Unlocking the final door for building large software systems

Modules overview

Functions of a true module system:

Real modules include separately compilable interfaces and implementations


Collect declarations

Things typically declared:

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

Roles of interfaces in programming:

The best-proven technology for structuring large systems.

Ways of thinking about interfaces

Two approaches to writing interfaces

Interface "projected" from implementation:

Full interfaces:

Module Implementations

Standard ML Modules

The Perl of module languages?

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

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

Implementations of integers

A selection...

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

ML Modules examples, part II

          *** Queues in Standard ML: A Signature ***
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)

          *** Queues in Standard ML: A Structure ***
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)

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

Exercise: Signature for a Stack

structure Stack = struct
   type 'a stack = 'a list
   exception Empty
   val empty = []
   val push = op ::
   fun pop [] = raise Empty
     | pop (tos::rest) = tos

Exercise: Signature for a Stack

signature STACK = sig
   type 'a stack 
   exception Empty
   val empty : 'a stack
   val push  : 'a * 'a stack -> 'a stack
   val pop   : 'a stack -> 'a 

          *** Dot notation to access elements ***
structure Queue :> QUEUE = struct
  type 'a queue = 'a list
  exception Empty

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

fun single (x:'a) : 'a Queue.queue = 
   Queue.put(Queue.empty, x)

Signature Matching


 structure Queue :> QUEUE = QueueI

if the principal signature of QueueI matches the ascribed signature QUEUE. Intuitively:

Signature Ascription

Signature Ascription is the process of attaching a signature to a structure.

Transparent Ascription


 structure IntLT : ORDERED = struct
   type t = int
   val le = (op <)
   val eq = (op =)

Valid: IntLT.t = int

Opaque Ascription


 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)

Not valid: 'a Queue.queue = 'a list


A Functor is a function on modules.

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

Instantiating Functors

Functor applications are evaluated at compile-time.

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

structure QueueS  = AddSingle(Queue)
structure EQueueS = AddSingle(EQueue)

where EQueue is a more efficient implementation

Sharing Constraints:
TeX slide

Why functors?:
TeX slide

20 Apr 2016: Extended SML Example

pdf slides



Extended example: Error-tracking Interpreter

Error-tracking Interpreter

An Extended Example

Why this example?

Error modules: Three common implementations (all covered in recitation)

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

          *** First Error Implementation ***
structure FirstError :> 
    ERROR where type error = string
          and type summary = string option =
    type error   = string
    type summary = string option

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

    val oneError = SOME

          *** All Error Implementation ***
structure AllErrors :>
    ERROR where type error   = string
            and type summary = string list =
    type error   = string
    type summary = error list

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

Computations Abstraction

Ambitious! (will make your head hurt a bit)

Computations either:

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)
                    |  err2 as (Err s2) => err2)
       |  err1 as (Err s1) => (case (eval e2)
                    of OK v2 => err1
                    |  err2 as (Err s2) => 
                        Err (AllErrors.<+> (s1, s2))))

          *** Exercise: DIV case ***
  | eval (DIV (e1, e2)) = 
     (case (eval e1)  
       of OK v1 => (case (eval e2) 
          of OK v2 => 
             (case v2 
               of 0 => Err (AllErrors.oneError "Div by 0.")
               | _  => OK (v1 div v2))
          |  err2 as (Err s2) => err2)
       | err1 as (Err s1) => (case (eval e2)
               of OK v2 => err1
               |  err2 as (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


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.


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 \emph{generic} 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

          *** 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) =
  val (<*>, <$>, >>=) = (Comp.<*>, Comp.<$>, Comp.>>=)
  (* Definition of Interpreter *)


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

          *** {Extend a signature with \lit{include}} ***
signature ERRORCOMP = sig
  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

          *** {Let's build \lit{ERRORCOMP}} ***
functor ErrorCompFn(structure Error : ERROR) :> 
  ERRORCOMP where type Error.error   = Error.error
              and type Error.summary = Error.summary =
  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

          *** ``Computations Abstraction" = a monad ***
Haskell has syntactic support to make 
monadic programming easier:

eval :: Exp -> Hopefully Int
eval (LIT i)     = return i
eval (PLUS  e1 e2) = do {
    v1 <- eval e1;
    v2 <- eval e2;
    return (v1 + v2)     }
eval (DIV  e1 e2) =  do {
    v1 <- eval3 e1;
    v2 <- eval3 e2;
    if v2 == 0 then Error "divby0" else return (v1 `div` v2)}

25 Apr 2016: Lambda Calculus Intro

pdf slides



Lambda Calculus Overview

Why study lambda calculus?

The world's simplest reasonable programming language

Only three syntactic forms:

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

Everything is programming with functions

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

Everything is continuation-passing style

Q: Who remembers the boolean equation solver?

Q: What classes of results could it produce?

A: success, failure

Q: How were the results delivered?

A: calling continuations

Q: How shall we do Booleans?

A: true continuation, false continuation

Coding Booleans

Booleans take two continuations:

true  = \t.\f.t
false = \t.\f.f

if M then N else P = ???   (* M N P *)

if = \b.\t.\e.b t e

Coding Pairs

Coding Lists

Coding numbers: Church Numerals

Wikipedia good: "Church numerals"

Key Idea: The value of a numeral is the number of times it applies its argument function.

Encoding natural numbers:
TeX slide

Church Numerals:
TeX slide

          *** Church Numerals in $\lambda$ ***
zero  = \f.\x.x;
succ  = \n.\f.\x.f (n f x);
plus  = \n.\m.n succ m;
times = \n.\m.n (plus m) zero;
-> four;
\f.\x.f (f (f (f x)))
-> three;
\f.\x.f (f (f x))
-> times four three;
\f.\x.f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))

Taking stock:

Question: What's missing from this picture?

Answer: We're missing recursive functions.

Astonishing fact: we don't need letrec or val-rec (Wednesday)

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

{Reduction rules}:
TeX slide


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

Board examples:

  1. Are these functions the same?

  2. Are these functions the same?


Free variables:
TeX slide

Examples of free variables:

\x. + x y        (* y is free *)

\x.\y. x         (* nothing is free *)

          *** Exercise: Free Variables ***

What are the free variables in:

  \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        

          *** Exercise: Free Variables ***
What are the free variables in:

  \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

Capture-avoiding substitution:
TeX slide


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

and never

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

Must rename the bound variable:

(\yes.\no.yes) (\time.no) tuesday
(\yes.\z.yes)  (\time.no) tuesday
(\z.\time.no)  tuesday

{Renaming of bound variables}:
TeX slide

27 Apr 2016: Lambda Calculus: Reduction and Normal Forms

pdf slides




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

Must rename the bound variable:

(\yes.\no.yes) (\time.no) tuesday
   ->   (alpha)
(\yes.\z.yes)  (\time.no) tuesday
   ->   (beta)
(\z.\time.no)  tuesday
   ->   (beta)

{Conversion/Reduction Rules}:
TeX slide

Capture-avoiding substitution:
TeX slide

Nondeterminism of conversion:

              / \
             V   V
            B     C

Now what??

Church-Rosser Theorem:
TeX slide

Normal Forms

Idea: Normal Form

A term is a normal form if

It cannot be reduced

What do you suppose it means to say

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)

Normal Forms: Code for Values:
TeX slide

Reduction strategies (your homework)

Applicative-order reduction

Given a beta-redex

(\x.M) N

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

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:
TeX slide

Normal-order reduction

Always choose leftmost, outermost redex

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

Normal-order illustration:
TeX slide

Normal-order is not your typical call-by-value semantics!

Fixed points, recursion

What solves this equation?:
TeX slide


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 (isZero? n 100 (pred n));

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

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

Exercise answers

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

f2 = \n.f2 (isZero? 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 functions ...

Recursion = Fixed point:
TeX slide

Why the term "Fixed point"?

The function g doesn't "move/change" x.

x = g x

Suppose g F = F. Proof that F is factorial.

For all n, g F n = n!, by induction:

Basis: n = 0.

F 0 = g F 0 = 1

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

Your turn:

          *** Conversion to fixed point ***

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

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

Note that: lg length = length

Fixed-point operators

A recursive function f implies there is a higher-order function g such that f = g f.

Amazing fact: Given g, we can compute f, the fixed-point of g.

One startling idea

You can define a fixed-point operator fix

Algebraic Law: fix g = g (fix g)

Use fix g to define recursive functions!

{Y combinator can implement fix}:
TeX slide

Lambda calculus in context

Why is it called a "calculus"?

What's the role of calculi in computer science:

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

2 May 2016: Comp 105 Conclusion

pdf slides



What have we done?



ML Pattern Matching

ML Exceptions

Type Systems

Type Systems: Big Idea

Static vs. Dynamic Typing

Type Systems: Big Idea

Type Systems: Mechanics

Hindley-Milner Type Inference: Big Idea

Hindley-Milner Type Inference: Mechanics

Object-Oriented Programming

Object-Oriented Programming: Big Ideas

Object-Oriented Programming: Mechanics

Module Systems

Module Systems a la SML: Big Ideas

Module Systems a la SML: Mechanics

Lambda Calculus

Lambda Calculus: Big Ideas

Lambda Calculus: Mechanics

Programming Experience

Programming Experience

Built substantial pieces of code

Where might you go from here?

Where might you go from here?




Additional Courses

Big-picture questions?

Studying for the Exam

Studying for the Exam

Other Questions?


Course feedback

In future courses


Back to class home page