Lecture notes for COMP 105 (Programming Languages)

3 September 2019: Introduction to Comp 105

There are PDF slides for 9/3/2019.

Handout: Lessons in program design

Handout: Design checklists

Why we are here

What it involves:

Today:

What is a programming language?

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

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

Syntactic structure: induction

Numerals

Show some example numerals

Numerals:

2018
73
1852

Not numerals:

3l1t3
2+2
-12

Q: What does a numeral stand for?
    That is, if a numeral appears in the syntax, what sort of value flies around at run time?

Q: Does every numeral stand for one of these things?

Q: How many of them are there?

Q: How many numerals are there?

In-class Exercise: Inductive definitions of numerals

Value structure: induction again

In-class exercise: inductive definition of natural number

Writing code with recursion and induction

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

Design checklist:

  1. Forms of data

  2. Example inputs

  3. Function’s name

  4. Function’s contract

  5. Example results

  6. Algebraic laws

  7. Code case analysis

  8. Code right-hand sides

  9. Revisit tests

Recursive-function problem

Exercise: all-fours?

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

Key design step: form of number

Choose inductive structure for natural numbers:

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

Example inputs

Step 2:

Function’s name and contract

Steps 3 and 4:

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

Example results

Step 5: write expected results as unit tests:

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

Algebraic laws

Step 6: Generalize example results to arbitrary forms of data

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

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

Left-hand sides turn into case analysis

Step 7:

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

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

Each right-hand side becomes a result

Step 8:

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

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

Revisit tests:

Step 9:

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

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

Checklist:

Syntax in programming languages

Concrete Syntax

Programming-languages people are wild about compositionality.

Syntactic structure of Impcore

Watch for syntactic categories, syntactic composition

Our common framework

Goal: eliminate superficial differences

No new language ideas.

Imperative programming with an IMPerative CORE:

Idea of LISP syntax

Parenthesized prefix syntax:

Examples:

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

(For now, we use just the round brackets)

Impcore structure

Two syntactic categories: expressions, definitions

No statements!—expression-oriented

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

Evaluating e has value, may have side effects

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

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

Syntactic structure of Impcore

An Impcore program is a sequence of definitions

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

Compare

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

Impcore variable definition

Example

(val n 99)

Compare

int n = 99;

Slide 15 

Example function shows every form

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

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

Live coding in Impcore

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

9 September 2019: Abstract syntax and operational semantics

There are PDF slides for 9/9/2019.

Live coding: Impcore

All fours, tests, big literals

square, negated, interactive check-expect

Review: algebraic laws

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

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

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

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

Approaching 105

100-level course

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

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

Awareness of your own learning: Metacognition

Office hours

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

Review

Short discussion: One thing you learned in the first class

Language: syntax, rules/organization/grammar

Programming language: you can run it (values)

Preparing for a language you’ve never seen before

You need a vocabulary. It will involve math.

This week: abstract syntax and operational semantics

Bloom’s taxonomy (Metacognition 10)

Cognitive actions:

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

Operational semantics

Cognitive actions:

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

Concrete and abstract Syntax

Programming-languages people are wild about compositionality.

Example of compositionality: concrete syntax (grammar)

                                C/C++  Impcore

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

Add new names to program
  - initialized                  def     def
  - uninitialized                decl

Example rules of composition:

Programming-language semantics

“Semantics” means “meaning.”

We want a computational notion of meaning.

What problem are we trying to solve?

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

Ways of knowing:

Why bother with precise semantics?

(Needed to build implementation, tests)

Same reason as other forms of math:

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

The idea: your new skills will apply

Behavior decomposes

What happens when we run (* y 3)?

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

Knowledge is expressed inductively

Concrete syntax for Impcore

Definitions and expressions:

How to define behaviors inductively

Expressions only

Base cases (plural): numerals, names

Inductive steps: compound forms

First, simplify the task of specification

What’s different? What’s the same?

 x = 3;               (set x 3)

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

Abstract away gratuitous differences

(See the bones beneath the flesh)

Abstract syntax

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

More uniform notation

Good representation in computer

Concrete syntax: sequence of symbols

Abstract syntax: ???

The abstraction is a tree

The abstract-syntax tree (AST):

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

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

ASTs

Question: What do we assign behavior to?

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

Question: How can we represent all while loops?

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

Answer:

As a data structure:

In C, trees are fiddly

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

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

Let’s picture some trees

An expression:

  (f x (* y 3))

(Representation uses Explist)

A definition:

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

Key question: names (review)

From ASTs to behaviors

Behaviors of ASTs, part I: Atomic forms

Numeral: stands for a value

Name: stands for what?

Slide 12 

Slide 13 

``Environment’’ is pointy-headed theory

You may also hear:

Influence of environment is “scope rules”

Find behavior using environment

Recall

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

Your thoughts?

Impcore uses three environments

Global variables ξ

Functions ϕ

Formal parameters ρ

There are no local variables

Function environment ϕ not shared with variables—just like Perl

11 September 2019: Judgments and Rules

There are PDF slides for 9/11/2019.

Students: Take a blank white card

Handout: Redacted Impcore rules

Today:

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

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

    • Metatheory

Review: environments

Slide 1 

Find behavior using environment

Recall

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

Impcore uses three environments

Global variables ξ (“ksee”)

Functions ϕ (“fee”)

Formal parameters ρ (“roe”)

There are no local variables

Function environment ϕ not shared with variables—just like Perl

Rules and metatheory

Review: What elements are needed to know run-time behavior?

