9 September 2020: Introduction to Comp 105

There are PDF slides for 9/10/2020.

Handout: 105 Tip Sheet

Handout: 105 Syllabus

Handout: Experiences of successful 105 students

Handout: Lessons in program design

Introduction

My pronouns are she, her, hers.

Please call me “Kathleen,” or “Professor Fisher”

Reflection: Are all programming languages created equal?

Why we are here

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

Why it’s different from COMP 40:

• Machines haven’t really changed since 1970 (mainframes), 1980 (minicomputers), 1982 (microcomputers)
• Languages are changing all the time

What it involves:

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

Today:

• Start with technical work
• Then a little about experience and expectations

What is a programming language?

What is a PL?

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

My answer: a language with a compositional structure that has an element of run time to it.

Key idea: phase distinction

• Something you write down, which just sits there

• Something that runs

We will talk about “compile time” and “run time” (and later, type-checking time).

Key ideas: static and dynamic

The thing that you write down is syntax

What flies around at run time is values

(You know about syntax and values already—but this semester we’re going to think about them very systematically.

First three classes: new ways of thinking about stuff you already know

Check your understanding: The big picture

Check your understanding: Syntax vs. semantics

Reflection: Inductive definitions for numerals

Value structure for numerals: Induction

Example: Numerals

Numerals are syntax; Natural numbers are semantics

Numerals:

2018
73
1852

Not numerals:

3l1t3
2+2
-12

Approach 1: the cons approach

• if d is a digit then d is a numeral
• if d is a digit and n is a numeral then dn is a numeral

Approach 2: the snoc approach

• if d is a digit then d is a numeral
• if d is a digit and n is a numeral then nd is a numeral

Approach 3: the tree approach

• if d is a digit then d is a numeral
• if n1 is a numeral and n2 is a numeral then n1 n2 is a numeral

have written a list or sequence of digits as a definition. That’s good thinking, but it leaves open the problem of defining “list” or “sequence”. These definitions take care of that issue.

Check your understanding: Representations of numerals

Reflection: Natural numbers

Value structure for natural numbers: induction again

Natural numbers are semantics for numerals.

Infinite set, that we’ll define using induction.

• Base case: a digit is a nat
• Inductive case: if m is a nat and d is a digit then 10*m + d is a nat

Check your understanding: Representations of numerals

Reflection: Defining functions over natural numbers

Writing code with recursion and induction

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

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

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

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

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

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

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

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

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

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

Check your understanding: Design process

The all-fours? function

;; forms of data
;; Either a single digit d
;; OR 10 * m + d where m not equal 0

;; example inputs
(val x1 4 )
(val x2 9)
(val x3 44)
(val x4 907)
(val x5 48)

;; Pick the name now
;; Write the contract now
;; Write check assert cases now

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

;; The code!
  ;; return nonzero if and only if 
  ;; decimal rep of n can be written
  ;; using only the digit 4
(define all-fours? (n)
  (if (< n 10)
      (= n 4)
      (and (= 4 (mod n 10)) 
           (all-fours? (/ n 10)))))

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

Coding Interlude: all-fours?

Reflection: Various syntactic forms

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

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

Syntax in programming languages

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

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

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

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

(val n 99)

int n = 99;

14 September 2020: Abstract syntax and operational semantics

There are PDF slides for 9/15/2020.

Retrospective: Introduction to the study of programming languages, induction and recursion, and Impcore.

Reflection: Exploring composition in programming languages

Programming-language semantics

“Semantics” means “meaning.”

What problem are we trying to solve?

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

Ways of knowing:

• People learn from examples
• You can build intuition from words
  (Book is full of examples and words)
• To know exactly, unambiguously, you need more precision

You may recall the beginner exercise “make a peanut butter and jelly sandwich”

• You can watch and learn, but a computer can’t
• We must specify exactly what must be done.

Why bother with precise semantics?

• Prepare to program in languages you’ve never seen before
  • “X-ray glasses”
• Compare languages by translating into semantics
  • Python and JavaScript are much more similar than they look
  • C++ and Java are much different than they look
• Prove properties of programs and programming languages
  • Useful for security audits and program optimizations
• Understand what a correct language implementation must do

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 payoff: Your new skills will apply

Behavior decomposes

We want a computational notion of meaning.

What happens when we run (* y 3)?

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

Knowledge is expressed inductively

• Atomic forms: Describe behavior directly (e.g., constants, variables)
• Compound forms: Behavior specified by composing behaviors of parts

Example of domain where compositionaliy doesn’t apply: English spelling and pronunciation

• fish vs ghoti
  
• Both composed from letters, but no rules of composition guide pronunciation

Check your understanding: Principle of composition

 x = 3;               (set x 3)

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

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)

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

struct Exp {  // 'alt' combines with any field in union
    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;
    };
};

ASTs

Question: What do we assign behavior to?

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

• An AST is a data structure that represents a program.

• A parser converts program text into an AST.

Question: How can we represent all while loops?

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

Answer:

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

As a data structure:

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

  (f x (* y 3))

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

Check your understanding: AST Representations

Key question: names

Reflection: What’s in a name?

From ASTs to behaviors

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

Check your understanding: Operational semantics judgments

16 September 2020: Judgments, Rules, and Proofs

There are PDF slides for 9/17/2020.

Handout: Redacted Impcore rules

Handout: Overview of Induction

Reflection: Modeling computation in math

Rules and metatheory

Reflection: Operational semantics judgments

Check your understanding: Semantics of variables

Reflection: Mapping semantics to code

Check your understanding: C implementation of environment operations

Reflection: Using semantics to understand how programs are evaluated

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

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

Good and bad judgments

Reflection: Good and bad judgments

Proofs: Putting rules together

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

How do we know it’s right?

From rules to proofs

<– The ``Tony Hawk’’ algorithm –>

Building a derivation

Building derivations

Check your understanding: Derivation trees

21 September 2020: Derivations and metatheory

There are PDF slides for 9/22/2020.

All your operational-semantics questions are answered.

Reflection: Metatheory vs theory

Proofs about all derivations: metatheory

Reflection: Writing metatheoretic properties

Cases to try:

• Literal
• GlobalVar
• SetGlobal
• IfTrue
• ApplyUser2

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

Check your understanding: Proving metatheoretic properties

Summary and Next Steps

Theory: Operational semantics

• A “high-level assembly language”
• Justify algebraic laws
• Guide to implementation
  (Will return to formal rules about code in about a month)

Practice: For the next month, programming!

Return to algebraic laws! Lean on them!

23 September 2020: Scheme I: Recursive Programming with Lists and S-Expressions

There are PDF slides for 9/24/2020.

Retrospective: Operational Semantics

Reflection: From inference rules to recursive functions

For a new language, five powerful questions

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

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

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

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

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

Introduction to Scheme

Why Scheme?

Vehicle to study recursion and composition, two powerful programming techniques:

• Recursive functions in depth

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

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

Today: programming with lists and S-expressions using algebraic laws

Two new kinds of data:

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

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

Scheme Values

Most values are S-expressions.

An fully general S-expression is one of

• a symbol 'Halligan 'tufts

• a literal integer 0 77

• a literal Boolean #t #f

• (cons v₁ v₂), where v₁ and v₂ are S-expressions

It is very common to work with a list of S-expressions, which is either

• the empty list '()
• (cons v vs), where v is an S-expression and vs is a list of S-expressions

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

Lists: A subset of S-Expressions.

These are your linked lists from COMP 11 or COMP 15.

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

Check your understanding: S-Expressions

Reflection: Manipulating values

Understanding values through their operations

Constructors:

