6 September 2017: Introduction to Comp 105

There are PDF slides for 9/7/2017.

Handout: 105 Tip Sheet

Handout: 105 Syllabus

Handout: Experiences of successful 105 students

Handout: Homework

Video: The Big Picture

Announcements

Overview

Why so many languages?

Question: What languages have you programmed in?

There are thousands of programming languages, each unique.

Question: Why do you suppose there are so many?

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

The Blub paradox

What this course isn’t

Why not?

What this course is:

Why?

What are reusable principles?

What if the course were called “Cooking”?

The same division for programming languages:

What Programming Languages are, technically

What can you get out of Comp 105?

Students who get the most out of 105 report

Great languages begin with great features

In Comp 105,

How will we study language features?

Common Framework

Course logistics and administration

Books

Homework

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!

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

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

We provide lots of resources to help:

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

Two two bad habits to avoid:

The role of lectures

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

Recitations

Questions and answers on Piazza

Other policies and procedures on the web

What am I called?

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

ImpCore: The first language in our common framework

Exercise: all-fours?

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

Code

Impcore variable definition

Example

(val n 99)

Compare

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)
33
-> (define f (x) (+ x x))
f
-> (f f)
66

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.

11 September 2017: Introduction to Semantics

There are PDF slides for 9/12/2017.

Handout: 105 Impcore Semantics, Part 1

Today: Abstract Syntax and Operational Semantics

Discussion: Two things you learned last class.

Programming-language semantics

Semantics means meaning.

What problem are we trying to solve?

Know what’s supposed to happen when you run the code

Ways of knowing:

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

Why bother with precise semantics?

Same reason as other forms of math:

Plus, needed to build language implementation and tests

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

The idea: The skills you learn in this class will apply

Behavior decomposes

We want a computational notion of meaning.

What happens when we run (* y 3)?

We must know something about *, y, 3, and function application.

Knowledge is expressed inductively

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

By design, programming languages more orderly than natural language.

Review: Concrete syntax for Impcore

Definitions and expressions:

def ::= (define f (x1 ... xn) exp)
     |  (val x exp)                
     |  exp
     |  (use filename)            
     |  (check-expect exp1 exp2)
     |  (check-error exp)

exp ::= integer-literal      ;; atomic forms
     |  variable-name
     |  (set x exp)          ;; compound forms
     |  (if exp1 exp2 exp3)
     |  (while exp1 exp2)
     |  (begin exp1 ... expn)
     |  (function-name exp1 ... expn)

How to define behaviors inductively

Expressions only

Base cases (plural): numerals, names

Inductive steps: compound forms

First, simplify the task of definition

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

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.

Question: How can we represent all while loops?

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

Answer:

As a data structure:

In C, trees are a bit 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))

Behaviors of ASTs, part I: Atomic forms

Numeral: stands for a value

Name: stands for what?

Slide 9 

Slide 10 

``Environment’’ is pointy-headed theory

You may also hear:

Influence of environment is “scope rules”

Find behavior using environment

Recall

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

Your thoughts?

Impcore uses three environments

Global variables ξ

Functions ϕ

Formal parameters ρ

There are no local variables

Function environment ϕ not shared with variables—just like Perl

Syntax and Environments determine behavior

Behavior is called evaluation

Evaluation is

You know code. You will learn math.

Key ideas apply to any language

Expressions

Values

Rules

Rules written using operational semantics

Evaluation on an abstract machine

Idea: “mathematical interpreter”

Slide 17 

Slide 18 

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

Slide 19 

Slide 20 

Slide 21 

13 September 2017: Semantics, Syntactic Proofs, Metatheory

There are PDF slides for 9/14/2017.

Handout: Impcore expression rules

Announcements

Today

Last Time

Both math and code on homework

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

Slide 1 

Slide 2 

Slide 3 

Slide 4 

Slide 5 

Slide 6 

Slide 7 

Slide 8 

Slide 9 

Slide 10 

Questions:

Slide 11 

Using Operational Semantics

The big idea:

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

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

Code example

  (define and (p q)
    (if p q 0))

  (define digit? (n)
    (and (<= 0 n) (< n 10)))

Suppose we evaluate (digit? 7)

Exercise:

  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?

Slide 12 

What is the result of (digit? 7)?