Slide 4 

Slide 5 

Slide 6 

OK, your turn: what do you think is rule for evaluating literal, variable? (Base cases)

Slide 7 

Slide 8 

Slide 9 

Slide 10 

Slide 11 

Slide 12 

Slide 13 

Slide 14 

Slide 15 

Slide 16 

Good and bad judgments

Your turn: good and bad judgments

Which correctly describes what happens at run time?

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

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

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

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

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

To know for sure, we need a proof

Proofs: Putting rules together

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

Code example

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

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

Suppose we evaluate (digit? 7)

Exercise:

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

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

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

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

What is the result of (digit? 7)?

How do we know it’s right?

From rules to proofs

Judgment speaks truth when ``derivable’’

Special kind of proof: derivation

A form of “syntactic proof”

Recursive evaluator travels inductive proof

Root of derivation at the bottom (surprise!)

Build

The ``Tony Hawk’’ algorithm

First let’s see a movie

Building a derivation

Slide 20 

Slide 21 

Slide 22 

Slide 23 

Slide 24 

Slide 25 

Slide 26 

Slide 27 

Slide 28 

Slide 29 

Slide 30 

Slide 31 

Slide 32 

Slide 33 

Building derivations

Slide 34 

16 September 2019: Derivations, metatheory, better semantics

There are PDF slides for 9/16/2019.

Review: calls

Slide 1 

Slide 2 

Slide 3 

Review: Derivations

Judgment speaks truth when ``derivable’’

Special kind of proof: derivation

A form of “syntactic proof”

Valid derivation

Initial state partially or fully known

Final state determined by initial state (homework)

Every node in tree is an instance of some rule

No primes!

Recursive evaluator travels inductive proof

Root of derivation at the bottom (surprise!)

Build

The ``Tony Hawk’’ algorithm

First let’s see a movie

Building a derivation

Slide 7 

Slide 8 

Slide 9 

Slide 10 

Slide 11 

Slide 12 

Slide 13 

Slide 14 

Slide 15 

Slide 16 

Slide 17 

Slide 18 

Slide 19 

Slide 20 

Building derivations

Slide 21 

Proofs about derivations: metatheory

Syntactic proofs empower meta reasoning

Proof 𝒟 is a data structure

Got a fact about all proofs?

Prove facts by structural induction over derivations

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

Metatheorems often help implementors

More example metatheorems:

Slide 24 

Metatheorems are proved by induction

Induction over structure (or height) of derivation trees 𝒟

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

Proof

Let’s try it!

Cases to try:

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

Slide 26 

Slide 27 

Slide 28 

Slide 29 

Slide 30 

18 September 2019: Scheme

There are PDF slides for 9/18/2019.

Announcements

Note: course not graded on a curve

Scheme homework:

Where are we going?

Recursion and composition:

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

For a new language, five powerful questions

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

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

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

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

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

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

(Initial basis for μScheme on page 159)

Introduction to Scheme

Two new kinds of data:

Scheme Values

Most values are S-expressions.

An fully general S-expression is one of

Many predefined functions work with a list of S-expressions

A list of S-expressions is either

Programming with lists and S-expressions

Lists: A subset of S-Expressions.

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

Slide 1 

Slide 2 

Constructors: '(),cons

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

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

Why are lists useful?

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

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

Programming example: lists of numbers

Problem-solving: students pose problem on list of numbers

Lists generalized: S-expressions

An ordinary S-expression is one of:

Can write literally in source, with quote

μScheme’s new syntax

Slide 4 

Immutable data structures

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

List-design shortcuts

Three forms of “followed by”

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?

You fill in these right-hand sides:

(append '()         ys) == 

(append (cons z zs) ys) == 

Equations and function for append

(append '()         ys) == ys

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


(define append (xs ys)

  (if (null? xs)

      ys

      (cons (car xs) (append (cdr xs) ys))))

Why does it terminate?


Cost model

The major cost center is cons because it corresponds to allocation.

How many cons cells are allocated?

Let’s rigorously explore the cost of append.

Induction Principle for List(A)

Suppose I can prove two things:

  1. IH (’())

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

then I can conclude

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

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

Proof: By induction on the structure of xs.

Base case: xs = ’()

Inductive case: xs = (cons z zs)

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

Costs of list reversal

Algebraic laws for list reversal:

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

And the code?

Naive list reversal

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

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

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

The method of accumulating parameters

Write laws for

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

Who could write the code?

Reversal by accumulating parameters

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

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

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

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

Association lists represent finite maps (code not to be covered in class)

Implementation: list of key-value pairs

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

Picture with spine of cons cells, car, cdar, caar, cadar.

A-list example

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

Notes:

Algebraic laws of association lists

Laws of association lists

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

23 September 2019: First-class and higher-order functions

There are PDF slides for 9/23/2019.

Skills refresh

Refresh: Complete these laws

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

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

Refresh: Complete these laws

Waiting…

Refresh: Complete these laws

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

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

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

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

Today: New syntax, its rules and values

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

Already doing it: immutable data (append)

Next up: better ways of gluing functions together

μScheme’s semantics

Impcore: Things that should offend you

Look up function vs look up variable:

To get variable, check multiple environments

Create a function? Must give it a name

Slide 5 

Slide 6 

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

New syntax exploits semantics

Slide 7 

Slide 8 

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

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

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

Slide 9 

So let’s see that semantics!

Key idea: don’t worry about memory

Slide 10 

From Impcore to uScheme: Lambda

Anonymous, first-class functions

From Church’s lambda-calculus:

(lambda (x) (+ x x))

“The function that maps x to x plus x”

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

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

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

Functions become just like any other value.

First-class, nested functions

(lambda (x) (+ x y))  ; means what??

What matters is that y can be a parameter or a let-bound variable of an enclosing function.

First example: Finding roots. Given n and k, find an x such that x^n = k.

Step 1: Write a function that computes x^n - k.

Step 2: Write a function that finds a zero between lo and hi bounds.

Picture of zero-finding function. Algorithm uses binary search over integer interval between lo and hi. Finds point in that interval in which function is closest to zero.

Code that computes the function x^n - k given n and k:

Function escapes!

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

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

No need to name the escaping function

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

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

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

The zero-finder

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

findzero-between is also a higher-order function because it takes another function as an argument. But nothing escapes; you can do this in C.

Example uses:

Cube root of 27 and square root of 16

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

Your turn!!

Lambda questions

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

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

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

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

Lambda answers

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

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

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

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

Slide 17 

How lambda works

Rule for lambda

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

Slide 18 

Rule for function Application

Slide 19 

Questions about ApplyClosure:

25 Sep 2019: Vocabulary building: List HOFs, the function factory

There are PDF slides for 9/25/2019.

Today: Using lambda to enlarge your vocabulary

Similar: Haskell, ML, Python, JavaScript

Bonus: proving facts about functions

Higher-Order Functions on lists

Today: both functions and lists

Slide 1 

Your turn: Common list algorithms

Algorithms on linked lists (or arrays in sequence):

Predefined list algorithms

Some classics:

Fold also called reduce, accum, a “catamorphism”

Live coding interlude

List search: exists?

Slide 4 

Algorithm encapsulated: linear search

Example: Is there an even element in the list?

Algebraic laws:

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


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

Defining exists?

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

List selection: filter

Defining filter

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

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

Running filter

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

“Lifting” functions to lists: map

Algorithm encapsulated: Transform every element

Example: Square every element of a list.

Algebraic laws:

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

Your turn:

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

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

Answers:

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

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

Defining and running map

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

Slide 11 

The universal list function: fold

Slide 12 

foldr takes two arguments:

Example: foldr plus zero '(a b)

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

Slide 13 

Slide 14 

In-class exercise

Slide 15 

Slide 16 

Slide 17 

Language design — why?

Slide 18 

One-argument functions: Curry and compose

Build one-argument functions from two-argument functions

Slide 19 

The idea of currying

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

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

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

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

What is the benefit? Functions like exists?, all?, map, and filter all expect a function of one argument. To get there, we use Currying and partial application.

To get one-argument functions: Curry

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

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

Slide 22 

Slide 23 

Currying and list HOFs

Your turn!

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

Answers

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

One-argument functions compose

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

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

Another algebraic law, another function:

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

One-argument functions compose

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

Another example: (o not null?)

Slide 27 

30 Sep 2019: Tail calls and continuations

There are PDF slides for 9/30/2019.

Where have we been, where are we going: functions

Today: proofs, costs, control flow

Proofs about functions

Proofs about functions

Function consuming A is related to proof about A

Tail calls

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

A tail call is a call in tail position.

Important for optimizations: Can change complexity class.

What is tail position?

Tail position is defined inductively:

Idea: The last thing that happens

Anything in tail position is the last thing executed!

Key idea is tail-call optimization!

Slide 3 

Slide 4 

Slide 5 

Example: reverse '(1 2)

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

Call stack:

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

Answer: Linear in the length of the list

Tail calls and the method of accumulating parameters

Trick: put answer in parameter
Write laws for

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

Reversal by accumulating parameters

Moves recursive call to tail position

Contract:

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

Laws:

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

Who could write the code?

Reversal by accumulating parameters

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

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

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

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

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

Slide 8 

Slide 9 

Example: revapp '(1 2) '()

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

Call stack: (each line replaces previous one)

revapp ‘(1 2)’() –> revapp ‘(2)’(1) –> revapp ‘()’(2 1)

Answer: Constant

Are tail calls familiar?

In your past, what did you call a construct that

  1. Transfers control to a point in the code?

  2. Uses no stack space?

Answer: a goto!!

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

But goto is limited to labels named in the code.

Remember tail calls? Suppose you call a parameter!

A continuation is code that represents “the rest of the computation.”

Continuations

Different coding styles

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

Continuation-passing style (CPS): Last action of a function is to “throw” value to a continuation. For us, tail call to a parameter.

Uses of continuations

Implementation

Motivating Example: From existence to witness

Slide 11 

Ideas?

Bad choices:

Good choice:

Slide 12 

Slide 13 

Slide 14 

Slide 15 

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

Answer: Constant

Example Use: Instructor Lookup

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

Slide 17 

Slide 18 

Slide 19 

Slide 20 

9 Oct 2019: Lambda Calculus

There are PDF slides for 10/9/2019.

Today: Living with just application, abstraction, variables

Why study lambda calculus?

The world’s simplest reasonable programming language

Only three syntactic forms:

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

Everything is programming with functions

First example:

(\x.\y.x) M N --> (\y.M) N --> M

Crucial: argument N is never evaluated (could have an infinite loop)

Programming in Lambda Calculus

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

Alert to the reading: Wikipedia is reasonably good on this topic

Systematic approach to constructed data:
Everything is continuation-passing style

Q: Who remembers the boolean-formula solver?

Q: What classes of results could it produce?

Q: How were the results delivered?

Q: How shall we do Booleans?

Coding Booleans and if expressions

A Boolean takes two continuations.

Laws:

true  s f = s
false s f = f

Code:

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

Coding the if expression, laws:

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

Therefore, code is:

if M then N else P = ???

Your turn: implement not

Coding data structures

Coding pairs

Coding lists

Coding recursion

Slide 1 

Factorial in lambda calculus

Wish for:

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

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

Successive approximations

Function bot always goes into an infinite loop.

What are these?

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



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



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

cessive approximations (manufactur

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

fact0 = g bot;

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

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

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

   ...

Fixed point

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

Proof by induction on n.

Fixed-point combinator

What if

fix g = g (fix g)

Then fix g n is n factorial!

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

Expand as much as you need to.

Slide 7 

Using fixed points

Now you do it

Conversion to fixed point


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


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

Example recursion equations

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

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

f2 = \n.f2 (isZero? n 100 (pred n));

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

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

Slide 10 

Example recursion equations

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

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

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

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

Coding numbers: Church Numerals

Slide 12 

Church Numerals to machine integers

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

Church Numerals in λ

zero  = \f.\x.x;
succ  = \n.\f.\x.f (n f x);
plus  = \n.\m.n succ m;
times = \n.\m.n (plus m) zero;
 ...
-> four;
\f.\x.f (f (f (f x)))
-> three;
\f.\x.f (f (f x))
-> times four three;
\f.\x.f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))

15 Oct 2019: Lambda-calculus semantics; encoding recursion

There are PDF slides for 10/15/2019.

Calculus examples:

A selection of calculi
Concurrency CCS (Robin Milner)
Security Ambient calculus (Cardelli and Gordon)
Distributed computing pi calculus (Milner)
Biological networks stochastic pi calculus (Regev)
Computation lambda calculus (Church)

Substitution examples:

What is a calculus?

Demonstration of differential calculus: reduce

d/dx (x2 + y2)

Rules:

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

So

d/dx (x + y)2

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

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

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

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

2 ⋅ (x + y) ⋅ 1

2 ⋅ (x + y)

What is a calculus? Manipulation of syntax.

What corresponds to evaluation? “Reduction to normal form”

Today

Lambda:

Review: Live coding

Algebraic laws for

Review: Church encodings

Your turn: write and

Slide 1 

Review: Church Numerals

zero  = \f.\x.x;
succ  = \n.\f.\x.f (n f x);
plus  = \n.\m.n succ m;
times = \n.\m.n (plus m) zero;
 ...
-> four;
\f.\x.f (f (f (f x)))
-> three;
\f.\x.f (f (f x))
-> times four three;
\f.\x.f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))