• Form values
• List constructors: '() and cons
• Any list is therefore constructed with '() or with cons applied to a value and a smaller list.

Observers:

• These ask, “how were you formed, and from what parts?”
• They are null?, pair?, car, and cdr (car and cdr also known as “first” and “rest”, “head” and “tail”, and many other names)

Laws of lists:

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

Check your understanding: Deconstructing lists

Why are lists useful?

• Sequences a frequently used abstraction

• Can easily approximate a set

• Can implement finite maps with association lists (aka dictionaries)

• You don’t have to manage memory

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

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

Programming with lists: The member? function

;; forms of data
;; '()
;; (cons n ns) where n is a number and 
               ns is a list of numbers

;; example inputs
(val x1 '())
(val x2 '(1 2 3 4))
(val x3 '(8))
(val x4 '(10 10))

;; Write check assert cases now

;; Algebraic Laws
;; (member? n '()) = #f
;; (member? n (cons n ns)) = #t
;; (member? n (cons n' ns)) = (member? n ns), 
                              where n' != n

;; The code!
  ;; return true if and only if 
  ;; list of numbers ms contains
  ;; number m
(define member? (m ms)
  (if (null? ms)
      (if (= m (car ms))
      (member? m (cdr ms)))))

        (check-assert (not (member? 8 '())))
        (check-assert (not (member? 8 '(1 2 3))))
        (check-assert      (member? 8 '(8)))
        (check-assert      (member? 8 '(10 7 8 12)))

Coding Interlude: member?

• Live coding: do two distinct elements sum to 16?

Programming with lists: The sum-16? function

Do two distinct list elements sum to 16?

;; forms of data
;; '()
;; (cons n ns) where n is a number and 
               ns is a list of numbers

;; example inputs
(val x5 '(6 10))
(val x6 '(3 6 12 7 8 9 10))

;; Write check assert cases now

;; Algebraic Laws
;; (sum-16? '()) = #f
;; (sum-16? (cons n ns)) = 
;;      (sum-16? ns)  OR
;;      n and an element in ns sum to 16
;;      i.e., (member?  (- 16 n) ns))


;; The code!
  ;; returns #t if and only if ms contains 
  ;; two distinct elements that sum to 16, 
  ;; where ms is a list of numbers

(define sum-16? (ms)
  (if (null? ms)
      (|| (sum-16? (cdr ms))  
       (member? (- 16 (car ms)) (cdr ms)))))

        (check-assert (not (sum-16? x1)))
        (check-assert (not (sum-16? x2)))
        (check-assert (not (sum-16? x3)))
        (check-assert (not (sum-16? x4)))
        (check-assert      (sum-16? x5)))
        (check-assert      (sum-16? x6)))

Coding Interlude: sum-16?

Reflection: Quote syntax

Check your understanding: Quoted literals

Reflection: New syntactic forms

μScheme’s new syntax

28 September 2020: First-class and higher-order functions

There are PDF slides for 9/29/2020.

Big picture:

• Think of S-expressions and lists, not pointers
• Write less code and reuse more code

Retrospective: Scheme I: Recursive programming with lists

es

Reflection: Where is there shared structure?

Functions are values

;; (sum-16? '())         = #f
;; (sum-16? (cons n ns)) =
;;      (sum-16? ns)  OR
;;      ns has an element m with n + m = 16

-> (define product-is-16? (n m) (= (* m n) 16))
product-is-16?
-> (any-two? product-is-16? '(1 2 3 4))
#f
-> (any-two? product-is-16? '(8 2))    
#t

Reflection: Shared structure

  (define sum-is-16? (n m) (= (+ m n) 16))

Implementing any-two?

;; (sum-16? '())         = #f
;; (sum-16? (cons n ns)) = (sum-16? ns)  OR
;;                         ns has an element m
;;                         with m + n = 16

;; (any-two? q? '())         == ...
;; (any-two? q? (cons y ys)) == ...

;; (sum-16? '())         = #f
;; (sum-16? (cons n ns)) = (sum-16? ns)  OR
;;                         ns has an element m
;;                         with m + n = 16

;; (any-two? q? '())         == #f
;; (any-two? q? (cons y ys)) == (any-two? q? ys) OR
;;                              ys has z with (q? y z)

;; (exists? p? '())         == ...
;; (exists? p? (cons y ys)) == ...

;; (exists? p? '())         == #f
;; (exists? p? (cons y ys)) == (|| (p? y)
;;                                 (exists? p? ys))

Check your understanding: The exists? function

Introduction to lambda

;; (any-two? q? '())         == #f
;; (any-two? q? (cons y ys)) == (any-two? q? ys) OR
;;                              (exists? q-with-y? ys)
;;               where (q-with-y? z) == (q? y z)

q-with-y? = (lambda (z) (q? y z))

;; (any-two? q? '())         == #f
;; (any-two? q? (cons y ys)) ==
;;   (|| (any-two? q? ys)
;;       (exists? (lambda (z) (q? y z)) ys))

(define any-two? (q? xs)
  ;; tell if any two elements y and z 
  ;; in order satisfy (q? y z)
  (if (null? xs)
      (|| (any-two? q? (cdr xs))
          (exists? (lambda (z) (q? (car xs) z))
                   (cdr xs)))))

Check your understanding: Lambda

(define combine (p1? p2?)
   (lambda (x) (if (p1? x) (p2? x) #f)))

(define divvy (p1? p2?)
   (lambda (x) (if (p1? x) #t (p2? x))))

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

Escaping functions

μScheme’s semantics: Overview and let

Reflection: Scheme vs Impcore

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.

Strange syntax, but simple semantics!

Key idea: don’t worry about memory

Check your understanding: meta-variables

Check your understanding: The semantics of let

Semantics of lambda

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

Check your understanding: Semantics of lambda

Semantics of function application

Questions about ApplyClosure:

• What if we used σ instead of σ₀ in evaluation of e₁?

• What if we used σ instead of σ₀ in evaluation of arguments?

• What if we used ρ_c instead of ρ in evaluation of arguments?

• What if we did not require ℓ₁, ℓ₂ ∉ dom(σ)?

• What is the relationship between ρ and σ?

Check your understanding: Semantics of application

Immutable data: its costs and benefits (not covered in class)

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

Already doing it: immutable data (append)

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

(define append (xs ys)
  ;; returns a new list that holds all
  ;; the elements of xs followed by
  ;; all the elements of ys
  ...)

(append '()         ys) == 

(append (cons z zs) ys) == 

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

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.

Structural Induction Principle for List(A)

Suppose I can prove two things:

1. IH (’())

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

then I can conclude

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

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

Proof: By induction on the structure of xs.

Base case: xs = ’()

• I am not allowed to make any assumptions.

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

  Nothing has been allocated, cost is zero

  (length xs) is also zero.

  Therefore, cost = (length xs).

Inductive case: xs = (cons z zs)

• I am allowed to assume the inductive hypothesis for zs.

  Therefore, I may assume the number of cons cells allocated by (append zs ys) equals (length zs)

  Now, the code:

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

  The number of cons cells allocated is 1 + the number of cells allocated by (append zs ys).

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

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

More functional programming (not covered in class)

List-design shortcuts

Three forms of “followed by”

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

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

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

Two lists? Four cases!

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

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

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

• But we have no snoc

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

  So cross out the law xs .. e == xs.

• Which rules look useful for writing append?

Costs of list reversal

Algebraic laws for list reversal:

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

And the code?

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

The list1 function maps an atom x to the singleton list containing x.

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

• Q: How many calls to reverse? A: n
• Q: How many calls to append? A: n
• Q: How long a list is passed to reverse? A: n-1, n-2, … , 0
• Q: How long a list is passed as first argument to append? A: n-1, n-2, … , 0
• Q: How many cons cells are allocated by call to list1? A: one per call to reverse.
• Conclusion: O(n²) cons cells allocated. (We could prove it by induction.)

The method of accumulating parameters

Write laws for

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

Who could write the code?

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

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

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

Parameter ys is the accumulating parameter.
(A powerful, general technique.)

30 September 2020: Higher-order functions

There are PDF slides for 10/1/2020.

Reflection: List functions

List search: exists?

Algorithm encapsulated: linear search

Example: Is there a number in the list?

Algebraic laws:

(exists? p? '())          == ???
(exixts? p? (cons x xs))  == ???


(exists? p? '())          == #f
(exists? p? (cons x xs))  == #t,
                             if (p? x)
(exixts? p? (cons x xs))  == exists? p? xs,
                             otherwise

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

Coding Interlude: exists?

;; (exists? p? '() = #f
;; (exists? p? (cons x xs)) = (|| (p? x) 
;;                                (exists? p? xs))

List selection: filter

Algorithm encapsulted: Filter list according to a predicate

Example: Keep positive numbers in a list.

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

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

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

Coding Interlude: filter

Reflection: Lifting functions to lists: map

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

Algorithm encapsulated: Transform every element according to argument function

Example: Square every element of a list.

Algebraic laws:

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

-> (define map (f xs)
     (if (null? xs)
       '()
       (cons (f (car xs)) (map f (cdr xs)))))
-> (map number? '(3 a b (5 6)))
(#t #f #f #f)
-> (map (lambda(x)(* x x)) '(5 6 7))
(25 36 49)

The universal list function: foldr

Algorithm encapsulated: Aggregate all elements in a list.

Example: What is the sum of the numbers in a list?

foldr takes two arguments:

• zero: What to do with the empty list.

• plus: How to combine next element with running results.

Example: foldr plus zero '(a b)

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

Check your understanding:

-> (define foldr (plus zero xs)
     (if (null? xs)
       zero
       (plus (car xs) (foldr plus zero (cdr xs)))))
-> (define combine (x a) (+ 1 a))
-> (foldr combine 0 '(2 3 4 1))

Reflection: Language design: Why the redundancy?

Currying

Deriving one-argument functions from two-argument functions

q-with-y? = (lambda (z) (q? y z))

q-with-y? = ((curry q?) y)

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


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


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

Check your understanding:

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

Composing functions

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

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

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

Coding Interlude: compose

Proofs about functions

5 Oct 2020: Costs, tail calls, and continuations

There are PDF slides for 10/6/2020.

Retrospective: Higher-order functions retrospective

Reflection: Expected performance

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

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

Where have we been, where are we going: functions

Today: costs and control flow

Costs of list reversal

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

Consider the call reverse xs and let n = |xs|.

How many stack frames are allocated for reverse and append?

How many cons cells are allocated?

• Q: How many calls to reverse? A: n
• Q: How many calls to append?
  A: n
• Q: How long is list passed to reverse?
  A: n-1, n-2, … , 0
• Q: How long is list passed as 1st arg to append?
  A: n-1, n-2, … , 0
• Q: How many cons cells are allocated by call to list1? A: one per call to reverse.
• Conclusions: (We could prove by induction.)
  • O(n) stack frames are allocated.
  • O(n²) cons cells allocated.
  • Function is quadratic.

Alarm bells should be ringing: Reversing a list should be linear!

We’ll get to a linear verson of list reversal via tail calls and the method of accumulating parameters.

Tail calls

Check your understanding: Tail Position

-> (define foldr (plus zero xs)
     (if (null? xs)
       zero
       (plus (car xs) (foldr plus zero (cdr xs)))))

Tail calls and the method of accumulating parameters

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

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

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

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


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

We’ll seee that the cost of this version is linear in the length of the list being reversed.

Parameter ys is the accumulating parameter.

Example: revapp '(1 2) '()

Call stack: (each line replaces previous one)

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

Consider the call revapp xs '() and let n = |xs|.

How many stack frames are allocated?

How many cons cells are allocated?

• Q: How many calls to revapp? A: n
• Q: How many of them are tail calls? A: n
• Q: How many stack frames are allocated for revapp? A: 1
• Q: How much work is done per call to revapp? A: constant.
• Conclusions: (We could prove by induction.)
  • O(1) stack frames for revapp are allocated.
  • O(n) cons cells allocated.
  • Function is linear in length of list being reversed.

Check your understanding: Accumulating Parameters

Continuations

Reflection: Another construct that transfers control

Check your understanding: Continuation Introduction

Motivating Example: Using continuations to signal exceptions

Reflection: Handling unusual circumstances

  (witness p? xs) == x, where (member x xs),
                        provided (exists? p? xs)

 (witness p? xs) == x, where (member x xs),
                       provided (exists? p? xs)

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

Answer: Constant

-> (val 2020f '((Fisher 105)(Monroe 40)(Chow 116)))
-> (instructor-info 'Fisher 2020f)
(Fisher teaches 105)

-> (instructor-info 'Chow 2020f)
(Chow teaches 116)

-> (instructor-info 'Votipka 2020f)
(Votipka is-not-on-the-list)

Coding Interlude: witness-cps

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


(val 2020f '((Fisher 105)(Monroe 40)(Chow 116)))


(define instructor-info (instructor classes)
  (let (
         [s  (lambda (info)    ; success continuation
                (list3 instructor 'teaches (cadr info)))]
         [f  (lambda ()        ; failure continuation
                (list2 instructor 'is-not-on-the-list))])
        (witness-cps (o ((curry =) instructor) car)
                      classes s f)))

(instructor-info 'Fisher 2020f)
(instructor-info 'Chow 2020f)
(instructor-info 'Votipka 2020f)

7 Oct 2020: Continuations for backtracking

There are PDF slides for 10/8/2020.

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

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

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

Reflection: Solving Boolean formulas

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

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

(val f3 (make-or (list2 'x 'y)))
   ; x \/ y

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

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

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

{ x |-> #f, y |-> #f }

(val f3 (make-or (list2 'x 'y)))
   ; x \/ y 

{ x |-> #t, ... }
{ y |-> #t, ... }

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

{ x |-> #f, ... }, ...

Searching via continuations: An example

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

Continuations for Search

the name of the literal in the box.

Solving a Literal

start carries a partial truth assignment to variables current

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

Case 1: current(x) = #t

Call success continuation with current

Pass fail as resume continuation (argument to success)

Case 2: current(x) = #f

Call fail continuation

Case 3: x not in current

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

Pass fail as resume continuation

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

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

Check your understanding: Solving a Negated Literal

Solving A and B

1. Solver enters A

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

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

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

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

Solving A or B

1. Solver enters A

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

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

4. If ever B is started, we’ve given up on A entirely. So B’s success and failure continuations are exactly the ones in the context.

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

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

Lisp and Scheme Retrospective

Common Lisp, Scheme

Advantages:

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

Down sides:

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

Bottom line: it’s all about lambda

• Major win
• Real implementation cost (heap allocation)

Next time: think about good and bad points

Bonus content: Scheme as it really is

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

Macros!

Conditional expressions

(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

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

12 Oct 2020: Introduction to ML

There are PDF slides for 10/13/2020.

Retrospective: Continuations

Reflection: μScheme evaluation

Introduction to ML

Meta: Apply your new knowledge in Standard ML:

• You’ve already learned (most of) the ideas
• There will be a lot of new detail
• Not your typical introduction to a new language
• Not definition before use, as in a manual
• Not tutorial, as in Ullman
• Instead, the most important ideas that are most connected to your work up to now

ML Overview

• Designed for manipulating programs, logic, and symbolic data
• Good language for implementing language features
• Good language for studying type systems
• Theme: Precise ways to describe data

Three new ideas

ML = uScheme + pattern matching + static types + exceptions

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

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.

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

And lots of new concrete syntax!

Example: The length function.

• Algebraic laws:

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

• The code:

  fun length []      = 0
    | length (x::xs) = 1 + length xs
  
  val res = length [1,2,3]

• Things to notice:

  • No brackets! (I hate the damn parentheses)

  • Function application by juxtaposition

  • Function application has higher precedence than any infix operator

  • Compiler checks all the cases (try in the interpreter)

Coding Interlude: length

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

μScheme to ML Rosetta stone

uScheme                    SML

 (cons x xs)             x :: xs

 '()                     []
 '()                     nil

 (lambda (x) e)          fn x => e

 (lambda (x y z) e)      fn (x, y, z) => e

 ||  &&                  andalso    orelse


 (let* ([x e1]) e2)      let val x = e1 in e2 end

 (let* ([x1 e1]          let val x1 = e1
        [x2 e2]              val x2 = e2
        [x3 e3]) e)          val x3 = e3
                         in  e
                         end

Check your understanding: ML Syntax

 &&                  

 (lambda (x y z) e)      

 '()                     

 ||  

 (lambda (x) e)          

 (let* ([x e1]) e2)      

 (cons x xs)             

 '()                     


 (let* ([x1 e1]          
        [x2 e2]          
        [x3 e3]) e)      

 fn (x, y, z) => e

 nil

 fn x => e

 x :: xs

 andalso    

 []

 false

 let val x = e1 in e2 end

 true   

 let val x1 = e1
     val x2 = e2
     val x3 = e3
 in  e
 end

 orelse

ML forms of data

Live coding:

(* ML's comment form *)
bool (* true, false *)
string (* "Tufts" *)
char (* #"A" *)
int  (* including negative integers, eg ~12 *)
list of int  [1,2,3]
list of bool [true, false]
ill-typed list [1, true]
pair  (1, "Halligan")
triple  (105, "Scheme", true)

Check your understanding: Simple ML Types

ML Functions

(* Can't use ? in the names of functions in ML *)
fun even x = (x mod 2 = 0)

fun map f []        = []
  | map f (y :: ys) = f y  :: map f ys

(* Anonymous functions are more verbose in ML *)
val res1 = map (fn (x) => (x + 1)) [1,2,3]

(* ML also has a case statement;
   It's not as elegant as clausal definitions. *)
(* orelse shortcircuits *)
fun exists p xs = 
    case xs 
      of [] => false
       | y :: ys => p y orelse exists p ys


val res2 = exists even [1,2,3,4]

(* Higher order functions exist in ML too *)
(* Notation (op +) converts infix to prefix *)
fun sum xs = foldr (op +) 0 [1,2,3,4]

Check your understanding: ML Functions

    filter p [] = []
    filter p (y :: ys) = 
        if p y then y :: filter p ys
               else filter p ys

fun filter p xs =
  case xs
    of [] => []
     | y :: ys => 
          if p y then y :: filter p ys
                 else filter p ys 

fun filter p [] = []
  | filter p (y :: ys) = 
       if p y then y :: filter p ys
             else filter p ys

fun filter p xs = 
     foldr (fn(x,a) => 
              if p x then (x::a) else a) 
           [] xs

New Forms of Data

Example: Binary Tree of Integers

(* LEAF and NODE are called data type constructors *)
datatype itree = LEAF
               | NODE of itree * int * itree


(* Data type constructors build data structures*)
(* and can be used in pattern matching *)
fun insert n LEAF                    = 
        NODE (LEAF, n, LEAF)
  | insert n (NODE (left, m, right)) =
        if n < m then
       NODE (insert n left, m, right)
        else if n > m then
       NODE (left, m, insert n right)
    else
       NODE (left, m, right)


(* insert is curried; 
   we might also want an uncurried version of insert *)
fun insert' (n, tree) = insert n tree

(* @ is ML's notation for appending two lists *)
fun elements LEAF = []
  | elements (NODE (left, n, right)) = 
      elements left @ (n :: elements right)

(* o is ML's composition operation *)
val isort = elements o foldl insert' LEAF
  (* uses binary-search tree for sorting *)

val result = isort [4,2,7,3,4,2,8,4,8,9];

Check your understanding: ML Data Type Introduction

datatype itree = LEAF
               | NODE of itree * int * itree

fun elements LEAF = []
  | elements (NODE (left, n, right)) = 
      elements left @ (n :: elements right)

Exceptions in ML

Example: Take from a list

(* Note use of exceptions. *)
(* And ; to sequence imperative operations *)
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!"; [])

Check your understanding: ML Exceptions

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!"; [])

find p [] = raise NotFound
find p (x::xs) = x          if p x
                 find p xs  otherwise  

exception Blank1
fun find p [] = Blank2 NotFound
  | find p (x::xs) = 
       if p x then x 
              else find p xs
val res = find even [1,3,5] 
            Blank3 NotFound => Blank4

in a course-specific video or in some other medium.

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

val res = length [1,2,3]

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

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

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

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

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]

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]

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

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

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

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

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]

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]

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

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

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

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

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]

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]

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

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

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

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

14 Oct 2020: Programming with constructed data and types

There are PDF slides for 10/15/2020.

Handout: Learning ML

be two text answer boxes, one for the C/scheme answer and one for the ML answer.

Reflection: Defining new kinds of data

Programming with Types

Foundation: Data

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

“Language support for forms of data”

• Base types: int, real, bool, char, string
• Functions: A -> B

• Constructed data:

  • Tuples: pairs A*B, triples A*B*C, etc.
  • (Records with named fields)
  • Lists and other algebraic types

  Deconstruct using pattern matching

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

Lightweight constructed data: Tuples

• Types defined wtih *: A₁ * A₂ * … * A_n

• Expressions to create: (e₁, e₂, …, e_n)

• Patterns to observe: (p₁, p₂, …, p_n)

Example (splitList from merge sort):

    let val (left, right) = splitList xs
        in  merge (sort left, sort right)
        end

Enumerated types

Datatypes can define an enumerated type and associated values.

datatype suit = HEARTS | DIAMONDS | SPADES | CLUBS

Here suit is the name of a new type.

The value constructors HEARTS, DIAMONDS, SPADES, and CLUBS are the values of type suit.

Value constructors are separated by vertical bars.

Pattern matching

Datatypes are deconstructed using pattern matching.

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

val suitName = toString HEARTS

Check your understanding: Basic Datatypes

fun isRed  HEART  = BLANK1
  | BLANK2 BLANK3 = true
  | isRed  _      = false

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

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

int_tree is the name of a new type.

There are two data constructors: LEAF and NODE.

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

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

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

It’s recursive!

Building values with constructors

We build values of type int_tree using the associated constructors:

 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

Reflection: How general is the code?

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

   fun inOrder LEAF = []
      | inOrder (NODE (v, left, right)) = 
           inOrder left @ [v] @ inOrder right

    fun preOrder LEAF = []
      | preOrder (NODE (v, left, right)) = 
           v :: preOrder left @ preOrder right

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

int_tree is monomorphic because it has a single type.

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

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

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

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

Examples:

• int tree is a tree of integers

• bool tree is a tree of booleans

• char tree is a tree of characters

• int list tree is a tree of a list of integers.

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

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

CHILD and PARENT are value constructors.

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

When given a value of type 'a and two 'a trees, PARENT produces a 'a tree

Constructors build tree values

val empty = CHILD
val tint1 = PARENT (1, empty, empty)
val tint2 = PARENT (2, tint1, tint1)
val tint3 = PARENT (3, tint2, tint2)

val tstr1 = PARENT ("a", empty, empty)
val tstr2 = PARENT ("b", tstr1, tstr1)
val tstr3 = PARENT ("c", tstr2, tstr2)

Pattern matching deconstructs tree values

fun inOrder CHILD = []
  | inOrder (PARENT (v, left, right)) = 
       (inOrder left) @ [v] @ (inOrder right)

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

Functions inOrder and preOrder are polymorphic: they work on any value of type 'a tree. 'a is a type variable and can be replaced with any type.

Environments

Datatype definitions introduce names into:

1. the type environment: suit, int_tree, tree

2. the value environment: HEART, LEAF, PARENT

Inductive

Datatype definitions inherently inductive:

• the type int_tree appears in its own definition

• the type tree appears in its own definition

Check your understanding: Defining Datatypes

datatype sx1 = ATOM of BLANK1
             | LIST of BLANK2 list

datatype sx2 = ATOM of BLANK1
             | PAIR of BLANK2 BLANK3 BLANK4

Coding interlude: Defining a datatype

Making types work for you

Type-directed programming

Common idea in functional programming: lifting

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

The type of a function tells us a lot about how to write it—the type often narrows the code down to a very few sensible choices. This technique works especially well with polymorphic functions.

Here’s the problem we’re going to solve: we have a predicate on single elements, and we want a predicate on lists of elements:

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

And here is the main tool we are going to use: for every type, we are going to be aware of how to make a value of the type (its introduction form) and what we can do with a value of the type (its elimination form).

Let’s review for the types we have:

• Arrow types: A function of any type can always be create with an explicit lambda (fn). And the only thing we can do with a function is apply it.

• Boolean: can make Booleans with true and false. We can use them in if expressions and we can pattern match on them.

• List types: Any value of list type is always made with ::.
  And to take one apart, we use pattern matching (in case or fun).

• The unknown type 'a: We have to be prepared for any 'a at all, so there’s no syntax that goes with it. Instead

  • If we want an expression of unknown type 'a, our choices are that we have a variable of 'a (maybe a parameter), or maybe we can apply a function that returns a value of 'a.

  • All we can do with a value of unknown type are the things we can do with any type: pass it to functions or store it in data structures.

Table:

     Type                 Intro                  Elim
     
      ... -> ...           fn                     application
      
      bool                true, false             if, pattern matching (case/fun)
   
      ... list            [], ::                  pattern matching (case/fun)


      'a                    ---                    ---

Let’s get started: our goal is to make a function of type

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

We can always use fun

fun lift p = _goal1

Q: What is the type of p? How do we know?

Q: What is the type of _goal1? How do we know?

Answers:

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

fun lift (p : 'a -> bool) = (_goal1 : 'a list -> bool)

Our new goal is a term of type 'a list -> bool. Which of these forms of expression is always safe and makes progress toward a goal of this type?

1. A recursive call
2. A lambda expression of the form (fn ... => ...)
3. A let expression

Our goal is an arrow type, and it is always safe to make a value of arrow type using lambda:

_goal1 = (fn xs => _goal2)

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

fun lift (p : 'a -> bool) = (fn xs => _goal2)

Q: What is the type of xs? How do we know?

Q: What is the type of _goal2? How do we know?

Answers:

_goal1 = (fn xs => _goal2)

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

fun lift (p : 'a -> bool) = (fn (xs : 'a list) => (_goal2 : bool))

Things we have

lift : ('a -> bool) -> ('a list -> bool)   [it could call itself recursively]
p : 'a -> bool
xs : 'a list

Now we have a goal of type bool and we want to use the parameter xs of type 'a list. What is the safest tactic to make progress using xs?

1. Break it down by cases, that is, ask whether it is nil or cons
2. Pass it to foldl or foldr
3. Pass it to lift p

Now we have a new goal of type bool. And we know two ways to make a value of type bool: we can return true or false. But if we choose true or false, we will have defined a function that is not very interesting, and we will have completely ignored all the parameters to lift. That is probably not a great design choice.

Is there some other way to make a bool? Some way to use what we have?

• Our p has type 'a -> bool, and that’s an arrow type, so the only thing we can do with it is apply it. But we don’t have a value of 'a to apply it to. Let’s set it aside.

• Our xs has type 'a list. This doesn’t solve our immediate goal of a bool, but since it’s a list, we can try to take it apart. We know xs is either nil or cons. So let’s fill the hold [goal2] with a case expression.

Next take:

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

fun lift (p : 'a -> bool) =
  fn (xs : 'a list) =>
     case xs
       of [ ] => _goal3 : bool
        | y :: ys => _goal4 : bool

Now instead of one hole we have two holes, each of type bool. But we have used xs, so that’s progress. What’s next? Let’s look at the first hole.

This first hole still has type bool. And we now know that xs is empty, so we have used all the information available in xs, but we still haven’t used p. Which of the following tactics is viable for fulfilling our goal of type bool? Mark all that apply.

1. Look for a value of type 'a to apply p to
2. Give up on p and fill the hole with true
3. Give up on p and fill the hole with false

• The hole _goal3 has a type bool. We know everything available to be known about xs (namely, it’s empty). All we have left is p.

  And p has type 'a -> bool, with no prospect of 'a to apply it to. But we have to fill the hole.

  Our only choices are true and false. Which would you like to pick?

Let’s flip a coin. My coin comes up true. So now we have

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

fun lift (p : 'a -> bool) =
  fn (xs : 'a list) =>
     case xs
       of [ ] => true
        | y :: ys => _goal4 : bool

Our final goal has type bool, but now we have more Booleans than we know what to do with: both p y and lift p ys. What answer best describes what we should do?

1. Ignore p y and fill the hole with lift p ys
2. Ignore lift p ys and fill the hole with p y
3. Combine the two Booleans using andalso
4. Combine the two Booleans using orelse
5. Two Booleans can be combined in 16 different ways, and they are all equally good.

We have to fill that last hole. And we have new variables y and ys. What are their types? How do we know?

y : 'a
ys : 'a list

Add them to everything we have and it’s now

lift : ('a -> bool) -> ('a list -> bool)
p : 'a -> bool
y : 'a
ys : 'a list

How can we use y and ys?

• We can apply p y and that’s an expression of bool.

• But we’d also like to use ys.

  Q: Can we use ys?

  A: Yes! We can all lift p recursively. We know it terminates because the list argument keeps getting smaller.

So now these are the things we have:

lift : ('a -> bool) -> ('a list -> bool)
p : 'a -> bool
y : 'a
ys : 'a list

p y : bool
lift p ys : bool

We have just one hole to fill, but we have two terms of type bool. If we want to use all our information, both y and ys, we’d better combine them.

Q: What are common ways to combine two Booleans?

A: Two good ways are andalso and orelse.

Q: Which one do you like here?

A: Let’s think about both choices:

• Q: Suppose we pick orelse here. How does lift behave?

  A: It always returns true

• Q: Suppose we pick andalso here. How does lift behave?

  A: Hey! It behaves just like the all function! I know that function!

Q: Nice. And here it is:

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

fun lift (p : 'a -> bool) =
  fn (xs : 'a list) =>
     case xs
       of [ ] => true
        | y :: ys => p y andalso lift p ys

Or if we pretty it up a little,

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

fun lift p xs = 
     case xs
       of [ ] => true
        | y :: ys => p y andalso lift p ys

or even

fun lift p []        = true
  | lift p (y :: ys) = p y andalso lift p ys

Making types work for you: The false case

Q: Suppose back at the empty-list step, the coin had come down differently and we had used true there. What would we want to do then?

A: I know this one! We combine two Booleans with orelse instead of andalso! That’s the exists function!

Q: Indeed:

fun lift' p []        = false
  | lift' p (y :: ys) = p y orelse lift p ys

Potential bonus content: inorder traversal of binary tree.

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

Additional language support for algebraic types: case expressions

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

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

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

Bonus content: Exceptions — Handling unusual circumstances

Syntax:

• Definition: exception EmptyQueue
• Introduction: raise e where e : exn
• Elimination: e1 handle pat => e2

Informal Semantics:

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

• Handler uses pattern matching

  e handle pat1 => e1 | pat2 => e2

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: A different explanation of ML Datatypes

Tidbits:

• The most important idea in ML!

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

Notes:

• A “suit” is constructed using HEARTS, DIAMONDS, CLUBS, or SPADES

• A “list of A” is constructed using nil or a :: as, where a is an A and as is a “list of A”

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

datatype  suit    = HEARTS | DIAMONDS | CLUBS | SPADES

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

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

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

Exegesis (on board):

• Notation 'a is a type variable

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

• Name before = introduces a new type constructor into the type environment. Type constructors may be nullary.

• Alternatives separated by bars are value constructors of the type

  • They are new and hide previous names

  • (Do not hide built-in names nil and list from the initial basis!)

  • Value constructors build constructed data

  • Value constructors participate in pattern matching

  • Complete by themselves: HEARTS, SPADES, nil

  • Expect parameters to make a value or pattern: ::, HEAP

  • The value a constructor is applied to is said to be carried

• Every val on this slide is a value constructor

• op enables an infix operator to appear in a nonfix context

• Type application is postfix

  • A list of integer lists is written: int list list

• New names into two environments:

  • suit, list, heap stand for new type constructors

  • HEARTS, CLUBS, nil, ::, EHEAP, HEAP stand for new value constructors

• Algebraic datatypes are inherently inductive (list appears in its own definition)—to you, that means finite trees

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

Bonus Content: ML traps and pitfalls

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

(* what goes wrong? *)

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

Bonus content (seen in examples)

Syntactic sugar for lists

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

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

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

Bonus content: ML from 10,000 feet

Environments

Patterns

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

Functions

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

Types

19 Oct 2020: Types

There are PDF slides for 10/20/2020.

Retrospective: Evaluating ML

Reflection: Catching errors with types

Where type systems are found:

• C#, Swift, Go
• Java, Scala, Rust (polymorphism)
• ML, Haskell, TypeScript, Hack (inference)

Our trajectory:

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

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

This “lecture”:

• Formal type system with only two types:
  • words and flags
• Type checker derived from inference rules

Next time:

• Unbounded number of types! (Formation, introduction, elimination)

Type systems

What kind of thing is it?

n + 1  : int

"hello" ^ "world"  : string

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

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

Questions type systems can answer:

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

• What is the contract of the function?

• Is each function called with the right number of arguments?
  (And similar errors)

• Who has the rights to look at it/change it?

• Is the number miles or millimeters?

Questions type systems typically do not answer:

• Can it divide by zero?

• Can it access an array out of bounds?

• Can it take the car of '()?

• Will it terminate?

Decidability and Type Checking

Suppose L is a Turing-Complete Language.

P 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. (See Comp170 for the Halting Problem)

Choices:

• Allow type checker to run forever.

• Don’t use type system to track termination.

Static vs. Dynamic Type Checking

Most languages use a combination of static and dynamic checks

Static: “for all inputs”

• input independent
• efficient at run-time
• approximate : rules out some programs that won’t trigger errors
  example: (if false then 2 else "hi") ^ "there"

Dynamic: “for some inputs”

• depends on input
• run-time overhead
• precise

Check your understanding: Static vs. Dynamic Type Systems

Type System and Checker for a Simple Language

Why do we write a type checker?

• Canonical example of static analysis. Used pervasively in industry in code improvement and security analysis.

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

• Tool for structuring language design, which applies to input validation. If (when!) you get to do your own language designs, type systems are an area where you are most likely to be able to innovate. The ideas behind type systems apply any time you need to validate user input, for example. This is the highest level of cognitive task: creation of new things.

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

datatype ty = WORDTY | FLAGTY

Examples to rule out

Can’t add a word and a flag:

3 + (3 < 99)

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

Can’t compare a word and a flag

(3 < (4 = 24))

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

Check your understanding: AST Representation of Simple Language

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

datatype ty = WORDTY | FLAGTY

Inference rules to define a type system

• Form of judgment Context |- term : type

  Written |- e : tau

  Contexts vary between type systems

  (Right now, the empty context)

• Judgment is proved by derivation

• Derivation made using inference rules

• Inference rules determine how to code val typeof : exp -> ty:

  Given e, find tau such that |- e : tau

Rule for arithmetic operators

Informal example:

|- 3 : word    |- 5 : word 
-------------------------
|- 3 + 5 : word

Rules out:

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

General form:

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

Rule for comparisons

Informal example:

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

General form:

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

Rule for literals

Informal example:

|- 14 : word

General form:

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

Rule for conditionals:

Informal example:

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

General form:

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

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

• input to checker: e

• output from checker: tau

Type checker in ML

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

Check your understanding: A type checker from inference rules

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

datatype ty = WORDTY | FLAGTY

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

    val typeof : exp -> ty
    exception IllTyped
    fun typeof (ARITH (_, e1, e2)) = 
          case (typeof e1, typeof e2) 
            of (WORDTY, WORDTY) => WORDTY
             | _              => raise IllTyped
      | typeof (CMP (_, e1, e2)) = 
          case (BLANK1, BLANK2) 
            of (BLANK3, BLANK4) => BLANK5
             | _              => raise IllTyped
      | typeof (LIT _) = WORDTY
      | typeof (IF (e,e1,e2)) = 
          case (typeof e, typeof e1, typeof e2) 
            of (FLAGTY, tau1, tau2) => 
               if eqType (tau1, tau2) 
               then tau1 else raise IllTyped
             | _                    => raise IllTyped

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

• Give each type a distinct subscript

• Introduce equality constraints

• Remember to be careful using primitive equality to check types—you are better off with eqType.

Typing Rules: Contexts and Term Variables

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

    datatype ty = WORDTY | FLAGTY

    datatype exp = ...
                 | VAR   of name
                 | LET   of name    * exp * exp

    datatype ty = WORDTY | FLAGTY

What could go wrong with a variable?

• Used inconsistently:

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

  x + x @ x

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

  let y = 10 in y ^ “hello” end

So we need to track variable use to ensure consistency

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

Rule for var

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

So as long as x is recorded in Gamma as a WORDTY, it can only be used as a WORDTY.

Rule for let

Gamma          |- e1 : tau1
Gamma{x->tau1} |- e2 : tau2   
-------------------------------------
Gamma |- LET x = e1 in e2 : tau2

Type Checker

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

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

Check your understanding: Adding variables

    Gamma          |- e1 : tau1
    Gamma{x->tau1} |- e2 : tau2   
    -------------------------------------
    Gamma |- LET x = e1 in e2 : tau2

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

Taking Stock

• I gave you syntax for simple language.

• We came up with formal typing rules.

• We used the typing rules to implement the type checker.

• On your homework,

  • You will design new syntax and typing rules for lists

  • You will extend an existing type checker

  • You will implement a full type checker from scratch

This is a big chunk of what language designers do.

Bonus content

What is a type?

• Weak: a set of values

• Better: a conservative prediction about values

• Best: the precise definition: classifier for terms!!

  • The relationship to values becomes a proof obligation.

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

Source of new language ideas for next 20 years

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

What types can rule out

things that could go wrong:

(8 < 10) + 4

(8 == 8) < 9

x + (x :: xs)

let val y = 10 in length y end

21 October 2020: Type checking with type constructors

There are PDF slides for 10/22/2020.

should have two separate answer boxes: one for what they have learned and one for what they have questions about.

Reflection: Simple type checking

Reflection: How many types?

Where we’ve been

New watershed in the homework

• You’ve been developing and polishing programming skills: recursion, higher-order functions, using types to your advantage. But the problems have been mostly simple problems around simple data structures, mostly lists.

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

Where we’re going

• We’re now going to shift and spend the next several weeks doing real programming-languages stuff, starting with type systems.

• What’s next is much more sophisticated type systems, with an infinite number of types.

Focus on two questions about type systems:

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

• How shall we represent types?

We’ll look at these questions in two contexts: monomorphic (this “lecture”) and polymorphic (next “lecture”) languages.

Monomorphic vs Polymorphic Types

Monomorphic types have “one shape.”

• Examples: int, bool, int -> bool, int * int

Polymorphic types have “many shapes.”

• Examples:

  (forall ('a) (list 'a))
  (forall ('a) ((list 'a) -> int))
  (forall ('a) ((list 'a) -> (list 'a)))

  Substitute any type you like for 'a.

• ML Examples: 'a list, 'a list -> int, 'a list -> 'a list

  In ML, forall is only at the top level, and it isn’t written explicitly

Designing monomorphic type systems

Mechanisms:

• Every new variety of type requires special syntax (examples: structs, pointers, arrays)

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

Language designer’s process:

• What new types do I have?

  • Formation rules

• How do I create new values with that type?

  • Introduction rules

  For introduce think “produce”, “create”, “make”, “define”

• What new syntax do I have to observe terms of a type?

  • Elimination rules

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

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

Managing the set of types: Type formation

Check your understanding: Types, type constructors, or garbage

These rules are actually the same as we saw for the simple arithmetic language, but we’ll review them again here.

Monomorphic type rules

Check your understanding: Checking type equalities

Classic types for data structures

At run time, these pairs are identical to cons, car, cdr.

These rules dictate type checker code just like in previous “lecture”.

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

Check your understanding: Writing Typing Rules

Bonus Content

Coding the arrow-introduction rule

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

Approaching types as programmers

Talking type theory: Introduction and elimination constructs

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

• Introduce means “produce”, “create”, “make”, “define”

• Eliminate means “consume”, “examine”, “observe”, “use”, “mutate”

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

Type soundness

26 Oct 2020: Polymorphic Type Checking

There are PDF slides for 10/27/2020.

Your type-system questions are answered.

Today

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

Reflection: Type checking type constructors

Limitations of monomorphic type systems

Notes:

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

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

Check your understanding: Monomorphism limitations

Quantified types

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

Check your understanding: Quantified Types

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

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

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

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

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

Two forms of abstraction:

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

Coding Interlude: Instantiating Polymorphic Functions

Polymorphic Type Checking

Representing quantified types

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

Check your understanding: Representation of quantified types

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

Type rules for polymorphism

Check your understanding: Rules for type-lambda

Type formation through kinds

-> (lambda ([a : array]) (Array.size a))
type error: used type constructor `array' as a type

-> (lambda ([x : (bool int)]) x)
type error: tried to apply type bool as type constructor

-> (@ car list)
type error: instantiated at type constructor `list', 
which is not a type

Check your understanding: Use kinds to classify types

Opening the closed world

Bonus content: a definition manipulates three environments

28 October 2020: Introduction to type inference

There are PDF slides for 10/29/2020.

Retrospective: Type Checking

Reflection: How does the compiler know?

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

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

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

Let’s do some examples

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

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

What do we know?

• double has type ′a₁

• x has type ′a₂

• + has type int * int -> int

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

  • ′a2 ~ int and ′a2 ~ int

• Is this possible?

Key idea: Record the constraint in a typing judgement.

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

Example: (if y 1 0)

• y has type ′a3, 1 has type int, 0 has type int

• Requires what constraints? (int ~ int, ′a3 ~ bool)

Example: (if z z (- 0 z))

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

• Requires what constraints? (′a3 ~ bool /\ int ~ int /\ ′a3 ~ int)

• These constraints are not solveable so the program is ill-typed.

Check your understanding: Gathering constraints

    'ax ~ int /\ 'ay ~ int, 
    {x : 'ax, y : 'ay } |- (+ x y) : int

    'ax ~ int /\ 'ay ~ int, 
    {x : 'ax, y : 'ay } |- (+ x y) : int

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 -> 'a2) 'a_x 'a_x -> 'a2)

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

we can generalize to:

(forall ('a_x 'a2) (('a_x -> 'a2) 'a_x 'a_x -> 'a2))

which is the same thing as:

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

Check your understanding: Type inference with polymorphic functions

(val cc (lambda (nss) (car_2 (car_1 nss))))

car : forall 'a . 'a list -> 'a

Extra examples

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

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

Precise inference with Hindley-Milner types

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

datatype type_scheme
  = FORALL of tyvar list * ty

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

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

Check your understanding: Hindley-Milner Types

FORALL (BLANK1, 
        CONAPP(BLANK2, 
               [CONAPP (TYCON "arguments", BLANK3), 
                        TYVAR "alpha" ]))

2 November 2020: Making type inference formal

There are PDF slides for 11/3/2020.

Retrospective: Introduction to type inference

Type inference algorithm, formally

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

What you know and can do now

Check your understanding: Type inference algorithm

Reflection: Solving constraints

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

What does it mean to solve constraints?

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

  TYVAR "alpha1" ~ TYCON "int" /\  
  TYVAR "alpha2" ~ TYCON "bool"

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

just formalize it. It’s a function that behaves a certain way.

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

Check your understanding: Substitutions and satisfied constraints

Solving simple type equalities

Reflection: Solving type-equality constraints

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

tau1 \ tau2    TyVar2    TyCon2      ConApp2

                alpha2     mu2     (tau21,...,tau2n)tau2

TyVar1             1        2          3

TyCon1             S      mu1=mu2?     Fail

ConApp1            S        S          Recurse

I = immediate; S = symmetry; 

1 = alpha1 -> alpha2

2 = alpha1 -> mu2

3 = if occurs check passes, alpha1 -> (tau21,...,tau2n)tau2

Solving conjunctions

Check your understanding: Solving constraints

The inference algorithm, formally

4 November 2020: Instantiation and generalization

There are PDF slides for 11/5/2020.

Retrospective: Making type inference precise

Reflection: Introducing type schemes

Introducing and eliminating type schemes

Moving from type scheme to types (Instantiation)

Moving from types to type scheme (Generalization)

Check your understanding: Instantiation

(if y (fst 2 3) 4)

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

fst : 'c * 'b -> 'c

'c ~ bool  ;; because y:'c and y is tested by the if

'c ~ int   ;; because first argument to fst is an int

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

Bonus question: Why the distinctness requirement?

Consider again

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

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

Now suppose we instantiate fst as follows:

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

The mistake was ignoring the distinctness requirement when instantiating the type scheme.

From types to type scheme: Val rule

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

We can’t generalize over those variables.

Applying idea to the type inferred for the function fst:

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

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

On the condition θΓ = Γ: Γ is “input”: it can’t be changed.
The condition ensures that θ doen’t conflict with Γ.

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

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

Check your understanding: The full Val rule

(val pick-t (lambda (y z) (pick #t y z)))

To derive that judgment, which of the following might have been how the polymorphic pick function was instantiated, assuming α_y and α_z are the types assumed for variables y and z, respectively? Consider what instantiation would have been necessary to produce the observed constraints and resulting type.

• pick : bool $\cross$ α_p $\cross$ α_y $\arrow$ α_y

• pick : bool $\cross$ α_z $\cross$ α_z $\arrow$ α_z

• pick : bool $\cross$ α_p $\cross$ α_p $\arrow$ α_p

• pick : α_p $\cross$ α_p $\cross$ α_p $\arrow$ α_p

2. The next step is to produce a substitution θ that solves the constraints α_y ~ α_p ∧ α_z ~ α_p and leaves Γ unchanged (θ Γ = Γ). Which of the following substitutions is a such solution?

• θ = { α_z -> α_p}

• θ = { α_y -> α_p, α_z -> α_p}

• θ = { α_p -> α_x, α_z -> α_p}

• None of the above because they all change Γ.

3. The next step is to generalize. Given the substitution θ = { α_y -> α_p, α_z -> α_p}, what type should be passed as the first argument to the generalize function? (The second argument is the empty set because ftv(Γ) = ∅.

• θ(α_y $\cross$ α_z $\arrow$ α_p) = α_p $\cross$ α_p $\arrow$ α_p

• θ(α_y $\cross$ α_z $\arrow$ α_p) = α_z $\cross$ α_z $\arrow$ α_z

• θ(α $\cross$ α $\arrow$ α) = α $\cross$ α $\arrow$ α

• θ(α_y) = α_p

Reflection: Type inference for let form

(lambda (ys)  
   (let ([s (lambda (x) (cons x '()))])
      (pair (s 1) (s #t))))
<function> : 
  (forall ['a] ('a -> (pair (list int) (list bool))))

(lambda (ys)  
   (let ([extend (lambda (x) (cons x ys))])
      (pair (extend 1) (extend #t))))
type error: cannot make int equal to bool

(lambda (ys)  ; OK
    (let ([extend (lambda (x) (cons x ys))])
       (extend 1)))
<function> : ((list int) -> (list int))

Let with constraints, operationally:

1. typesof: returns τ₁, …, τ_n and C

2. val theta = solve C

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

4. freetyvarsGamma, union, freetyvarsConstraint

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

6. Extend the typing environment Gamma (pairfoldr)

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

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

Check your understanding: The Let rule

Check your understanding: The val-rec and letrec rules

Forall things

9 November 2020: Introduction to Object-orientation

There are PDF slides for 11/10/2020.

Retrospective: Type Inference

Reflection: Introduction to Object-Oriented Programming

Information Hiding

So far: Programming in the small

• Expressive power

• Success stories:

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

What about big programs?

• Immersion in pile of interpreter code: not fun

An area of agreement and a great divide:

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

Key idea: Interfaces

• Provide external abstraction of gory details
• Limit access so internals can evolve

Introduction to OOP

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

Goals:

• Abstraction
• Code reuse
• Scaling to large code bases

Mechanism:

• Every object is a black box
• All you can do is send it messages!
• What messages? What do they do?
  That’s the protocol
  (an example of an interface)

Object-oriented demo

Demo: circle, diamond, triangle cards with these methods:

Front:

Object 1 : Circle

• pos: cardinal-point

• set-pos:to: cardinal-point coord

• draw

Back:

Object 1: Circle

;; stores center of shape

center: coord

methods: ...

Message sends:

1. object1 set-pos:to: 'S (0,0)

2. object1 pos: 'N answer: (0,2)

3. object2 set-pos:to: 'S (0,2)

4. object2 pos: 'N answer: (0,4)

5. object3 set-pos:to: 'SW (0,4)

6. object1 draw

7. object2 draw

8. object3 draw

Key concepts of object-orientation

• Don’t ask about my form:
  It’s not your concern!
  (information hiding)

• Instead:

  • Ask me to tell you something
  • Ask me to do something

  (In object-oriented world, imperative “do this” is common.)

• If you ask me something, I might delegate to my parent.

  (Code reuse: one parent can do things for many children.)

Functional vs. OOP mindset

• Functional and procedural:

  • I find out what form you are
  • I decide what to do and how to do it.
  • Function name comes first in the syntax.

• Object oriented:

  • I ask you what to do
  • You decide how to do it, based on what form you are.
  • Receiving object comes first in the syntax.

Reflected in the syntax: the decider comes first!

Examples

Print every element of a list

• Functional: Are you nil or cons?
• OOP: Ask every element to do something.

Multiplication of natural numbers, base 10

• Functional: Are you zero or nonzero?
• OOP: return a number that is 10 times yourself.

Check your understanding: Key concepts of object-orientation

the fact that the concepts are intertwined to the point that it is hard to present them one at a time. In this video, I’ll review some of the key terms to give you some context, but we’ll introduce them again as we see them in use.

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

Check your understanding: OOP Terminology

(method select: (_) self) ;; on ListSentinel

(method select: (aBlock)  ;; on Cons
   ([aBlock value: car] ifFalse:ifTrue:
       {(cdr select: aBlock)}
       {(((Cons new) car: car) 
                     cdr: (cdr select: aBlock))}))

Check your understanding: Classes represent forms of data

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

-> (val ms (ns select: [block (n) ((n mod: 2) = 0)]))
List( 2 4 )

-> (ms do: [block (m) ('element print) (space print)
                      ('is print) (space print)
                      (m println)])
element is 2
element is 4
nil

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

  (method do: (aBlock)
      (aBlock value: car)
      (cdr do: aBlock))

Basic OOP mechanism review

• Message send replaces function application

  • (ns select: pred) vs filter ns pred
• Receiver appears first: it’s in charge!
• Object responds to message by evaluating method

• Method determined by object’s class

Not shown: a method can use primitive operations.

Check your understanding: Code selection via dynamic dispatch

The six questions for Smalltalk

Message passing

Look at SEND

• Message identified by name (messages are not values)
• Always sent to a receiver
• Optional arguments must match arity of message name
  (no other static checking)

N.B. BLOCK and LITERAL are special objects.

Check your understanding: The six questions for Smalltalk

10 November 2020: OOP Mechanisms

There are PDF slides for 11/11/2020.

Retrospective: Introduction to OOP

Smalltalk syntax

little livecoding.

Coding in uSmalltalk

• ;; blocks
• (val twice [block (n) (n + n)])
• (twice value: 3)
• ;; note lightweight syntax for parameterless blocks
• (val delayed {(’hello println) 42})
• delayed
• (delayed value)
• ;; blocks sent to Booleans
• (val x 10)
• (val y 20)
• ;; Note the number of columns matches number of args
• ((x <= y) ifTrue:ifFalse: {x} {y})
• ;; numbers
• ;; Fractions: exact 1 / 3
• ;; (1/3) is a name; (1 / 3) is what you want!
• ((1 / 3) - (1 / 2))
• ((1 / 3) + 1) ;; mixing classes!
• ((1 / 3) asFloat) ;; software floating point
• (2 asFloat)
• ((2 asFloat) sqrt)
• (((2 asFloat) sqrt) squared)
• (100 squared)
• (it squared)
• … keep going until overflow …
• (use bignum.smt)
• 100
• (it squared)
• Try again, go until CPU cap, stack trace