How do we know it’s right?

From rules to proofs

What can a proof tell us?

Slide 13 

Judgment is valid when ``derivable’’

Special kind of proof: derivation

A form of “syntactic proof”

Recursive evaluator travels inductive proof

Root of derivation at the bottom (surprise!)

Build

First let’s see a movie

Example derivation (rules in handout)

Slide 16 

Slide 17 

Slide 18 

Slide 19 

Slide 20 

Slide 21 

Slide 22 

Slide 23 

Slide 24 

Slide 25 

Slide 26 

Slide 27 

Slide 28 

Slide 29 

Building derivations

Slide 30 

Slide 31 

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

Proofs about all derivations: Metatheory

Derivations (aka syntactic proofs) enable meta-reasoning

Derivation D is a data structure

Got a fact about all derivations?

Prove facts by structural induction over derivations

Example: Evaluating an expression doesn’t change the set of global variables

Metatheorems often help implementors

More example metatheorems:

Slide 34 

Metatheorems are proved by induction

Induction over structure (or height) of derivation trees $\mathcal D$

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

Proof

Let’s try it!

Cases to try:

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

18 September 2017: Metatheory wrapup. Intro to functional programming

There are PDF slides for 9/19/2017.

Announcements

Today

Last Time

Slide 1 

Slide 2 

Slide 3 

Slide 4 

Slide 5 

Slide 6 

Slide 7 

Where are we going?

Recursion and composition:

Recursion comes from inductive structure of input

Structure of the input drives the structure of the code.

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

  1. Inductive structure
  2. Equations (“algebraic laws”)
  3. Code

To discover recursive functions, write algebraic laws:

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

Which direction gets smaller?

Code:

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

Another example:

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

Can you find a direction in which something gets smaller?

Code:

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

For a new language, five powerful questions

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

  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?

(Initial basis for μScheme on page 157)

Introduction to Scheme

Question 2: What are the values?

Two new kinds of data:

Graphically:

Picture of two cons cells

(cons 3 (cons 2 ’()))

Scheme Values

Values are S-expressions.

An S-expression is either

Many predefined functions work with a list of S-expressions

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))        equals '(b a)

 (cons 'c '(b a))      equals '(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.

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

Your turn!

  1. What is the representation of

'((a b) (c d))

which can be alternatively written

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

 `(cons (cons c (cons d '())) '()))`
  1. 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.

Picture of '((a b) (c d))

Picture of cons('a 'b)

20 September 2017: More Scheme

There are PDF slides for 9/21/2017.

Announcements

Today

Last Time

Lists

Subset of S-Expressions.

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

Slide 1 

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

Immutable data structures

Key idea of functional programming. Instead of mutating, build a new one. Supports composition, backtracking, parallelism, shared state.

Review: Algebraic laws of lists

You fill in these right-hand sides:

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