Operational semantics of lambda calculus

New kind of semantics: small-step

New judgment form

M --> N   ("M reduces to N in one step")

No context!! No turnstile!!

Just pushing terms around == calculus

Slide 3 

Board examples:

  1. Are these functions the same?

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

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

Slide 4 

Examples of free variables:

\x . + x y

\x. \y. x

Your turn! Free Variables

What are the free variables in each expression?

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

Your turn! Free Variables

What are the free variables in each expression?

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

Beta-reduction

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

Slide 7 

Example:

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

and never

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

Really wrong!

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

Must rename the bound variable:

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

Slide 8 

Slide 9 

Nondeterminism of conversion:

               A
              / \
             V   V
            B     C

Now what??

Slide 10 

Normal forms

Idea: normal form

A term is a normal form if

It cannot be reduced

What do you suppose it means to say

Idea: normal form

A term is a normal form if

It cannot be reduced

A term has a normal form if

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

A term has no normal form if

It always reduces forever
(This term diverges)

Slide 13 

Slide 14 

Reduction strategies (your homework, part 2)

Applicative-order reduction

Given a beta-redex

(\x.M) N

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

Q: Does applicative order ever prevent you from making progress?

A: No. We can prove it by induction on the number of lambdas in N

Slide 15 

Normal-order reduction

Always choose leftmost, outermost redex

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

Slide 16 

Not your typical call-by-value semantics!

Lambda calculus in context

What’s its role in the world of theory?

Operational semantics          Type theory     Denotational      Lambda 
(Natural deducation style)                       semantics      calculus
--------------------------     -----------     ------------     --------

Interpreters like Python       type checkers   compilers        *models*

Why is it “calculus”?

What’s the role of calculi in computer science:

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

21 Oct 2019: Introduction to ML

There are PDF slides for 10/21/2019.

Handout: Learning Standard ML

Scheme: What’s Good? What’s Bad?

An advanced cognitive task:

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

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

Apply your new knowledge in Standard ML:

Meta: Not your typical introduction to a new language

ML Overview

Designed for programs, logic, symbolic data

Theme: Precise ways to describe data

ML = uScheme + pattern matching + static types + exceptions

ML forms of data

Live coding:

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

More live coding:

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

Still more live coding? (New forms of data)

Ordinary S-expression
Binary tree of integers

Live coding memories:

(* list selection *)

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

(* better version: *)

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

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

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

(* testing code *)

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

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

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

μScheme to ML Rosetta stone

uScheme                    SML

 (cons x xs)             x :: xs

 '()                     []
 '()                     nil

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

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

 ||  &&                  andalso    orelse


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

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

Three new ideas

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

Pattern matching makes code look more like algebraic laws: one pattern for each case

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

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

And lots of new concrete syntax!

Examples

The length function.

Length

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

val res = length [1,2,3]

Map

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

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

Map, without redundant parentheses

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

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

Filter

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

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

Filter, without redundant parentheses

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

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

Exists

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

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

Exists, without redundant parentheses

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

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

All

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

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

All, without redundant parentheses

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

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

Take

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

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

(* Note use of exceptions. *)

Take, without redundant parentheses

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

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

(* Note use of exceptions. *)

Drop

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

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

Takewhile

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

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

Takewhile, without redundant parentheses

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

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

Dropwhile

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

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

Dropwhile, without redundant parentheses

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

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

Folds

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

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


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

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

Folds, without redundant parentheses

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

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


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

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

ML—Five Questions

Values: num/string/bool, constructed data

Syntax: definitions, expressions, patterns, types

Environments: names stand for values (and types)

Evaluation: uScheme + case and pattern matching

Initial Basis: medium size; emphasizes lists

(Question Six: type system—a coming attraction)

A note about books

Ullman is easy to digest

Ullman costs money but saves time

Ullman is clueless about good style

Suggestion:

Details in course guide Learning Standard ML

23 Oct 2019: Programming with constructed data and types

There are PDF slides for 10/23/2019.

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

Improving on Scheme

Scheme problems

Unsolved:

Solved:

New vocabulary

Data:

Code:

Types:

Today’s plan: programming with types

  1. Mechanisms to know:

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

Foundation: Data

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

“Language support for forms of data”

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

Tuple types and arrow types

Background for datatype review (board):

This is all you need to know about the special built-in type constructors (cross and arrow).

Constructed data: Algebraic data types

Tidbits:

Notes:

Mechanisms to know

Three programming tasks:

Datatype definitions

datatype  suit    = HEARTS | DIAMONDS | CLUBS | SPADES

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

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

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

Exegesis (on board):

Your turn: S-expressions

Structure of algebraic types

An algebraic data type is a collection of alternatives

The thing named is the value constructor

(Also called “datatype constructor”)

Your turn: Define a type

An ordinary S-expression is one of

Two steps:

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

Your turn: Define a type

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

The other form of constructed data: tuples

Other constructed data: Tuples

Always only one way to form

Example:

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

Additional language support for algebraic types: case expressions

“Eliminate” values of algebraic types

New language construct case (an expression)

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

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

works for any datatype

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

But often a clausal definition is better style:

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

Making types work for you

Types help me, part I: type-directed programming

Common idea in functional programming: "lifting:

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

Potential bonus content: inorder traversal of binary tree.

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

Bonus content

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

Bonus content: Even more algebraic datatypes

Algebraic datatype review:

Enumerated types

Datatypes can define an enumerated type and associated values.

datatype suit = HEARTS | DIAMONDS | SPADES | CLUBS

Here suit is the name of a new type.

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

Value constructors are separated by vertical bars.

Pattern matching

Datatypes are deconstructed using pattern matching.

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

val suitName = toString HEARTS

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

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

int_tree is the name of a new type.

There are two data constructors: LEAF and NODE.

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

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

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

Building values with constructors

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

 val tempty = LEAF
 val t1 = NODE (1, tempty, tempty)
 val t2 = NODE (2, t1, t1)
 val t3 = NODE (3, t2, t2)

What is the in-order traversal of t3?

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

What is the pre-order traversal of t3?

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

Deconstruct values with pattern matching

(The @ symbol denotes append in ML)

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

val il3 = inOrder t3

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

val pl3 = inOrder t3

int_tree is monomorphic because it has a single type.

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

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

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

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

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

Examples:

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

Datatype Exercise

Slide 13 

Wait for it …

Exercise answers

datatype sx1 = ATOM1 of atom
             | LIST1 of sx1 list

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

Bonus content: Exceptions — Handling unusual circumstances

Syntax:

Informal Semantics:

Exception handling in action

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

Bonus Content: ML traps and pitfalls

Slide 17 

Order of clauses matters


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

(* what goes wrong? *)

Gotcha — overloading

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

Slide 20 

Gotcha — parentheses

Put parentheses around anything with |

case, handle, fn

Function application has higher precedence than any infix operator

Bonus content (seen in examples)

Syntactic sugar for lists

Syntactic sugar for lists

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

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

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

Bonus content: ML from 10,000 feet

Slide 23 

Environments

The value environment

Names bound to immutable values

Immutable ref and array values point to mutable locations

ML has no binding-changing assignment

Definitions add new bindings (hide old ones):

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

Nesting environments

At top level, definitions

Definitions contain expressions:

def ::= val pattern = exp

Expressions contain definitions:

exp ::= let defs in exp end

Sequence of defs has let-star semantics

Patterns

What is a pattern?

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

Design bug: no lexical distinction between

Workaround: programming convention

Functions

Function pecularities: 1 argument

Each function takes 1 argument, returns 1 result

For “multiple arguments,” use tuples!

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


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

Tuples are “usual and customary.”

Slide 28 

Types

Slide 29 

Slide 30 

Slide 31 

Slide 32 

30 October 2019: Hiding information with abstract data types

There are PDF slides for 10/30/2019.

Handout: Mastering Multiprecision Arithmetic

Announcements

Today’s learning objectives:

Data abstraction

Where have we been?

What about big programs?

An area of agreement and a great divide:

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

Why modules?

Unlocking the final door for building large software systems

Modules overview

Functions of a true module system:

Real modules include separately compilable interfaces and implementations

Interfaces

Collect declarations

Things typically declared:

Key idea: a declared type can be abstract

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

Example interface with declarations

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

Roles of interfaces in programming:

The best-proven technology for structuring large systems.