(length '()) ==
(length (cons v vs)) ==

Combine creators/producers with observers to create laws.

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

Recursive functions for recursive types

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

Example: length

Algebraic Laws for length

Code:

;; you fill in this part

Algebraic laws to design list functions

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

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

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

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

Suppose I can prove two things:

  1. IH (’())

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

then I can conclude

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

Example: The cost of append

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

Proof: By induction on the structure of xs.

Base case: xs = ’()

Inductive case: xs = (cons z zs)

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

Example: list reversal

Algebraic laws for list reversal:

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

And the code?

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

The function revapp takes two list arguments xs and ys.
It reverses xs and appends the result to ys:

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

Write algebraic laws for revapp involving different possible forms for xs.

Who could write the code?

Reversal by accumulating parameters

(define revapp (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.)

Linear reverse, graphically

We call reverse on the list '(1 2 3):

Function reverse calls the helper function revapp with '() as the ys argument:

The xs parameter isn’t '(), so we recursively call revapp with the cdr of xs and the result of consing the car of xs onto ys:

The xs parameter still isn’t '(), so we again call revapp recursively:

Still not '(), so we recurse again:

This time xs is '(), so now we just return ys, which now contains the original list, reversed!

PDF slides of revapp

25 September 2017: Let and Lambda

There are PDF slides for 9/26/2017.

Code

Announcements

Last Time

Today

Association lists represent finite maps [Not covered in class]

Implementation: List of key-value pairs

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

Picture with spine of cons cells

Functions car, cdar, caar, cadar can help navigate.

Recall that the left box in a cons cell is the address and the right box is the data. Read the a as “address” and the d as “data” from right to left.

In association lists, these operations correspond to

A-list example

    -> (find 'Building 
             '((Course 105) (Building Robinson) 
               (Instructor Fisher)))
    Robinson
    -> (val ksf (bind 'Office 'Halligan-242
                (bind 'Courses '(105)
                (bind 'Email 'comp105-staff '()))))
    ((Email comp105-staff) 
     (Courses (105)) 
     (Office Halligan-242))
    -> (find 'Office ksf) 
    Halligan-242
    -> (find 'Favorite-food ksf)
    ()

Notes:

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!

Handy new feature of Scheme: let binding

Introduce local names into environment

    (let ((x1 e1)
          ...
          (xn en))
        e)

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

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

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

Syntax McCarthy should have used

(let ((val x1 e1)
      ...
      (val xn en))
   e)

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.

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.

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

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

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.

Slide 12 

An example:

What’s the closure for conjunction?

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

Slide 14 

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)
#t
-> (odd? 4)
#f

Another example: (o not null?)

Currying

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

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

Classic functional technique: Currying

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

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)

Slide 18 

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))
#t
-> (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)
14
-> (rand)
131
-> (set seed 1)
1
-> (rand)
14

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)
14
-> (rand)
131
-> (set seed 1)
error: set unbound variable seed
-> (rand)
160

27 September 2017: Higher-order functions

There are PDF slides for 9/28/2017.

Code

Announcements

Last Time

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))
#t
-> (filter  ((curry >) 3) '(1 2 3 4 5)) 
(1 2)

Today

Reasoning about code

Reasoning principle for lists

Recursive function that consumes A has the same structure as a proof about A

Reasoning principle for functions

Q: Can you do case analysis on a function?

A: No!

Q: So what can you do then?

A: Apply it!

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, or a “catamorphism”

List search: exists?

Algorithm encapsulated: linear search

Example: Is there a even element in the list?

Algebraic laws:

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


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

Defining exists?

-> (define exists? (p? xs)
      (if (null? xs)
          #f
          (or (p? (car xs)) 
              (exists? p? (cdr xs)))))
-> (exists? even? '(1 3))
#f
-> (exists? even? '(1 2 3))
#t
-> (exists? ((curry =) 0) '(1 2 3))
#f
-> (exists? ((curry =) 0) '(0 1 2 3))
#t

Slide 4 

Your turn: Does everything match: all?

Example: Is every element in a list even?

Algebraic laws:

(all? p? '())          == ???
(all? p? '(cons a as)) == ???


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

Defining all?

-> (define all? (p? xs)
      (if (null? xs)
          #t
          (and (p? (car xs)) 
               (all? p? (cdr xs)))))

-> (all? even? '(1 3)) 
#f
-> (all? even? '(2)) 
#t
-> (all? ((curry =) 0) '(1 2 3))
#f
-> (all? ((curry =) 0) '(0 0 0))
#t

Slide 6 

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)

Slide 9 

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

Slide 11 

The universal list function: fold

Slide 12 

foldr takes two arguments:

Example: foldr plus zero '(a b)

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

Slide 13 

Slide 14 

In-class exercise: Folding combine?

Slide 15 

Slide 16 

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!

Slide 18 

Slide 19 

Slide 20 

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

Slide 21 

Slide 22 

Example: revapp '(1 2) '()

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

Call stack: (each line replaces previous one)

revapp '(1 2) '() –>

revapp '(2) '(1) –>

revapp '() '(2 1)

Answer: Constant

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

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

Slide 23 

Answer: a goto!!

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

2 October 2017: Continuations

There are PDF slides for 10/3/2017.

Last Time

Announcements

Today

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

Uses of continuations

Implementation

Slide 1 

Motivating Example: From existence to witness

Slide 2 

Ideas?

Bad choices:

Good choice:

Slide 3 

Your turn: Refine the laws

(witness-cps p? xs succ fail) = (succ x)
     ; where x is in xs and (p? x)
(witness-cps p? xs succ fail) = (fail)
     ; where (not (exists? p? xs))

(witness-cps p? '() succ fail) = ?

(witness-cps p? (cons z zs) succ fail) = ?
    ; when (p? z)

(witness-cps p? (cons z zs) succ fail) = ?
    ; when (not (p? z))

Refine the laws

(witness-cps p? xs succ fail) = (succ x)
     ; where x is in xs and (p? x)
(witness-cps p? xs succ fail) = (fail)
     ; where (not (exists? p? xs))

(witness-cps p? '() succ fail) = (fail)

(witness-cps p? (cons z zs) succ fail) = (succ z)
    ; when (p? z)

(witness-cps p? (cons z zs) succ fail) = 
     (witness-cps p? zs succ fail)  
    ; when (not (p? z))

Coding with continuations

(define witness-cps (p? xs succ fail)
   (if (null? xs)
       (fail)
       (let ((x (car xs)))
         (if (p? x)
             (succ x)
             (witness-cps p? (cdr xs) succ fail)))))

Slide 7 

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

Answer: Constant

Example Use: Instructor Lookup

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

Slide 9 

Slide 10 

Slide 11 

Slide 12 

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

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

Slide 15 

Solving a Literal

start carries a partial truth assignment to variables current

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

Case 1: current(x) = #t

Call success continuation with current

Pass fail as resume continuation (argument to success)

Case 2: current(x) = #f

Call fail continuation

Case 3: x not in current

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

Pass fail as resume continuation

Solving a Negated Literal (Your turn)

start carries a partial truth assignment to variables current

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

Case 1: current(x) = #f

Call success continuation with current

Pass fail as resume continuation (argument to success)

Case 2: current(x) = #t

Call fail continuation

Case 3: x not in current

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

Pass fail as resume continuation

These diagrams (and the corresponding code) compose!

Solving A and B

Picture of 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

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

4 October 2017: Scheme Semantics

There are PDF slides for 10/5/2017.

Announcements

Today

Scheme Semantics

Last Time

New Syntax, Values, Environments, and Evaluation Rules

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

Key changes from Impcore:

Slide 1 

Slide 2 

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

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

Variables

Slide 3 

Board: Picture of environment pointing to store.

Questions about Assign:

Lambdas

Slide 4 

Function Application

Example


  (val even (lambda (x) (= 0 (mod x 2)))) 

  (val f    (lambda (y) (if (even y) 5 15)))

  (val even 3)

  (f 10)

Question: Which even is referenced when f is called?
Answer: With static scoping, it’s the predicate. With dynamic scoping it’s the one bound to 3.

Slide 6 

Questions about ApplyClosure:

Slide 7 

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

Closure Optimizations

11 October 2017: Scheme Wrap-up; ML Intro

There are PDF slides for 10/12/2017.

Handout: Which let is which?

Announcements

Today

Last Time

Lets

Which let is which and why?

Three versions of let:

Handout: Which let is which?

Lisp and Scheme Retrospective

Slide 1 

Common Lisp, Scheme

Advantages:

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

Macros!

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

Mutation

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

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

And lots of new concrete syntax!

Examples

The length function.

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) =   (* pred? not legal *)
      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]

(* Note fn x => e is syntax for lambda in SML *)

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]

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]

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 ListTooShort
fun take 0     l   = []
  | take n    []   = raise ListTooShort
  | take n (x::xs) = x::(take (n-1) xs)

val res5 = take 2 [1,2,3,4]
val res6 = take 3 [1] 
           handle ListTooShort => 
             (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     l   = l
  | drop n    []   = raise ListTooShort
  | drop n (x::xs) = (drop (n-1) xs)

val res7 = drop 2 [1,2,3,4]
val res8 = drop 3 [1] 
           handle ListTooShort => 
              (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]

Drop while

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

16 Oct 2017: Programming with constructed data and types

There are PDF slides for 10/17/2017.

Announcements

Today

Last Time

A note about books

Ullman is easy to digest

Ullman costs money but saves time

Ullman is clueless about good style

Suggestion:

Details in course guide Learning Standard ML

Foundation: Data

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

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

Algebraic Datatypes

Enumerated types

Datatypes can define an enumerated type and associated values.

datatype suit = heart | diamond | spade | club

Here suit is the name of a new type.

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

Data constructors are separated by vertical bars.

Pattern matching

Datatypes are deconstructed using pattern matching.

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

val suitName = toString heart

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

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

IntTree is the name of a new type.

There are two data constructors: Leaf and Node.

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?

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

What is the pre-order traversal of t3?

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

Deconstruct values with pattern matching

(The @ symbol denotes append in ML)

fun inOrder Leaf = []
  | inOrder (Node (v, left, right)) = 
       (inOrder left) @ [v] @ (inOrder right)

val il3 = inOrder t3

fun preOrder Leaf = []
  | preOrder (Node (v, left, right)) = 
       v :: (preOrder left) @ (preOrder right)

val pl3 = preOrder t3

IntTree is monomorphic because it has a single type.

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

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

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

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

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

Examples:

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

Things to notice about datatypes

Environments

Datatype declarations introduce names into:

  1. the type environment: suit, IntTree, tree

  2. the value environment: heart, Leaf, Parent

Inductive

Datatype declarations are inherently inductive:

Datatype Exercise

Slide 2 

Exercise answers

datatype sx1 = ATOM1 of atom
             | LIST1 of sx1 list

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

Case expressions: How we use datatypes

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"

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

Slide 7 

Tuple Pattern Matching

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

val (left, pivot, right) = split xs

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

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

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

Exceptions: Handling unusual circumstances

Syntax:

Informal Semantics:

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)
      | NotFound n        => continue (n ^ "not found")

Bonus Content: ML traps and pitfalls

Slide 9 

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

Slide 12 

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

Slide 15 

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

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

Slide 20 

Types

Slide 21 

Slide 22 

Slide 23 

Slide 24 

18 October 2017: Types

There are PDF slides for 10/19/2017.

Announcements

Today

Type systems

What kind of value do we have?

Slogan: “Types classify terms.”

 n + 1  : int

 "hello" ^ "world"  : string

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

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

Questions type systems can answer:

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.

Choices:

Static vs. Dynamic Type Checking

Most languages use a combination of static and dynamic checks

Static: “for all inputs”

Dynamic: “for some inputs”

Type System and Checker for a Simple Language

Define an AST for expressions with:

Language of expressions

    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)

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

Can’t compare an integer and a boolean

(3 < (4 = 24))

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

Inference rules to define a type system

Rule for arithmetic operators

Informal example:

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

Rules out:

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

General form:

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

Rule for comparisons

Informal example:

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

General form:

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

Rule for literals

Informal example:

|- 14 : int

General form:

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

Rule for conditionals:

Informal example:

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

General form:

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

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

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

What is a type?

Type checker in ML

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

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

Typing Rules: Contexts and Term Variables

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

Extended language of expressions

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

Review

This is a big chunk of what language designers do.

23 October 2017: Type Checking with Type Constructors

There are PDF slides for 10/24/2017.

Announcements

Last Time

Today

Functions

Introduction:

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

Elimination:

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

Where we’ve been and where we’re going

New watershed in the homework

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

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

Mechanisms:

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

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

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

Managing the set of types: Type Formation

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:

Slide 5 

Type judgments for monomorphic system

Two judgments:

Monomorphic type rules

Slide 7 

Slide 8 

Notice: one rule for if!!

Classic types for data structures

Slide 9 

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

Slide 10 

Slide 11 

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

Slide 13 

Slide 14 

Typing Rule Exercise

Slide 15 

Slide 16 

Coding the arrow-introduction rule

Slide 17 

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  funtype (formaltypes, bodytype)
  end

25 October 2017: Polymorphic Type Checking

There are PDF slides for 10/26/2017.

Announcements

Last Time

Today

Limitations of monomorphic type systems

Monomorphic types are limiting

Each new type constructor requires

Slide 2 

Notes:

Monomorphism hurts programmers too

Monomorphism leads to code duplication

User-defined functions are monomorphic:

(define int lengthI ([xs : (list int)])
   (if (null? xs) 0 (+ 1 (lengthI (cdr xs)))))
(define int lengthB ([xs : (list bool)])
   (if (null? xs) 0 (+ 1 (lengthB (cdr xs)))))
(define int lengthS ([xs : (list sym)])
   (if (null? xs) 0 (+ 1 (lengthS (cdr xs)))))

Quantified types

Slide 4 

Type formation via kinds

``’’???

Back up here—what types do we have?

Type formation: Composing types

Typed Impcore:

Standard ML:

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

Slide 7 

Slide 8 

Slide 9 

Well-formed types

We still need to classify type expressions into:

Idea: kinds classify types

one-off type-formation rules

Δ tracks type constructors, vars

Polymorphic Type Checking

Quantified types

Slide 11 

Representing quantified types

Two new alternatives for tyex:

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

Slide 13 

Programming with quantified types

Substitute for quantified variables 

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

Create your own!

Abstract over unknown type using type-lambda

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

'a is type parameter (an unknown type)

This feature is parametric polymorphism

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 rules for polymorphism

Slide 19 

Slide 20 

A phase distinction embodied in code


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

fun processDef (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')
  end

Slide 22 

Type formation through kinds

Slide 23 

Slide 24 

Slide 25 

Slide 26 

Slide 27 

Bonus content: a definition manipulates three environments

Slide 28 

Slide 29 

Slide 30 

30 October 2017: Midterm Review

There are PDF slides for 10/31/2017.

Announcements

Last Time

Today

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

ML

ML Pattern Matching

ML Exceptions

6 November 2017: Type Inference

There are PDF slides for 11/7/2017.

Announcements

Midterm: Returned at the end of class today.

Final: Thursday, December 14, 8:30 to 10:30.

HW: Type Checking due Wednesday 11/8

Today

Type Inference Intuition

Key Ideas:

Why Study?

Slide 1 

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

The compiler tells you useful information and there is a lower annotation burden.

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

How it works

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

  2. Every typing rule adds equality constraints

  3. Instantiate every variable automatically

  4. Introduce polymorphism at let/val bindings

Slide 5 

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

General form of typing judgement:

C, Gamma |- e : tau

which is pronounced “Assuming the constraints in C are true, in environment Gamma, expression e has type tau.”

Example: if

Example:

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 -> 'a1

f y implies 'a_f = 'a_y -> 'a2

Together, these constraints imply 'a_x = 'a_y and 'a1 = 'a2

begin implies result of function is 'a2

So, app2 : ('a_x -> 'a1) * 'a_x * 'a_x -> 'a1

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

we can generalize to:

forall 'a_x, 'a1 . ('a_x -> 'a1) * 'a_x * 'a_x -> 'a1

which is the same thing as:

forall 'a, 'b . ('a -> 'b) * 'a * 'a -> 'b

Exercise: Give the type of cc


let 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

Exercise: Give the type of cc


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

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

8 November 2017: Formalizing Type Inference and Instantiation

There are PDF slides for 11/9/2017.

Announcements

Last Time

Today

Formalizing type inference

Moving from type schemes to types (Instantiation)

Moving from types to type schemes (Generalization)

Formalizing Type Inference

Formalizing Type Inference

Sad news:

Solution:

Consequences:

Slide 2 

Representing Hindley-Milner types

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

datatype type_scheme
  = FORALL of name list * ty

Slide 4 

Slide 5 

Slide 6 

Slide 7 

Slide 8 

Slide 9 

What you know and can do now

Your skills so far

You can complete typeof

(Except for let forms.)

Next up: solving constraints!

Solving Constraints

Representing Constraints

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

Question: What does a solution to a set of constraints look like?

Answer: A substitution/mapping from types variables to types: θ.

Slide 12 

Examples

Which have solutions?

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

Examples

Which have solutions?

1. int        ~ bool    No
2. int list   ~ bool list   No
3. 'a         ~ int         'a |-> int
4. 'a         ~ int list    'a |-> int list
5. 'a         ~ int -> int  'a |-> int -> int
6. 'a         ~ 'a          'a |-> 'a
7. 'a * int   ~ bool * 'b   'a |-> bool and 'b |-> int
8. 'a * int   ~ bool -> 'b  No
9. 'a         ~ ('a, int)   No
10. 'a        ~ tau         depends if 'a in free-vars(tau)

Slide 15 

Slide 16 

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

Question: how are you going to handle each case?

Slide 17 

What you know and can do after this lecture

What you can do now

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

From Type Scheme to Type

Slide 19 

Slide 20 

Why the freshness requirement?

Consider

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

13 November 2017: Generalization

There are PDF slides for 11/14/2017.

Announcements

Last Time

Today

Generalization: going from types to type schemes

From Type to Type Scheme

Slide 1 

Slide 2 

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

Slide 3 

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

Slide 4 

Slide 5 

Slide 6 

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.

Slide 7 

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

Slide 9 

Let with constraints, operationally:

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

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

  3. val theta = solve C'

  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)

Slide 10 

Slide 11 

Slide 12 

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

15 November 2017: Hiding information with abstract data types

There are PDF slides for 11/16/2017.

Announcements

Last Time

Today

Where have we been?

What about big programs?

An area of agreement and a great divide:

                 INFORMATION HIDING
                     /         \
 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

Modules overview

Functions of a true module system:

Real modules include separately compilable interfaces and implementations

Interfaces

Collect declarations

Things typically declared:

Key idea: a declared type can be abstract

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

What about natural numbers?

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

   val of_int   : 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 decimals : nat -> int list
end

Signatures 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

Structures 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

Your turn! Signature for a stack

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

Your turn! 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 * 'a stack
  end

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

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

What interface with what implementation?

Maybe mixed together, extracted by compiler!

Maybe matched by name:

Best: any interface with any implementation:

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:

Signature Ascription

Ascription attaches signature to structure

Slogan: “use the beak”

Transparent Ascription

Not recommended!

Example:

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

Exposed: IntLT.t = int

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: 'a Queue.queue = 'a list

Abstract data types

How opaque ascription works

Outside module, no access to representation

Inside module, complete access to representation

Data abstraction for reuse

Abstract data types and your homework

Two-player games:

Problems abstraction must solve:

Result: a very wide interface

Abstraction design: Computer player

Computer player should work with any game, provided

Brute force: exhaustive search

Your turn! What does computer player need?

Our computer player: AGS

Any game has two key types:

  type config
  structure Move : sig
     type move
     ...  (* string conversion, etc *)
  end

Key functions use both types: 

  val possmoves : config -> Move.move list
  val makemove  : config -> Move.move -> config

Multiple games with different config, move?

Yes! Using key feature of ML: functor

20 November 2017: Functors and an Extended SML Example

There are PDF slides for 11/21/2017.

Announcements

Last Time

Today

Game interoperability with functors

functor AgsFun (structure Game : GAME) :> sig
  structure Game : GAME
  val bestmove : Game.config -> Game.Move.move option
  val forecast : Game.config -> Player.outcome
end
   where type Game.Move.move = Game.Move.move
   and   type Game.config    = Game.config
= struct
    structure Game = Game
    ... definitions of `bestmove`, `forecast` ...
  end

Functors

A functor is a function that operates on modules.

Formal parameters are declarations:

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

Combines familiar ideas:

Using Functors

Functor applications are evaluated at compile time.

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

Actual parameters are definitions

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

where EQueue is a more efficient implementation

Slide 4 

Slide 5 

Functors on your homework

Separate compilation:

Code reuse with type abstraction

ML module summary

New syntactic category: declaration

Signature groups declarations: interface

Structure groups definitions: implementation

Functor enables reuse:

Opaque ascription hides information

Extended Example: Error-tracking Interpreter

An Extended Example

Error-tracking interpreter for a toy language

Why this example?

Error modules: Three common implementations

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

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

Slide 20 

{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

27 November 2017: Object-orientation

There are PDF slides for 11/28/2017.

Announcements

Last Time

Today

Demo: circle, square, and triangle objects

Circle, Square, and Triangle Objects

Methods:

Instructions to student volunteers

Note: Mutable state is back!

Messages

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

    set-position:to: Object1 South (0,0)

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

    position: Object1 North

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

    set-position:to: Object2 South (0,2)

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

    position: Object2 North

More Messages

  1. Object 3, adjust your coordinate to place your Southwest control point at (0, 4). set-position:to: Object3 Southwest (0,4)

  2. Object 1, draw yourself on the board

    draw Object1

  3. Object 2, draw yourself on the board

    draw Object2

  4. Object 3, draw yourself on the board

    draw Object3

Key concepts of object-orientation

Key mechanisms

Private instance variables

Code attached to objects and classes

Dynamic dispatch

Key idea

Protocol determines behavioral subtyping

Class-based object-orientation

Object implementations determined by its class definition.

So, each class implicitly defines the protocol for its objects, and, dynamic dispatch is determined by object’s class.

Code reuse by sending messages around like crazy.

Example: list filter

Example: list filter

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

Slide 5 

Slide 6 

Slide 7 

Slide 8 

Blocks and Booleans

Blocks are objects

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

Boolean example: minimum

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

Slide 11 

Booleans implemented with two classes True and False

Slide 12 

Method dispatch in the Booleans

Slide 13 

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”

Slide 14 

Dispatching to 

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

Slide 16 

Slide 17 

29 November 2017: Inheritance

There are PDF slides for 11/30/2017.

Announcements

Last Time

Today

Slide 1 

Slide 2 

Your turn: Short-circuit 

(class Boolean Object
  ()
  ...
  (method not ()          
    (ifTrue:ifFalse: self {false} {true}))
  (method and: (aBlock)
    ...))

Your turn: Short-circuit 

(class Boolean Object
  ()
  ...
  (method not ()          
    (ifTrue:ifFalse: self {false} {true}))
  (method and: (aBlock)
    (ifTrue:ifFalse: self aBlock {self})))

History and overview of objects

History of objects

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

What’s an object?

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

Objects are another way to mix code and data

Agglutination containing

A lot like a closure

What are objects good at?

Not really useful for building small programs.

If you build a big, full-featured abstraction, you can 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 undrstand.

Smalltalk objects

Why Smalltalk?

The six questions:

Slide 5 

Slide 6 

Slide 7 

Message passing

Look at SEND

N.B. BLOCK and LITERAL are special objects.

Magnitudes and numbers

Key problems on homework

Slide 8 

Slide 9 

Slide 10 

Slide 11 

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

Slide 13 

Slide 14 

Slide 15 

Example class : initialization

(class Fraction Number
    (num den) ;; representation (concrete!)
    (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 ...
)

Slide 17 

Slide 18 

Slide 19 

4 December 2017: Double dispatch, collections

There are PDF slides for 12/5/2017.

Announcements

Last Time

Today

Slide 1 

Slide 2 

Slide 3 

Slide 4 

Slide 5 

Slide 6 

Slide 7 

Slide 8 

Slide 9 

Making open system extensible

Slide 10 

Slide 11 

Slide 12 

Slide 13 

Slide 14 

Slide 15 

Slide 16 

Subtyping

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

Slide 17 

Slide 18 

Slide 19 

Slide 20 

Bonus content not covered in class: Collections

Why collections?

Goal of objects is reuse

Key to successful reuse is a well-designed class hierarchy

Slide 21 

Slide 22 

Slide 23 

Slide 24 

Implementing Collections

Slide 25 

Slide 26 

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?

Slide 27 

Slide 28 

Example collection - Sets

Slide 29 

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!

Slide 30 

6 December 2017: Lambda Calculus

There are PDF slides for 12/7/2017.

Announcements

Last Time

Today

Lambda Calculus

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.

Slide 1 

Slide 2 

Church Numerals in λ

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: Recursive functions.

Astonishing fact: we don’t need letrec or val-rec

The Y-combinator = \f.(\x.f (x x))(\x.f (x x)) can encode recursion.

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

Slide 4 

Beta-reduction

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

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

Slide 5 

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

Slide 8 

Example:

(\yes.\no.yes)(\time.no) ->
\z.\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
   ->
\time.no

Slide 9 

Summary

11 December 2017: Comp 105 Conclusion

There are PDF slides for 12/12/2017.

Announce

Last Time

Today

What have we done?

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

Module Systems

Module Systems a la SML: Big Ideas

Module Systems a la SML: Mechanics

Object-Oriented Programming

Object-Oriented Programming: Big Ideas

Object-Oriented Programming: Mechanics

Lambda Calculus

Lambda Calculus: Big Ideas

Lambda Calculus: Mechanics

Slide 12 

Programming Experience

Programming Experience

Built substantial pieces of code

Where might you go from here?

Where might you go from here?

Haskell

Prolog

Ruby

Additional Courses

Big-picture questions?

Studying for the Exam

Studying for the Exam

Other Questions?

Feedback

Course feedback

In future courses

Congratulations!