Ways of thinking about interfaces

Design choice: placing interfaces

Interface “projected” from implementation:

Full interfaces:

Module Implementations

Standard ML Modules

The Perl of module languages?

What we’ve been using so far is the core language

Modules are a separate language layered on top.

ML module terminology

Interface is a signature

Implementation is a structure

Generic module is a functor

Structures and functors match signature

Analogy: Signatures are the ``types’’ of structures.

Signature basics

Signature says what’s in a structure

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

Ordinary type examples:

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

Type constructors work too

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

ML Modules examples, part I

Signature example: Ordering


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

Signature example: Integers

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

Implementations of integers

A selection…

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

Homework: natural numbers

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

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

Homework: integers

signature BIGNUM = sig
   type bigint
   exception BadDivision

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

Signature review: collect

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

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

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

Structure: collect definitions

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

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


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

Dot notation to access components

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

What interface with what implementation?

Maybe mixed together, extracted by compiler!

Maybe matched by name:

Best: any interface with any implementation:

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

Signature Matching

Well-formed

 structure Queue :> QUEUE = QueueImpl

if principal signature of QueueImpl matches ascribed signature QUEUE:

Signature Ascription

Ascription attaches signature to structure

Slogan: “use the beak”

Opaque Ascription

Recommended

Example:

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

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

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

Abstract data types

How opaque ascription works

Outside module, no access to representation

Inside module, complete access to representation

Abstract data types and your homework

Natural numbers

Data abstraction for reuse

Abstract data types and your homework

Two-player games:

Problems abstraction must solve:

Result: a wide interface

Testing code with abstract types

Test properties of observed data:

Same story with numbers:

Abstraction design: Computer player

Computer player should work with any game, provided

Brute force: exhaustive search

Your turn! What does computer player need?

Our computer player: AGS

Any game has two key types:

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

Key functions use both types:

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

Multiple games with different state, move?

Yes! Using key feature of ML: functor

A is a generic module

A new form of parametric polymorphism:

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

Functors and an Extended SML Example

Game interoperability with functors

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

Functors: baby steps

A functor abstracts over a module

Formal parameters are declarations:

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

Combines familiar ideas:

Using Functors

Functor applications are evaluated at compile time.

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

Actual parameters are definitions

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

where EQueue is a more efficient implementation

Slide 27 

Slide 28 

Functors on your homework

Separate compilation:

Code reuse with type abstraction

ML module summary

New syntactic category: declaration

Signature groups declarations: interface

Structure groups definitions: implementation

Functor enables reuse:

Opaque ascription hides information

Extended example: Error-tracking Interpreter

Reusable Abstractions: Extended Example

Error-tracking interpreter for a toy language

Why this example?

Error modules: Three common implementations

Your obligations: two types, three functions, algebraic laws

Classic ``accumulator’’ for errors

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

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

  val oneError : error -> summary

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

First Error: Implementation

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

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

    val oneError = SOME
  end

All Errors: Implementation

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

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

Computations Abstraction

Ambitious! (will make your head hurt a bit)

Computations either:

Errors must be threaded through everything :-(

Exercise: Simple arithmetic interpreter

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

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


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

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

Exercise: LIT and PLUS cases

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

Exercise: DIV case

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

That’s really painful!

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

Combining generic computations

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

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

  (* Apply a pure function to a computation. *)
  val <$> : ('a -> 'b) * 'a comp -> 'b comp

  (* Application inside computations. *)
  val <*> : ('a -> 'b) comp * 'a comp -> 'b comp
                      
  (* Computation followed by continuation. *)
  val >>= : 'a comp * ('a -> 'b comp) -> 'b comp
end

Example:

eval e1 + eval e2

(op +) (eval e1, eval e2)

curry (op +) (eval e1) (eval e2)

curry (op +) <$> eval e1 <*> eval e2

The first three versions are not well typed. Why?

The last version will thread errors through the compuation behind the scenes.

Note:

eval e1, eval e2 : int comp

curry (op +) : int -> (int -> int)

<$> : (int -> (int -> int)) * (int comp) -> (int -> int) comp

<*> : (int -> int) comp * int comp -> int comp

curry (op +) <$> eval e1 : (int -> int) comp

let pa = curry (op +) <$> eval e1

note by above,  pa : (int -> int) comp 

pa <*> eval e2  : int comp

{Buckets of algebraic laws}

  succeeds a >>= k  == k a                  // identity
  comp >>= succeeds == comp                 // identity
  comp >>= (fn x => k x >>= h) == (comp >>= k) >>= h  
                                          // associativity
  succeeds f <*> succeeds x == succeeds (f x)  // success
  ...

Environments using ``computation’’

signature COMPENV = sig
  type 'a env   (* environment mapping strings
                   to values of type 'a *)
  type 'a comp  (* computation of 'a or
                   an error summary *)

  val lookup : string * 'a env -> 'a comp
end

Payoff!

functor InterpFn(structure Error : ERROR
                 structure Comp  : COMPUTATION
                 structure Env   : COMPENV
                 val zerodivide  : Error.error
                 val error       : Error.error -> 'a Comp.comp
                 sharing type Comp.comp = Env.comp) =
struct
  val (<*>, <$>, >>=) = (Comp.<*>, Comp.<$>, Comp.>>=)
  
  (* Definition of Interpreter *)

end

Definition of intepreter, continued

datatype exp = LIT of int
             | VAR of string
             | PLUS of exp * exp
             | DIV  of exp * exp
fun eval (e, rho) =
 let fun ev(LIT n) = Comp.succeeds n
       | ev(VAR x) = Env.lookup (x, rho)
       | ev(PLUS (e1, e2)) = curry op + <$> ev e1 <*> ev e2
       | ev(DIV (e1, e2))  = ev e1 >>= (fn n1 =>
                             ev e2 >>= (fn n2 =>
                             case n2
                               of 0 => error zerodivide
                                | _ => Comp.succeeds
                                              (n1 div n2)))
 in  ev e
 end

Slide 43 

{Extend a signature with }

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

{Let’s build }

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

  type 'a comp = 'a result
  fun run comp = comp
 
  fun error e = ERR (Error.oneError e)
  fun succeeds = OK
  ... 
end

ML Module summary

ML module summary

New syntactic category: declaration

Signature groups declarations: interface

Structure groups definitions: implementation

Functor enables reuse:

Opaque ascription hides information

13 Nov 2019: Types

There are PDF slides for 11/13/2019.

Notes on slide:

Type systems

What they do:

How they work

World’s most widely deployed static analysis

Where type systems are found:

Trajectory:

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

Today:

Type systems

What kind of thing is it?

``Types classify terms’’

“Term” is theory word for “syntax”:

n + 1  : int

"hello" ^ "world"  : string

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

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

Questions type systems can answer:

Questions type systems typically do not answer:

Type systems designed to solve a problem

Type System and Checker for a Simple Language

Why do we write a type checker?

Define an AST for expressions with:

Type soundness

Key theorem: prediction is accurate

Type-system example

Simple language of machine-level expressions

Two types:

Type this: Language of expressions

Words and flags:

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

datatype ty = WORDTY | FLAGTY

(Looks a lot like int and bool)

Examples to rule out

Can’t add a word and a flag:

3 + (3 < 99)

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

Can’t compare a word and a flag

(3 < (4 = 24))

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

Inference rules to define a type system

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.

What types can rule out

things that could go wrong:

(8 < 10) + 4

(8 == 8) < 9

x + (x :: xs)

let val y = 10 in length y end

What is a type?

Source of new language ideas for next 20 years

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

Type checker in ML

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

Slide 6 

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

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

Typing Rules: Contexts and Term Variables

Your turn:

Things to think about:

Q: What context do we need to evaluate an expression?

Q: Do we need all the same context to decide on a type?

Q: What do we need then?

Rule for var

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

Rule for let

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

What is the information flow?

Type Checker

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

Type checking for variables

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

18 Nov 2019: Type checking with type constructors

There are PDF slides for 11/18/2019.

Type soundness

Slide 1 

Approaching types as programmers

Understanding language design

Questions about types never seen before:

Examples: pointer, struct, function, record

Talking type theory

Formation: make new types

Introduction: make new values

Elimination: observe (“take apart”) existing values

Talking type theory: Introduction and elimination constructs

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

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

Slide 4 

Slide 5 

Slide 6 

Review:

Upcoming (on the new homework)

This is a big chunk of what language designers do.

Functions

Introduction:

Gamma{x->tau1} |- e : tau2   
-----------------------------------------
Gamma |- (lambda ([x : tau1]) e)  : tau1 -> tau2

Elimination:

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

Type Checking with Type Constructors

Where we’ve been and where we’re going

New watershed in the homework

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

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

Design and implementation of monomorphic languages

Mechanisms:

Language designer’s agenda:

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

Your turn: If I “add lists” to a language, how many new types am I introducing?

Managing the set of types: Type formation

Slide 7 

Examples: Not yet types, or not types at all

These ``types in waiting’’ These are

Type-formation rules

We need a way to classify type expressions into:

Slide 10 

Slide 11 

Type judgments for monomorphic system

Two judgments:

Monomorphic type rules

Slide 13 

Slide 14 

Slide 15 

Slide 16 

Notice: one rule for if!!

Classic types for data structures

Slide 17 

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

Slide 18 

Slide 19 

Typical syntactic support for types

Explicit types on lambda and define:

Abstract syntax:

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

Slide 21 

Slide 22 

Typing Rule Exercise

Slide 23 

Wait for it …

Slide 25 

Coding the arrow-introduction rule

Slide 26 

Type-checking LAMBDA

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

20 Nov 2019: Polymorphic Type Checking; Kinds classify types

There are PDF slides for 11/20/2019.

Today

In class:

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

Slide 1 

Slide 2 

Slide 3 

Slide 4 

Typing Rule Exercise

Slide 5 

Wait for it …

Slide 7 

Limitations of monomorphic type systems

New types are expensive

Closed world

A new type constructor (“array”) requires

Slide 9 

Notes:

Expense for programmers

Monomorphism leads to code duplication

User-defined functions are monomorphic:

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

Quantified types

Idea: Do it all with functions

Instead of syntax, use functions!

Requires: more expressive function types

Better type for a swap function

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

Slide 13 

Slide 14 

Polymorphic Type Checking

Quantified types

Representing quantified types

Two new alternatives for tyex:

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

Programming with quantified types

Substitute for quantified variables: “instantiate”

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

Substitute what you like

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

More instantiations

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

Bonus instantiation:

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

Slide 19 

Polymorphic array swap

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

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

Two forms of abstraction:

Power comes at notational cost

Function composition

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

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

Aka o :

Type rules for polymorphism

Slide 22 

Slide 23 

Type formation through kinds

What have we gained?

No more introduction rules:

No more elimination rules:

But, we still need formation rules

You can’t trust code

User’s types not blindly trusted:

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

How can we know which types are OK?

Slide 26 

Slide 27 

Slide 28 

Slide 29 

Designer’s burden reduced

To extend Typed Impcore:

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

You’ll do arrays both ways

Slide 31 

Opening the closed world

What can a programmer add?

Typed Impcore:

Typed μScheme:

Standard ML:

Bonus content: a definition manipulates three environments

Slide 33 

Slide 34 

Slide 35 

25 Nov 2019: Introduction to type inference

There are PDF slides for 11/25/2019.

Announcements

Recitation this week

Designed for final stages of homework. Your choice:

Extra office hours

(And you’ll get an email)

Today

How does the compiler know?

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

Questions: where do explicit types appear in C?

Where do they appear in Typed μScheme?

Get rid of all that:

Slide 1 

What type inference accomplishes

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

What else type inference accomplishes

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

How it works

  1. For each unknown type, a fresh type variable

  2. Every typing rule adds equality constraints

  3. Instantiate every variable automatically

  4. Introduce polymorphism at let/val bindings

Plan of study:

Slide 5 

Let’s do an example on the board

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

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

What do we know?

Key idea: Record the constraint in a typing judgement.

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

Example: if

Example:

Inferring polymorphic types

(val app2 (lambda (f x y)
             (begin
                (f x)
                (f y))))

Assume f : ’a_f

Assume x : ’a_x

Assume y : ’a_y

f x implies ’a_f ~ (’a_x -> ’a)

f y implies ‘a_f ~ (’a_y -> ’a’)

Together, these constraints imply ‘a_x = ’a_y and ’a = ’a’

begin implies result of function is ’a

So,

app2 : (('a_x -> 'a) 'a_x 'a_x -> 'a)

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

we can generalize to:

(forall ('a_x 'a) (('a_x -> 'a) 'a_x 'a_x -> 'a))

which is the same thing as:

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

2 Dec 2019: Making type inference precise

There are PDF slides for 12/2/2019.

Review

Type inference: Review of the basics

  1. For each unknown type, a fresh type variable

  2. Instantiate every variable automatically

  3. Every typing rule adds equality constraints

  4. Solve constraints to get substitution

  5. Apply substitution to constraints and types

  6. Introduce polymorphism at let/val bindings

Review: Using polymorphic names


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

Assume nss : ’b

We know car : forall ’a . ’a list -> ’a

=> car_1 : ’a1 list -> ’a1

=> car_2 : ’a2 list -> ’a2

(car_1 nss) => ’b ~ ’a1 list

(car_2 (car_1 nss)) => ’a1 ~ ’a2 list

(car_2 (car_1 nss)) : ’a2

nss : ’b

: 'a1 list                    

: ('a2 list) list

So, cc : (’a2 list) list -> ’a2

Because ’a2 is unconstrained, we can generalize:

cc : forall ’a . (’a2 list) list -> ’a

Using polymorphic names


-> (val cc (lambda (nss) (car (car nss))))
   
cc : (forall ('a) ((list (list 'a)) -> 'a))

Your turn!

Given

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

For

  (cons empty empty)

You fill in:

  1. Fresh instances
  2. Constraints
  3. Final type

Bonus examples

Bonus example

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

Bonus example solved

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

Infer the type of function two:

Precise inference with Hindley-Milner types

Making Type Inference Precise

Sad news:

Solution:

Consequences:

Slide 8 

Representing Hindley-Milner types

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

datatype type_scheme
  = FORALL of tyvar list * ty

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

Slide 10 

Slide 11 

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

All the pieces

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

The inference algorithm, formally

Slide 13 

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

Slide 14 

Slide 15 

What you know and can do now

Your skills so far

You can complete typeof

(Except for let forms.)

Next up: solving constraints

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

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

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

4 Dec 2019: Building and using a constraint solver

There are PDF slides for 12/4/2019.

Today:

Solving constraints

Representing Constraints

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

What’s going on with substitutions? We have the informal idea—we just formalize it. It’s a function that behaves a certain way.

Slide 2 

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

Slide 3 

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

Slide 4 

{Examples}

Which have solutions?

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

Solving simple type equalities

Slide 6 

Slide 7 

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

Question: how are you going to handle each case?

Solving conjunctions

Slide 8 

Final pieces: completing the algorithm

Revisit a rule:

Slide 9 

What you can know and do now

Write type inference for everything except VAL, VALREC, and LETX

Write function solve, which, given a constraint C, has one of three outcomes:

Instantiate and generalize

Moving from type scheme to types (Instantiation)

Moving from types to type scheme (Generalization)

From Type Scheme to Types

Slide 10 

Slide 11 

From Types to Type Scheme

Slide 12 

Slide 13 

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

We can’t generalize over those variables.

Applying idea to the type inferred for the function fst:

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

Slide 14 

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

Slide 15 

Slide 16 

Slide 17 

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

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

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

Type Inference for Lets and Recursive Definitions

Slide 18 

Let Examples

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

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

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

Slide 20 

Let with constraints, operationally:

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

  2. val theta = solve C

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

  4. freetyvarsGamma, union, freetyvarsConstraint

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

  6. Extend the typing environment Gamma (pairfoldr)

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

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

Slide 21 

Slide 22 

Slide 23 

Forall things

Managing Quantified types
val and val-rec let, letrec, … lambda
FORALL contains all variables (because none are free in the context) FORALL contains variables not free in the context FORALL is empty
Generalize over all variables (because none are free in the context) Generalize over variables not free in the context Never generalize