CS442 Course Notes

Professor: Brad Lushman | Term: Winter 2026

Lecture 1

The course where ML doesn't mean machine learning

Untyped $\lambda$-calculus

Calculus - A system or method of calculation. Syntax & rules for manipulating syntax.

$\lambda$-calc (1934) - A calculus of functions.

Syntax (Backus-Naur form)

$$\begin{array}{rl}⟨expr⟩& ::=⟨var⟩|⟨abs⟩|⟨app⟩\\ ⟨var⟩& ::=a|b|c|\cdots \\ ⟨abs⟩& ::=\lambda ⟨var⟩.⟨expr⟩\\ ⟨app⟩& ::=⟨\underset{\text{rator}}{\underbrace{expr}}⟩⟨\underset{\text{rand}}{\underbrace{expr}}⟩\end{array}$$

This is abstract syntax.

Use parentheses to disambiguate parses.

Conventions:

1. Abstractions extend as far to the right as possible

$\lambda x.yz=\lambda x(yz)\ne (\lambda x.y)z$

2. Applications associate left-to-right

$xyz=(xy)z\ne x(yz)$

Interpretation:

• Variables: self-explanatory
• Abstractions: $\lambda x.E$: Function taking argument $x$ and returning expression $E$.
• Applications: $MN$ result of applying function $M$ to argument $N$.

If you wondered where you would ever use what you learned from CS245, this is the place

Semantics: Two types of variables: free & bound

Consider:

$$\begin{array}{r}\lambda \underset{\text{binding occurrence}}{\underbrace{x}}.\stackrel{\text{bound occurrence}}{\overbrace{x}}\end{array}$$ $$\begin{array}{r}\lambda x.x\underset{\text{free occurrence}}{\underbrace{y}}x\end{array}$$ $$\begin{array}{r}\lambda x.x(\lambda x.x)x\text{idea of scope applies here}\end{array}$$ $$\begin{array}{r}\underset{\text{free}}{\underbrace{x}}\lambda x.x\end{array}$$

Informally, a variable is bound if it has a bound occurrence and free if it has a free occurrence.

Definition

Let $E$ be an expression. The bound variables of $E$, $BV[E]$, are given by

$$\begin{array}{rl}BV[x]& =\varnothing \\ BV[\lambda x.M]& =BV[M]\cup \{x\}\\ BV[MN]& =BV[M]\cup BV[N]\end{array}$$

The free variables of $E$, $FV[E]$, are given by

$$\begin{array}{rl}FVV[x]& =\{x\}\\ FV[\lambda x.M]& =FV[M]-\{x\}\\ FV[MN]& =FV[M]\cup FV[N]\end{array}$$

Two occurrences of a variable mean the same thing if

1. They are both free occurrences

Or

2. They have the same binding occurrence

Can change the name of bound variables, but not free variables.

Definition

$\alpha$-conversion: For all $x$, $y$, $M$, $\lambda x.M{=}_{\alpha }\lambda y.M[y/x]$ if $y\notin FV[M]$.

$M[N/x]$ means substitute $N$ for $x$ in $M$.

More generally, if $C[\lambda x.M]$ denotes an expression in which $\lambda x.M$ occurs as a sub-expression, then the $C[\lambda x.M]{=}_{\alpha }C[\lambda y.M[y/x]]$ if $y\notin FV[M]$.

Consider

$\lambda x.x{=}_{\alpha }\lambda y.y$

$x\lambda x.x{=}_{\alpha }x\lambda a.a$

$$\begin{array}{rl}\lambda a.ba& {=}_{\alpha }\lambda c.bc\\ & {\ne }_{\alpha }\lambda b.bb\\ & {\ne }_{\alpha }\lambda a.da\end{array}$$

Computation:

Expression of the form $(\lambda x.M)N$. The rator is now a function. This is called a $(\beta -)$ redex (reducible expression).

((lambda (x) M) N)

We expect $(\lambda x.M)N\equiv$ evaluate $M$, with $N$ substituted for $x$. i.e. $M[N/x]$.

Definition

($\beta -$reduction): For all $M$, $N$, $x$, $(\lambda x.M)N{\to }_{\beta }M[N/x]$.

More generally, $C[(\lambda x.M)/N]{\to }_{\beta }C[M[N/x]]$.

${\to }_{\beta }$ is a binary relation on terms.

$A{\to }_{\beta }B$: $A$ $\beta$-reduces to $B$ in one step.

$A{\to }_{\beta }^{n}B$: $A$ $\beta$-reduces to $B$ in $n$ steps.

$A{\to }_{\beta }^{\ast }B$: $A$ $\beta$-reduces to $B$ in $0$ or more steps.

$A{\to }_{\beta }^{+}B$: $A$ $\beta$-reduces to $B$ in $1$ or more steps.

Evaluating $M[N/x]$.

Want: Substitute $N$ for all free occurrences of $x$ in $M$.

Definition

Substitution (naïve): $x[E/x]=E$. $y[E/x]=y$. $(MN)[E/x]=M[E/x]N[E/x]$. $(\lambda X.P)[E/x]=\lambda x.P$. $(\lambda y.P)[E/x]=\lambda y.(P[E/x])$.

For example:

$$\begin{array}{rl}(\lambda x.xy)z& {\to }_{\beta }(xy)[z/x]\\ & =x[z/x]y[z/x]\\ & =zy\end{array}$$ $$\begin{array}{r}(\lambda x.x)a{\to }_{\beta }x[a/x]=a\end{array}$$ $$\begin{array}{rl}(\lambda x.\lambda y.x)ab& {\to }_{\beta }(\lambda y.x)[a/x]b\\ & =(\lambda y.x[a/x])b\\ & =(\lambda y.a)b\\ & {\to }_{\beta }a[b/y]\\ & =a\end{array}$$ $$\begin{array}{rl}(\lambda x.\lambda y.y)ab& {\to }_{\beta }(\lambda y.y)[a/x]b\\ & =(\lambda y.y[a/x])b\\ & =(\lambda y.y)b\\ & {\to }_{\beta }y[b/y]\\ & =b\end{array}$$ $$\begin{array}{rl}(\lambda x.\lambda y.x)yz& {\to }_{\beta }(\lambda y.x)[y/x]z\\ & =(\lambda y.x[y/x])z\\ & =(\lambda y.y)z\\ & {\to }_{\beta }y[z/y]\\ & =z\end{array}$$

The last example is referred to as dynamic binding. As the expression is reduced at runtime, the meaning could change.

Question

What happened here?

The free variable $y$ became bound after substitution. The binding occurrence of $x$ changed: $(\lambda x.\lambda y.x)$ On substitution, the last $x$ changed from the first $x$ to the $y$.

Dynamic Binding: The meaning of variables is uncertain until runtime.

We want static binding. The meaning of variables is fixed before runtime.

Definition

Fixed substitution: $x[E/x]=E$. $y[E/x]=y(y\ne x)$. $(MN)[E/x]=M[E/x]N[E/x]$. $(\lambda x.P)[E/x]=\lambda x.P$. We modify the last rule from before. $(\lambda y.P)[E/x]=\lambda y.(P[E/x])(y\ne x,y\notin FV[E])$. $(\lambda y.P)[E/x]=\lambda z.(P[z/y][E/x])(y\ne x,y\notin FV[E])$, $z$ is a brand new variable.

This is the correct definition.

Now

$$\begin{array}{rl}(\lambda x.\lambda y.x)yz& {\to }_{\beta }(\lambda y.x)[y/x]z\\ & =(\lambda a.x[a/y][y/x])z\\ & =(\lambda a.x[y/x])z\\ & =(\lambda a.y)z\\ & {\to }_{\beta }y[z/a]\\ & =y\end{array}$$

Lecture 2

Recall

$$\begin{array}{rl}& (\lambda x.\lambda y.x)yz\\ & {\to }_{\beta }(\lambda y.x)[y/x]z\\ & =(\lambda a.x[a/y][y/x])z\\ & =(\lambda a.x[y/x])z\\ & =(\lambda a.y)z\\ & {\to }_{\beta }y[z/a]\\ & =y\end{array}$$

Computation-$\beta$-reduction until you reach a normal form.

Definition

An expression is in $\beta$-BF if it contains no $\beta$-redices

Definition

An expression is in Weak Normal Form (WNF) if the only $\beta$-redices are inside abstractions.

Consider

$$\begin{array}{rlrl}& (\lambda x.x)((\lambda y.y)z)& & {\to }_{\beta }x[(\lambda y.y)z/x]\\ & =(\lambda x.x)(y[z/y])& & =(\lambda y.y)z\\ & =(\lambda x.x)z& & {\to }_{\beta }y[z/y]\\ & \to x[z/x]& & =z\\ & =z& & \end{array}$$

Two different reduction sequences.

Question

Does it matter which we take?

Theorem

(Church-Rosser): Let $E_1$, $E_2$, $E_3$, be expressions such that $E_1{\to }_{\beta }^{\ast }{E}_2$ and $E_1{\to }_{\beta }^{\ast }{E}_3$. Then there is an expression $E_4$ such that (up to $\alpha$-equivalence) $E_2{\to }_{\beta }^{\ast }{E}_4$ and $E_3{\to }_{\beta }^{\ast }{E}_4$.

Corollary: $\beta$-NFs are unique.

Question

Do all expressions have a $\beta$-NF?

No.

Consider an infinite loop

$$\begin{array}{rl}& (\lambda x.xx)(\lambda x.xx)\\ & {\to }_{\beta }(xx)[(\lambda x.xx)/x]\\ & =(\lambda x.xx)(\lambda x.xx)\end{array}$$

Question

Which expressions have a $\beta$-NF?

This is undecidable. It is equivalent to the Halting problem.

Consider

$$\begin{array}{rl}& (\lambda x.y)((\lambda x.xx)(\lambda x.xx))(\lambda x.y)((\lambda x.xx)(\lambda x.xx)){\to }_{\beta }\dots \\ & {\to }_{\beta }y[((\lambda x.xx)(\lambda x.xx))/x]\\ & =y\end{array}$$

Order matters when infinite reductions are possible.

Reduction Strategies: Plans for choosing a redex to reduce

Applicative Order Reduction (AOR): Choose the leftmost, innermost redex.

• Innermost $=$ not containing any other redex
• ”Eager evaluation”, “call-by-value”

Normal Order Reduction (NOR): Choose the leftmost, outermost redex.

• Outermost $=$ not contained in any other redex
• ”Lazy evaluation”, “call-by-name”

For example,

$$\begin{array}{rl}& (\lambda x.x)((\lambda y.y)z){\to }_{\beta }^{AOR}(\lambda x.x)z{\to }_{\beta }^{AOR}z\\ & {\to }_{\beta }^{NOR}(\lambda y.y)z\\ & {\to }_{\beta }^{NOR}z\end{array}$$

Theorem

(Standardization): If an expression has a $\beta$-NF, then NOR is guaranteed to reach it.

But many programming languages use applicative order, including Scheme.

$\eta$-Reduction:

Consider: $(\lambda x.y)z\to (yx)[z/x]=yz$

So $\lambda x.yz$ behaves exactly like $y$.

Definition

$(\eta$-reduction) $\lambda x.Mx{\to }_{\eta }M$ if $x\notin FV[M]$. More generally, $C[\lambda x.Mx]{\to }_{\eta }C[M]$. $\lambda x.yx{\to }_{\eta }y$.

Programming in the $\lambda$-Calculus

Shorthand for convenience:

$[[\bullet ]]$ : (real-world Programming language) $\to$ $\lambda$-calc

For a real world expression $E$, $[[E]]$ is our replication of $E$ in the $\lambda$-calc.

$[[id]]=\lambda x.x$

Booleans:

$$\begin{array}{r}[[true]]=\lambda x.\lambda y.x\\ [[false]]=\lambda x.\lambda y.y\end{array}$$

If <bool> then <true-part> else <false-part>

If (b,t,f) $=$ if b then t else f

$[[\text{if}]]=\lambda b.\lambda t.\lambda f.btf{\to }_{\eta }^2\lambda b.b$

Alternatively, $[[\text{if }BTF]]=[[B]][[T]][[F]]$

Question

Does it work?

$$\begin{array}{rl}[[\text{if }true\text{ then }P\text{ else }Q]]& =[[true]][[P]][[Q]]\\ & =(\lambda x.\lambda y.x)[[P]][[Q]]\\ & {\to }_{\beta }(\lambda y.[[P]])[[Q]]\\ & {\to }_{\beta }[[P]]\end{array}$$ $$\begin{array}{rl}[[\text{if }false\text{ then }P\text{ else }Q]]& =[[false]][[P]][[Q]]\\ & =(\lambda x.\lambda y.x)[[P]][[Q]]\\ & {\to }_{\beta }(\lambda y.y)[[Q]]\\ & {\to }_{\beta }[[Q]]\end{array}$$ $$\begin{array}{rl}[[not]]& =\lambda b.[[\text{if }b\text{ then }false\text{ else }true]]\\ & =\lambda b.b[[false]][[true]]\\ & =\lambda b.b(\lambda x.\lambda y.y)(\lambda x.\lambda y.x)\\ [[nottrue]]=(\lambda b.b[[false]][[true]])[[true]]& \\ & {\to }_{\beta }[[true]][[false]][[true]]\\ & =(\lambda x.\lambda y.x)[[false]][[true]]\\ & {\to }_{\beta }^2[[false]]\end{array}$$ $$\begin{array}{rl}[[and]]& =\lambda p.\lambda q[[\text{if }p\text{ then }q\text{ else }false]]\\ & =\lambda p.\lambda q.pq(\lambda x.\lambda y.y)\\ [[or]]=\lambda p.\lambda q.[[\text{if }p\text{ then }true\text{ else }q]]& \\ & =\lambda p.\lambda q.p(\lambda x.\lambda y.x)q\end{array}$$

Storage: Use lists

In Scheme, lists are based on pairs

(cons a b) creates the pair.

Nested pairs create lists. (cons a (cons b c))

Need to represent:

• cons
• nil- empty list
• null? - is the list empty?
• car - 1st component of the pair
• cdr - 2nd component of the pair

Modelling pairs: Pair is a function that takes a selector as a parameter. If the selector is true, return the first component. If it is false, return the second component.

$$\begin{array}{r}\text{Pair}:\lambda \underset{\text{selector}}{\underbrace{s}}.[[\text{ if }s\text{ then }\underset{\text{head}}{\underbrace{h}}\text{ else }\underset{\text{tail}}{\underbrace{t}}]]\end{array}$$

So $[[\text{cons}]]=\lambda h.\lambda t.\underset{\text{pair}}{\underbrace{\lambda s.sht}}$

$$\begin{array}{rl}[[(consa(consbnil))]]& =[[cons]]a([[cons]]b[[nil]])\\ & =(\lambda h.\lambda t.\lambda s.sht)a([[cons]]b[[nil]])\\ & {\to }_{\beta }^2\lambda s.sa([[cons]]b[[nil]])\\ & =\lambda s.sa((\lambda h.\lambda t.\lambda s.sht)b[[nil]])\\ & {\to }_{\beta }^2\lambda s.sa\lambda s.sb[[nil]]\end{array}$$

car: return the head, i.e. pass the selector $[[$ true $]]$

$$\begin{array}{rl}[[car]]& =\lambda \ell .\ell [[true]]=\lambda \ell .\ell (\lambda x.\lambda y.x)\end{array}$$

Similarly,

$$\begin{array}{r}[[cdr]]=\lambda \ell .\ell [[false]]=\lambda \ell .\ell (\lambda x.\lambda y.y)\end{array}$$

Example

$$\begin{array}{rl}& [[car]](\lambda s.sa\lambda s.sb[[nil]])\\ & =(\lambda \ell .\ell [[true]])(\lambda s.sa\lambda s.sb[[nil]])\\ & =(\lambda s.sa\lambda s.sb[[nil]])[[true]]\\ & {\to }_{\beta }(\lambda x.\lambda y.x)a\lambda s.sb[[nil]]\\ & {\to }_{\beta }^{2}a\end{array}$$

$$\begin{array}{rl}& [[car]]([[cdr]](\lambda s.sa\lambda s.sb[[nil]]))\\ & {\to }_{\beta }^{\ast }[[car]]\lambda s.sb[[nil]]\\ & {\to }_{\beta }^{\ast }b\end{array}$$

null? must return false when given a pair. $(\lambda s.sht)$. Pass a selector that consumes $h$, $t$, return false.

$$\begin{array}{rl}[[null?]]& =\lambda \ell .\ell (\lambda a.\lambda b.[[false]])\\ & =\lambda \ell .\ell (\lambda a.\lambda b.\lambda x.\lambda y.y)\end{array}$$

Lecture 3

Recall

$$\begin{array}{rl}& [[consht]]=\lambda s.sht\\ & [[cons]]=\lambda h.\lambda t.\lambda s.sht\\ & [[car]]=\lambda \ell .\ell [[true]]\\ & [[cdr]]=\lambda \ell .\ell [[false]]\\ & [[null?]]=\lambda \ell .\ell \lambda a.\lambda b[[false]]\end{array}$$ $$\begin{array}{rl}[[null?]](\lambda s.sht)& =(\lambda \ell .\ell \lambda a.\lambda b.[[false]])\lambda s.sht\\ & {\to }_{\beta }(\lambda s.sht)(\lambda a.\lambda b.[[false]])\\ & {\to }_{\beta }(\lambda a.\lambda b.[[false]])ht\\ & {\to }_{\beta }^2[[false]]\end{array}$$

nil: something to make null? return $true$. $\lambda s.[[true]]=\lambda s.\lambda x.\lambda y.x$

$$\begin{array}{rl}[[null?]][[nil]]& =(\lambda \ell .\ell \lambda a.\lambda b.[[false]])(\lambda s.[[true]])\\ & {\to }_{\beta }(\lambda s.[[true]])(\lambda a.\lambda b.[[false]])\\ & {\to }_{\beta }[[true]]\end{array}$$

So

$$\begin{array}{rl}& [[consa(consbnil)]]\\ & =\lambda s.sa(\lambda s.sb(\lambda s.[[true]]))\end{array}$$

Numbers - consider only non-negative integers.

Easy - encode $n$ as a list of length $n$.

$$\begin{array}{rl}[[0]]& =[[nil]]\\ [[1]]& =\lambda s.s?[[nil]]\\ [[2]]& =\lambda s.s.?\lambda s.s.?[[nil]]\end{array}$$

Primitives: pred, succ, isZero?

$$\begin{array}{rl}[[isZero?]]& =[[null?]]\\ [[pred]]& =[[cdr]]\\ [[succ]]& =\lambda n.\lambda s.s?n(\lambda n.[[cons]]?n)\end{array}$$

Another solution is Church Numerals

Represent $n$ as the act of applying a function $f$ $n$ times to an argument $x$.

$$\begin{array}{rl}[[0]]& =\lambda f.\lambda x.x\\ [[1]]& =\lambda f.\lambda x.fx\\ [[2]]& =\lambda f.\lambda x.f(fx)\\ [[3]]& =\lambda f.\lambda x.f(f(fx))\\ ⋮& \end{array}$$

Addition: $m+n$

• Apply $f$ $n$ times to $x$
• Apply $f$ $m$ times to the result

$$\begin{array}{rl}[[+]]=\lambda m.\lambda n\lambda f.\lambda x.mf(nfx)& \\ & \\ \text{ Note }:& mf(nfx)\\ & =f^m(f^n(x))\\ & =f^{m+n}(x)\end{array}$$ $$\begin{array}{rl}[+23]& =(\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx))(\lambda f.\lambda x.f(fx))(\lambda f.\lambda x.f(f(fx)))\\ & {\to }_{\beta }^2\lambda f.\lambda x(\lambda f.\lambda x.f(fx))f((\lambda f.\lambda x.f(f(fx)))fx)\\ & {\to }_{\beta }\lambda f.\lambda x.(\lambda x.f(fx))((\lambda f.\lambda x.f(f(fx)))fx)\\ & {\to }_{\beta }\lambda f.\lambda x.f(f((\lambda f.\lambda x.f(f(fx)))fx))\\ & {\to }_{\beta }^2\lambda f.\lambda x.f(f(f(f(fx))))\\ & =5\end{array}$$

Special Case: $[[succ]]=\lambda n.\lambda f.\lambda x.nf(fx)$.

Subtraction is considerably harder.

Find a function to apply $n$ times that produces $[[n-1]]$.

Consider: Start with $[[cons00]]$

Apply the function

$$\begin{array}{r}f:[[consab]]\to [[cons(a+1)a]]\end{array}$$

$n$ times:

$$[[consn(n-1)]]$$

then take the cdr.

$$\begin{array}{r}[[pred]]=\lambda n.\lambda f.\lambda x.[[cdr]](n(\lambda p.[[cons]][[car]]p+[[1]])([[carp]]))([[cons00]])\end{array}$$ $$\begin{array}{r}[[-]]=\lambda m.\lambda n.\lambda [[pred]]m\equiv [[m-n]]\end{array}$$

Multiplication: Apply $n$-fold repetition of $f$ $n$ times. $f^{mn}(x)=(f^m{)}^n(x)$.

$$\begin{array}{rl}[[\times ]]& =\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x\\ & {\to }_{\eta }\lambda m.\lambda n.\lambda f.m(nf)\end{array}$$

This is function composition.

Exponents: $m^n$.

$$\begin{array}{r}[[\hat{}]]=\lambda m.\lambda n.nm=m^n\end{array}$$

If you are okay with reversing the arguments,

$$\begin{array}{r}\lambda m.\lambda n.mn\text{for }{m}^n\\ {\to }_{\eta }\lambda m.m\end{array}$$

Recursion: Find the length of the list

$$\begin{array}{rl}[[length]]& =\lambda \ell .[[\text{if }(null?\ell )0(succ(length(cdr\ell )))]]\\ & =\lambda \ell .([[null?]]\ell )[[0]]([[succ]]([[length]]([[cdr]]\ell )))\end{array}$$

Error

$[[length]]$ is defined in terms of itself.

Question

How do we get a closed form repetition of $[[length]]$?

Solve the equation

$$\begin{array}{rl}[[length]]& =\lambda \ell .([[null?]]\ell )[[0]]([[succ]]([[len]]([[cdr]]\ell )))\\ & {=}_{\beta }(\lambda f.\lambda \ell .([[null?]]\ell )[[0]]([[succ]](f([[cdr]]\ell ))))[[length]]\\ & =F([[length]])\text{where }F=\lambda f.\lambda \ell .([[null?]]\ell )[[0]]([[succ]](f([[cdr]]\ell )))\end{array}$$

Aside: Fixed points.

A fixed point of a function $f$ is a value $x$, such that $x=f(x)$.

Example

$f(x)=x^2-6$ has fixed point $3$ since $3=f(3)$.

$[[len]]$ satisfies $[[len]]{=}_{\beta }F([[len]])$

Need a fixed point of $F$.

Consider: $(\lambda x.xx)(\lambda x.xx){\to }_{\beta }(\lambda x.xx)(\lambda x.xx)$

$$\begin{array}{r}X=(\lambda x.f(xx))(\lambda x.f(xx)){\to }_{\beta }f((\lambda x.f(xx))(\lambda x.f(xx)))=f(x)\end{array}$$

Therefore, $X$ is a fixed point of $f$.

Now, parameterize by $f$, get

$$\begin{array}{r}Y=\lambda f.((\lambda x.f(xx))(\lambda x.f(xx)))\end{array}$$

This expression is known as Curry’s Paradoxical Combinator (or Y combinator).

This returns the fixed point of any function.

$$\begin{array}{rl}{Y}_g& =(\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))g\\ & {\to }_{\beta }(\lambda x.g(xx))(\lambda x.g(xx))\\ & {\to }_{\beta }g((\lambda x.g(xx))(\lambda x.g(xx))){\leftarrow }_{\beta }g(Y_g)\end{array}$$

Therefore, for any $g$, $Y_g{=}_{\beta }g(Y_g)$ i.e. $Y_g$ is a fixed point of $g$.

Any combinator (closed expression, i.e. no free variables) $C$, such that $\forall g$ $Cg{=}_{\beta }g(Cg)$ is called a fixed point combinator.

$[[length]]=TF=Y(\lambda f.\lambda \ell .?)$

Consider

$$\begin{array}{rl}& [[length]]([[cons]]a([[cons]]b[[nil]]))\\ & {\to }_{\beta }^{\ast }[[length]](\lambda s.sa(\lambda s.sb[[nil]]))\\ & =YF(\lambda s.sa(\lambda s.sb[[nil]]))\\ & =(\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F(\lambda s.sa(\lambda s.sb[[nil]]))\\ & {\to }_{\beta }(\lambda x.F(xx))(\lambda x.F(xx))(\lambda s.sa(\lambda s.sb[[nil]]))\\ & {\to }_{\beta }F((\lambda x.F(xx))(\lambda x.F(xx))(\lambda s.sa(\lambda s.sb[[nil]])))\\ & =(\lambda f.\lambda \ell .[[null?]]\ell )[[0]]([[succ]](f([[cdr\ell ]])))((\lambda x.F(xx))(\lambda x.F(xx)))(\lambda s.sa(\lambda s.sb[[nil]]))\\ & {\to }_{\beta }^2([[nul?]](\lambda s.sa\lambda s.sb[[nil]]))[[0]]([[succ]]((\lambda s.F(xx))(\lambda x.F(xx))([[cdr]](\lambda s.sa.\lambda s.sb.[[nil]])))\\ & {\to }_{\beta }^{\ast }[[succ]]((\lambda x.F(xx))(\lambda x.f(xx))(\lambda s.sb[[nil]]))\\ & {\to }_{\beta }^{\ast }[[succ]](([[null?]](\lambda s.sb[[nil]])[[0]]([[succ]](\lambda x.F(xx))(\lambda x.F(xx))([[cdr]](\lambda s.sb[[nil]])))))\\ & {\to }_{\beta }^{\ast }[[succ]]([[succ]](\lambda x.F(xx))(\lambda x.F(xx))[[nil]]))\\ & {\to }_{\beta }^{\ast }[[succ]]([[succ][[0]]){\to }_{\beta }^{\ast }[[2]]\end{array}$$

Lecture 4

Recall:

$$\begin{array}{rl}& YF([[consa(consbnil)]])\\ & =(\lambda f.(\lambda x.f(xx))\lambda x.f(xx))F[[consa(consbnil)]]\\ & {\to }_{\beta }^{AOR}(\lambda f.f((\lambda x.f(xx))(\lambda x.f(xx))))F\dots \end{array}$$

This works under NOR, but not under AOR.

For recursion under eager evaluation, we need 3 things.

1. Modified reduction strategy - Applicative Order Evaluation (AOE)
   1. Choose the leftmost, innermost, redex that is not within the body of an abstraction.

$$\begin{array}{rl}& YF([[consa(consbnil)]])\\ & =(\lambda f.(\lambda x.f(xx))\lambda x.f(xx))F[[consa(consbnil)]]\\ & \xcancel{{\to }_{\beta }^{AOR}(\lambda f.f((\lambda x.f(xx))(\lambda x.f(xx))))F\dots }\\ & {\to }_{\beta }^{AOE}(\lambda x.F(xx))(\lambda x.F(xx))[[consa(consbnil)]]\\ & {\to }_{\beta }^{AOE}F((\lambda x.F(xx))(\lambda x.F(xx)))[[consa(consbnil)]]\\ & {\to }_{\beta }^{AOE}F(F((\lambda x.F(xx))(\lambda x.F(xx))))(cons-)\end{array}$$

2. Modified Y combinator: $Y^{\prime }=\lambda f.(\lambda x.f(\lambda y.xxy))(\lambda x.f(\lambda y.xxy))$. Note: $Y^{\prime }{\to }_{\eta }^{2}Y$.

$$\begin{array}{rl}& Y^{\prime }F(\dots )\\ & {\to }_{\beta }(\lambda x.F(\lambda y.xxy))(\lambda x.F(\lambda y.xxy))(\dots )\\ & {\to }_{\beta }F(\lambda y.(\lambda x.F(\lambda y.xxy))(\lambda x.F(\lambda y.xxy))y)(\dots )\end{array}$$

3. Short-circuit “if-then-else”

$$\begin{array}{r}[[\text{if }B\text{ then }T\text{ else }F]]=[[B]](\lambda x.[[T]])(\lambda x.[[F]])\end{array}$$

Type Theory

Consider

$$\begin{array}{rl}[[true\text{ id}]]& =(\lambda x.\lambda y.x)(\lambda z.z)\\ & {\to }_{\beta }\lambda y.\lambda z.z=[[false]]\end{array}$$

$(true\text{ id})$ produces false.

Unrestricted combinations $⟹$ unexpected results.

Question

Is there a way to do only things that “make sense”?

Introduce a system of types.

Type

• Set of values an expression can have
• Interpretation of raw data

Type system

• Set of types $+$ set of rules for assigning types

An expression is well-typed if a type is derivable for it from the rules, else, it is ill-typed.

Strong vs. Weak Typing - How strictly are the rules enforced?

Static vs. Dynamic Typing - When are the types determined?

• Static: At compile-time
• Dynamic: At run-time

Monomorphic vs. Polymorphic typing

• Monomorphic: Entities have a unique type
• Polymorphic: Entities can have multiple types

Focus: Strong, static, monomorphic (for now) typing

The Simply Typed $\lambda$-Calculus

Syntax:

$$\begin{array}{rl}⟨expr⟩& ::=⟨var⟩|⟨abs⟩|⟨app⟩\\ ⟨var⟩& ::=a|b|c|\cdots \\ ⟨abs⟩& ::=\lambda ⟨var⟩:⟨type⟩.⟨expr⟩\\ ⟨apps⟩& ::=⟨expr⟩⟨expr⟩\end{array}$$

Types:

$$\begin{array}{rl}⟨type⟩& ::=⟨primitive⟩|⟨constructed⟩\\ ⟨primitive⟩& ::=t_1|t_2|\cdots \\ ⟨constructed⟩& ::=⟨type⟩\to ⟨type⟩\end{array}$$

Primitive type: “Built-in”, e.g., int.

Constructed types: Built from other types. Constituent type $+$ type constructor

int -> bool is the type constructor for functions.

$\to$ is right-to-left associative. ${\tau }_1\to {\tau }_2\to {\tau }_3={\tau }_1\to ({\tau }_2\to {\tau }_3)\ne ({\tau }_1\to {\tau }_2)\to {\tau }_3$.

Type Checking / Type Inference

Type theory $\cong$ Institutionistic Implicational Logic

Called the Curry-Howard Isomorphism

Rules presented as a formal inference system (CS245)

$$\begin{array}{r}\frac{\text{premises}}{\text{conclusion}}\frac{p_1\dots p_n}{C}=\text{“If we can construct a proof of }{p}_1,\dots ,p_n,\text{ we have proof of }C\text{"}\end{array}$$

No premises $\frac{}{\text{conclusion}}$ - axioms. Conclusion always holds

Example

Modus Ponens:

$$\frac{p\to qp}{q}$$

$$\begin{array}{rl}& \frac{ab}{a\wedge b}\text{(}\wedge \text{ intro)}\\ & \frac{a\wedge b}{a}\frac{a\wedge b}{b}\text{(}\wedge \text{elim)}\end{array}$$

Type rules for ST$\lambda$C

Type Environment: Map from identifiers to types. List of $⟨$ name, type $⟩$ pairs “symbol table”. Denoted $A$ (“assumptions”) or $\Gamma$

$A(x)=$ “look up $x$ in $A$” - if $⟨x,\tau ⟩\in A$, $A(x)=\tau$.

Type Judgement: Statement of the form $A⊢E:\tau$. $E:\tau \equiv$ “Expr $E$ has type $\tau$“.

$A\underset{\text{“derivability"}}{\underbrace{⊢}}E:\tau \equiv$ “The statement $E:\tau$ is derivable from the assumptions in $A$“.

Variables:

$$\begin{array}{r}\frac{A(x)=\tau }{A⊢x:\tau }[var]\left(\text{or }\overline{A⊢x:A(x)}\right)\end{array}$$

Abstractions: Assume the parameter has the given type, then type the body.

$$\begin{array}{r}\frac{A,⟨x,{\tau }_1⟩⊢E:{\tau }_2}{A⊢(\lambda x:{\tau }_1.E):{\tau }_1\to {\tau }_2}[abs]\end{array}$$

Applications: Type the rator and the rand. Type of the rand must match the param type of the rator. The type of the expression is the result type of the rator.

$$\begin{array}{r}\frac{A⊢M:{\tau }_1\to {\tau }_{2}A⊢N:{\tau }_1}{A⊢MN:{\tau }_2}[app]\end{array}$$

Example

Find the type of $\lambda x:t_1.x$

$$\begin{array}{r}\frac{\frac{\{⟨x,t_1⟩\}(x)=t_1}{\{⟨x,t_i⟩\}⊢x:t_1}[var]}{\{\}⊢(\lambda x:t_1.x):t_1\to t_1}[abs]\end{array}$$

$\lambda x:t_1.\lambda y:t_1\to t_2.yx$

$$\begin{array}{r}\frac{\frac{\frac{A(y)=t_1\to t_2}{A⊢y:t_1\to t_2}[var]\frac{A(x)=t_1}{A⊢x:t_1}[var]}{\frac{A=\{⟨x,t_1⟩,⟨y,t_1\to t_2⟩\}⊢yx:}{\{⟨x,t_1⟩\}\lambda y:t_1\to t_2.yx:(t_1\to t_2)\to t_2}[abs]}}{\{\}⊢\lambda x:t_1.\lambda y:t_1\to t_2.yx:t_1\to (t_1\to t_2)\to t_2}[abs]\end{array}$$

Lecture 5

Evaluating Type Systems

Question

How do we know these rules work?

Two theorems: Progress and preservation.

Theorem

Let $E$ be a closed, well-typed term in the ST$\lambda$C, i.e. for some $A$, $\tau$, $A⊢E:\tau$. Then either $E$ is a value (WNF) or there is an expression $E^{\prime }$ such that $E{\to }_{\beta }{E}^{\prime }$.

Proof:

Induction on the length of the type derivation for $E$.

Cases:

1. $E$ is a variable. Impossible since $E$ is closed.
2. $E$ is an abstr. $⟹E$ is in WNF.
3. $E=MN$. Then the derivation for $E$ ends with

$$\begin{array}{r}\frac{A⊢M:{\tau }_1\to \tau A⊢N:{\tau }_1}{A⊢E:\tau }\end{array}$$

By induction, $M$, $N$ are in WNF or reducible.

If $M$ or $N$ is reducible, then so is $E=MN$. If neither is reducible, both are values.

In that case, $M$ is some value $\lambda x:\tau .M$‘.

$$\begin{array}{r}\frac{⋮}{\frac{\overline{A⊢(\lambda x:\tau .M^{\prime }):{\tau }_1\to \tau }A⊢N:{\tau }_1}{⋮}}\end{array}$$

And this is reducible $■$.

Progress $⟹$ can’t be stuck e.g. can’t derive a type for $1+true$.

Theorem

(Preservation, Subject-Reduction Theorem): Let $A$ be a type environment, $P$ and $Q$ be $\lambda$-expressions such that $P{\to }_{\beta \eta }^{\ast }Q$ (i.e. $P$ reduces to $Q$ by $\ge 0$ steps of $\beta$ and/or $\eta$ reduction). Suppose $A⊢P:\tau$. THen $A⊢Q:\tau$.

Preservation: Well-typed terms continue to be well-typed after reduction.

Progress $+$ Preservation $⟹$ Safety

$$\begin{array}{rl}& E\text{well-typed}\\ \text{Progress}& \downarrow \\ & E\text{reducible or }E\text{ value}\\ & E{\to }_{\beta }{E}^{\prime }\\ \text{Preservation}& \downarrow \\ & E^{\prime }\text{well-typed}\\ \text{Progress}& \downarrow \\ & E^{\prime }\text{reducible or value}\end{array}$$

Well-typed terms either reduce forever, or reach a sensible value.

Theorem

(Strong Normalization Theorem): The set of well-typed terms in the ST$\lambda$C is strongly normalizing - that is, infinite reductions are impossible.

$⟹$ ST$\lambda$C is not Turing complete.

Intuition: Consider $(\lambda x.xx)(\lambda x.xx)$.

Question

What type can we give $\lambda x.xx$?

If the second $x$ has some type ${\tau }_1$, then the first $x$ must have some type ${\tau }_1\to {\tau }_2$.

There is no way ${\tau }_1$ and ${\tau }_1\to {\tau }_2$ can represent the same type. $\therefore$ no type for $x$ in this context. $\therefore$ no type for $\lambda x.xx$. $\therefore$ no type for $(\lambda x.xx)(\lambda x.xx)$.

Cannot type $Y$ either, so would need special facilities to support recursion.

Polymorphism

Entities having multiple types.

Cardelli & Wegner (1985): Hierarchy of polymorphism

flowchart LR
a[Polymorphism]
b[Universal]
c[Ad hoc]
d[Parametric]
e[Inclusion]
f[Overloading]
g[Coercion]
a --> b
a --> c
b --> d
b --> e
c --> f
c --> g

Definition

Universal: Generally, one implementation with many types. Unbounded number of specializations. Works on unknown (not yet created) types.

Definition

Parametric: “Type parameter” (possibly implicit)

function id (x : t) : t { return x} $\approx$ generic programming: ML, Haskell

Definition

Inclusion: “Sub-typing” - hierarchy of types. Use a subtype anywhere that calls for a supertype. OO languages.

Definition

Ad-hoc: Generally several implementations. Bounded number of specializations. Usually only on known (existing) types.

Definition

Overloading: “Name sharing”. Functions with the same name and different types

Definition

Coercion: Types automatically converted.

System F (2nd order $\lambda$-Calculus)

Discovered independently by Girard (“System F”) and Reynolds (“polymorphic $\lambda$-calculus”). Models parametric polymorphism.

Example

$$\begin{array}{rlrl}& \lambda x:\mathrm{int}.x& & \text{id for ints}\\ & \lambda x:\mathrm{bool}.x& & \text{id for bool}\\ & \lambda x:\mathrm{int}\to \mathrm{int}.x& & \text{id for functions}\end{array}$$

Same implementation, different annotations> Idea is to make the type a parameter to the function.

$$\begin{array}{rl}⟨expr⟩& ::=⟨var⟩|⟨abs⟩|⟨app⟩|⟨t-abs⟩|⟨t-app⟩\\ ⟨var⟩& ::=a|b|c\dots \\ ⟨abs⟩& ::=\lambda ⟨var⟩:⟨type⟩.⟨expr⟩\\ ⟨app⟩& ::=⟨expr⟩⟨expr⟩\\ ⟨t-abs⟩& ::=\Lambda ⟨t-var⟩.⟨expr⟩\\ ⟨t-app⟩& ::=⟨expr⟩\{⟨type⟩\}\end{array}$$ $$\begin{array}{rl}⟨type⟩& ::=⟨prim⟩|⟨t-var⟩|⟨type⟩\to ⟨type⟩|\forall ⟨t-var⟩\\ ⟨prim⟩& ::=t_1|t_2|\cdots \\ ⟨t-var⟩& ::=\alpha |\beta |\gamma |\cdots \end{array}$$

$var$, $abs$, $app$ are as before. $t-abs$, $t-app$ are type abstraction, type application. $t-var$ is a type variable, placeholder for types.

$\forall ⟨t-var⟩.⟨type⟩$ - quantified type, the type of a type abstraction.

$$\begin{array}{rlrl}& \lambda x.:intx& & \lambda x:bool.x\\ & int\to int& & bool\to bool\end{array}$$ $$\begin{array}{rl}& \text{replace }int,bool\text{ with a type variable}\\ & (\lambda x:\alpha .x)\end{array}$$

$\alpha$ is a free type variable. Its meaning depends on external context.

Now abstract over $\alpha$ $id=\Lambda \alpha .\lambda x:a.x:\forall \alpha .\alpha \to \alpha$.

To apply $id$:

$$\begin{array}{rl}& id\{int\}3\\ & =(\Lambda \alpha .\lambda x:a.x)\{int\}3\\ & {\to }_{\beta }(\lambda x:int.x)3\\ & {\to }_{\beta }3\end{array}$$ $$\begin{array}{rl}& id\{bool\}true\\ & =(\Lambda \alpha .\lambda x:\alpha .x)\{bool\}true\\ & {\to }_{\beta }(\lambda x:bool.x)true\\ & {\to }_{\beta }true\end{array}$$

Type rules:

$$\begin{array}{r}\frac{A(x)=\tau }{A⊢x:\tau }[var]\end{array}$$ $$\begin{array}{r}\frac{⟨x,\tau ⟩,A⊢E:{\tau }_2}{A⊢(\lambda x:{\tau }_1.E):{\tau }_1\to {\tau }_2}[abs]\end{array}$$ $$\begin{array}{r}\frac{A⊢M:{\tau }_1\to {\tau }_{2}A⊢N:{\tau }_1}{A⊢MN:{\tau }_2}[app]\end{array}$$

These are the same. Need to create two new rules.

$$\begin{array}{r}\frac{A⊢E:\tau }{A⊢\Lambda \alpha .E:\forall a.\tau }[t-abs](\alpha \text{ not free in }A)\end{array}$$ $$\begin{array}{r}\frac{A⊢E:\forall \alpha .{\tau }_1}{A⊢(E\{{\tau }_2\}):{\tau }_1[{\tau }_2/\alpha ]}[t-app]\end{array}$$

Nested Quantifiers

Say $f:(\forall \alpha .\alpha \to \alpha )\to int$. Parameter type is $\forall \alpha .\alpha \to \alpha$. Result type is $int$. $\therefore$ $f$ is not a polymorphic function, it requires a polymorphic function as its argument, then returns $int$.

$g:((\forall \alpha .\alpha \to \alpha )\to int)\to (\forall \beta .\beta \to (\beta \to \beta ))$

Lecture 6

Abstract out the self-application:

$idid{=}_{\beta }(\lambda x.xx)id$.

So

$$\begin{array}{rl}& (\Lambda \alpha .\lambda x:\alpha .x)\{\forall \alpha .\alpha \to \alpha \}(\Lambda \alpha .\lambda x:\alpha .x)\\ & {=}_{\beta }(\lambda x:\forall \alpha .\alpha \to \alpha .x\{\forall \alpha .\alpha \to \alpha \}x)(\Lambda \alpha .\lambda x:\alpha .x)\end{array}$$

So $\lambda x:\forall \alpha .\alpha \to \alpha .x\{\forall \alpha .\alpha \to \alpha \}x$ is a well-typed implementation of $\lambda x.xx$.

$$\begin{array}{rl}& \overline{A⊢x:\forall \alpha .\alpha \to \alpha }\\ & \overline{A⊢x\{\forall \alpha .\alpha \to \alpha \}:\to (\forall \alpha .\alpha \to \alpha )}\overline{A⊢x:\forall \alpha .\alpha \to \alpha }\\ & \overline{A=\{⟨x,\forall \alpha .\alpha \to \alpha ⟩\}⊢x\{\forall \alpha .\alpha \to \alpha \}x:\forall \alpha .\alpha \to \alpha }\\ & \overline{\{\}⊢(\lambda x:\forall \alpha .\alpha \to \alpha .x\{\forall \alpha .\alpha \to \alpha \}x):(\forall \alpha .\alpha \to \alpha )\to (\forall \alpha .\alpha \to \alpha )}\end{array}$$

$\therefore$ $\lambda x.xx$ can be written as $\lambda x:\forall \alpha .\alpha \to \alpha .x\{\forall \alpha .\alpha \to \alpha \}x$ with type ($\forall \alpha .\alpha \to \alpha )\to (\forall \alpha .\alpha \to \alpha )$.

Another solution

$$\begin{array}{rl}& \overline{A⊢x:\forall \alpha .\alpha \to \alpha }\overline{A⊢x:\forall \alpha .\alpha \to \alpha }\\ & \overline{A⊢x\{t_1\to t_2\}:(t_1\to t_1)\to (t_1\to t_1)}\overline{A⊢x\{t_1\}:t_1\to t_1}\\ & \overline{A=\{⟨,x,\forall \alpha .\alpha \to \alpha ⟩\}⊢(x\{t_1\to t_1\})(x\{t_1\}):t_1\to t_1}\\ & \overline{\{\}⊢(\lambda x:\forall \alpha .\alpha \to \alpha .(x\{t_1\to t_1\})(x\{t_1\})):(\forall \alpha .\alpha \to \alpha )\to t_1\to t_1}\end{array}$$

So $\lambda x.xx$ can have type $(\forall \alpha .\alpha \to \alpha )\to t_1\to t_1$. Replace $t_1$ with $\beta$ and abstract.

$$\begin{array}{rl}& ⋮\\ & \overline{\{\}⊢\lambda x:\forall \alpha .\alpha \to \alpha .(x\{\beta \to \beta \})(x\{\beta \}):(\forall \alpha .\alpha \to \alpha \to \beta \to \beta )}\\ & \overline{\{\}⊢\Lambda \beta .\lambda x:\forall \alpha .\alpha \to \alpha .(x\{\beta \to \beta \})(x\{\beta \}):\forall \beta .(\forall \alpha .\alpha \to \alpha )\to (\beta \to \beta )}\end{array}$$

So $\forall \beta .(\forall \alpha .\alpha \to \alpha )\to (\beta \to \beta )$ is another valid type.

Another solution

$$\begin{array}{rl}& \overline{A⊢x:\forall \alpha .\alpha }\overline{A⊢x:\forall \alpha .\alpha }\\ & \overline{A⊢x\{\beta \to \beta \}:\beta \to \beta }\overline{A⊢x\{\beta \}:\beta }\\ & \overline{A=\{⟨x,\forall \alpha .\alpha ⟩\}⊢(x\{\beta \to \beta \})(x\{\beta \}):\beta }\\ & \overline{\{\}⊢\lambda x:\forall \alpha .\alpha .(x\{\beta \to \beta \})(x\{\beta \}):(\forall \alpha .\alpha )\to \beta }\\ & \overline{\{\}⊢\Lambda \beta .\lambda x:\forall \alpha .\alpha .(x\{\beta \to \beta \})(x\{\beta \}):\forall \beta (\forall \alpha .\alpha )\to \beta }\end{array}$$

So $\forall \beta .(\forall \alpha .\alpha )\to \beta$ is another valid type.

Three valid types for $\lambda x.xx$.

$$\begin{array}{rl}& (\forall \alpha .\alpha \to \alpha )\to (\forall \alpha .\alpha \to \alpha )\\ & \forall \beta .(\forall \alpha .\alpha \to \alpha )\to \beta \to \beta \\ & \forall \beta .(\forall \alpha .\alpha )\to \beta \\ & \text{and many more}\end{array}$$

Question

What kinds of programs can we write in System F?

Question

Which of our untyped constructions actually type-check?

Booleans:

$$\begin{array}{l}\lambda x.\lambda y.x\\ \lambda x.\lambda y.y\end{array}\}\begin{array}{l}\Lambda \alpha .\lambda x:\alpha .\lambda y:\alpha .x\\ \Lambda \alpha .\lambda x:\alpha .\lambda y:\alpha .y\end{array}\}\forall \alpha .\alpha \to \alpha \to \alpha$$

Let $[[Bool]]=\forall \alpha .\alpha \to \alpha \to \alpha$.

Natural #‘s - Church numerals: $[[n]]=\lambda f.\lambda x.f^n(x)$.

If $x$ has type $\alpha$, $f$ must have type $\alpha \to \alpha$ (since $f$‘s result is passed back to $f$).

So $[[n]]=(\Lambda \alpha .\lambda f:\alpha \to \alpha .\lambda x:\alpha .f^{n}x):\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha$

Let $[[Nat]]=\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha$.

Plus - $\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$

$$\begin{array}{r}\lambda m:[[Nat]].\lambda n:[[Nat]].\underset{\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha =[[Nat]]}{\underbrace{\Lambda \alpha .\lambda f:\alpha \to \alpha .\lambda x:\alpha .\underset{\alpha }{\underbrace{\underset{\alpha \to \alpha }{\underbrace{m\{\alpha \}f}}(\underset{\alpha }{\underbrace{\underset{\alpha \to \alpha }{\underbrace{\underset{(\alpha \to \alpha )\to (\alpha \to \alpha )}{\underbrace{n\{\alpha \}}}\underset{\alpha \to \alpha }{\underbrace{f}}}}\underset{\alpha }{\underbrace{x}}}}}}}})\end{array}$$

$[[Nat]]\to [[Nat]]\to [[Nat]]$.

Times - $\lambda m.\lambda n.\lambda f.m(nf)$

$$\begin{array}{r}\lambda m:[[Nat]].\lambda m:[[Nat]].\underset{\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha =[[Nat]]}{\underbrace{\Lambda a.\lambda f:\alpha \to \alpha .\underset{\alpha \to \alpha }{\underbrace{\underset{(\alpha \to \alpha )\to (\alpha \to \alpha )}{\underbrace{m\{\alpha \}}}(\underset{\alpha \to \alpha }{\underbrace{\underset{(\alpha \to \alpha )\to (\alpha \to \alpha )}{\underbrace{n\{\alpha \}}}\underset{(\alpha \to \alpha )}{\underbrace{f}}}}}}}})\end{array}$$

$[[Nat]]\to [[Nat]]\to [[Nat]]$.

Question

Is there a way to not pull these out of a hat?

No.

Exponents - $\lambda m.\lambda n.nm$

$$\begin{array}{r}\lambda m:[[Nat]].\lambda n:[[Nat]].\Lambda \underset{\forall \alpha .(\alpha \to \alpha )\to \alpha \to \alpha }{\underbrace{\underset{((\alpha \to \alpha )\to (\alpha \to \alpha ))\to ((\alpha \to \alpha )\to (\alpha \to \alpha ))}{\underbrace{\alpha .(n\{\alpha \to \alpha \})}}(\underset{(\alpha \to \alpha )\to (\alpha \to \alpha )}{\underbrace{m\{\alpha \}}}}})\end{array}$$

$[[Nat]]\to [[Nat]]\to [[Nat]]$.

Polymorphism in $Nat$ is essential for this type-check.

Pairs:

$$\begin{array}{rl}[[cons]]& =\lambda h.\lambda t.\lambda s.sht\\ & =\Lambda \alpha .\Lambda \beta .\lambda h:\alpha .\lambda t:\beta .\lambda s:\alpha \to \beta \to \gamma .\underset{\gamma }{\underbrace{\underset{\beta \to \gamma }{\underbrace{\underset{\alpha \to \beta \to \gamma }{\underbrace{s}}\underset{\alpha }{\underbrace{h}}}}t}}\end{array}$$

If $h:{\tau }_1$, $t:{\tau }_2$ then $[[cons]]\{{\tau }_1\}\{{\tau }_2\}ht:\forall \gamma ({\tau }_1\to {\tau }_2\to \gamma )\to \gamma$.

So $[[pair{\tau }_1{\tau }_2]]=\forall \alpha .({\tau }_1\to {\tau }_2\to \alpha )\to \alpha$.

Lecture 7

Recall for pairs,

$$\begin{array}{rl}[[cons]]& =\Lambda \alpha .\Lambda \beta .\lambda t:\beta .\Lambda \gamma .\lambda s:\alpha \to \beta \to \gamma .sht\\ & :\forall \alpha .\forall \beta .\alpha \to \beta \to \forall \gamma .(\alpha \to \beta \to \gamma )\to \gamma \end{array}$$

So $[[pair]]=\forall \alpha .({\tau }_1\to {\tau }_2\to \alpha )\to \alpha$.

Lists: Can’t just nest pairs. Types won’t be the same.

$$\begin{array}{r}[[pair{\tau }_1{\tau }_2]]\ne [[pair{\tau }_1(pair{\tau }_1{\tau }_2)]]\end{array}$$

Represent a list by its foldr function:

$$\begin{array}{r}\text{lst }\ell =\lambda f.\lambda e.foldrfe\ell \end{array}$$

$[[(\text{list }{\ell }_1{\ell }_2{\ell }_3)]]=\lambda f.\lambda e.f{\ell }_1(f{\ell }_2(f{\ell }_{3}e))$

If ${\ell }_1,{\ell }_2,{\ell }_3:\tau$

Then $f:\tau \to \underset{\text{type of }e\text{, also the result type of }f}{\underbrace{\beta }}\to \beta$

$$\begin{array}{rl}[[list{\ell }_1{\ell }_2{\ell }_3]]& =\Lambda \alpha .\lambda f:\tau \to \alpha \to \alpha .\lambda e:\alpha .f{\ell }_1(f{\ell }_2(f{\ell }_{3}e))\\ & :\forall \alpha .(\tau \to \alpha \to \alpha )\to \alpha \to \alpha \end{array}$$

The type $[[\text{list of }\tau ]]=\forall \alpha .(\tau \to \alpha \to \alpha )\to \alpha \to \alpha$.

$$\begin{array}{r}\underset{\text{take head and tail}}{\underbrace{\lambda h.\lambda t}}.\stackrel{\text{construct a list with }h\text{ at the head}}{\overbrace{\lambda f}}.\lambda e.fh\underset{\text{fold }f\text{, }e\text{ over the tail}}{\underbrace{(tfe)}}\end{array}$$

$\Lambda \alpha .\lambda h:\alpha .\lambda t:[[\text{list of }\alpha ]].\Lambda \beta .\lambda f:(\alpha \to \beta \to \beta ).\lambda e.\beta .fh(t\{\beta \}fe)$

$\forall \alpha .\alpha \to [[\text{list of }\alpha ]]\to [[\text{list of }\alpha ]]$

Conclusion: You can do a lot in System F.

Theory: Progress and Preservation hold for System F.

However, System F is strongly normalizing, so it is not Turing Complete.

ML (Meta-Language)

Robin Milner, 1978

Major dialects: SML (Standard ML) Caml (Categorical Abstract Machine Language

Standard ML of New Jersey

ML is a mostly functional, statically typed, eager evaluation.

1 + 2; 

ML responds with

$$\begin{array}{r}\text{val}\stackrel{\text{name given to the most recently evaluated expression}}{\overbrace{\text{it}}}=\underset{\text{value of result}}{\underbrace{3}}:\underset{\text{type of result}}{\underbrace{int}}\end{array}$$

Declarations:

val x : int = 1; (*case-sensitive*)

ML:

val x = 1 : int
x + 3;
- val it = 4 : int

Functions

val f = fn ( x : int ) => x + 1; 
- val f = fn : int -> int *function from int -> int*

Does not permit recursive definitions.

Recursion

val rec fact = fn ( n : int ) => 
	if n = 0 then 1 else n * fact (n-1)

Shorthand

fun f ( x : int ) = x + 1
fun fact ( n : int ) = if n = 0 then 1 
	else n * fact(n-1)

FYI: Negation is ~ tilde.

Primitive types: int, bool, real, char, string.

Constructed types: functions $(\to )$, tuples (cartesian product) (*).

(3, true) : int * bool

val x = (4,3);
	val x = (4,3): int * int
 
#1 x; 
	val it = 4 : int
	
#2 x
	val it = 3 : int

Lists: Homogeneous

[1,2,3];
	val it = [1,2,3] : int list
 
(*empty list : nil)

Functions: All functions in ML accept exactly one parameter.

Question

How do we pass multiple parameters?

Solution 1: Pass a tuple

fun add (x : int * int) = #1 x + #2 x
	 val add = fn : int * int -> int
 
val x = (3,4);
add x (or add (3,4))

Solution 2: $\lambda$-calculus approach

val add = fn(x : int) => fn (y : int) x + y 
	vall add = fn : int -> int -> int
	
add 3 4

Curried, permits partial application.

Shorthand for Solution 1

fun add (x : int , y : int ) = x + y
	val add = fn : int * int -> int

This is a pattern, parameter is a pair.

For solution 2:

fun add (x : int ) (y : int) = x + y
	int -> int -> int

Question

What if a function takes no parameters.

Degenerate type unit only value is ()

fun f ( x : unit) = 5
	val f = fn : unit -> int
	
(*f(); 5)

Shorthand:

fun f() = 5
	val f = fn : unit -> int

Pattern, matches type unit.

Question

May have noticed, assigning types in System F is tricky. Wouldn’t it be nice if there was a tool to automatically convert untyped expressions to their typed equivalents?

Type inference.

Lecture 8

Recall: Assigning types in System F is tricky.

Definition

The erasure of a term in System F is defined as

$$\begin{array}{rl}\mathrm{erase}(x)& =x\\ \mathrm{erase}(\lambda x:\tau .E)& =\lambda x.\mathrm{erase}\\ \mathrm{erase}(MN)& =\mathrm{erase}(M)\mathrm{erase}(N)\\ \mathrm{erase}(\Lambda \alpha .E)& =\mathrm{erase}(E)\\ \mathrm{erase}(E\{\tau \})& =\mathrm{erase}(E)\end{array}$$

The type inference problem is: given an untyped term $E$, find a term $E^{\prime }$ that is well-typed in System F, such that $\mathrm{erase}(E^{\prime })=E$.

Theorem

The type inference problem for System F is undecidable.

So confine ourselves to a decidable subset.

Hindley-Milner Polymorphic$\lambda$-Calculus

Restriction: Quantifiers cannot be nested inside $\to$, i.e. outermost only. This means no polymorphic parameters. $\forall \alpha .\alpha \to \alpha$ is okay, $(\forall \alpha .\alpha \to \alpha )\to int$ is not.

Syntax: Identical to untyped $\lambda$-calculus.

Types:

$$\begin{array}{rl}⟨monotype⟩& ::=⟨primitive⟩|⟨constructed⟩|⟨tyvar⟩\\ ⟨primitive⟩& ::=t_1|t_2|\cdots \\ ⟨constructed⟩& ::=⟨monotype⟩\to ⟨monotype⟩\\ ⟨tyvar⟩& ::=\alpha |\beta |\cdots \\ ⟨polytype⟩& ::=⟨monotype⟩|\forall ⟨tyvar⟩⟨polytype⟩\end{array}$$

We assign polytypes to top-level expressions. Abstractions may only demand that their arguments have a monotype.

E.g.

$$\begin{array}{r}id=\lambda x.x:\underset{\text{polytype}}{\underbrace{\forall \alpha .\alpha \to \alpha }}\\ (\text{implicitly}:\lambda x:\alpha .x:\forall \alpha .\alpha \to x)\end{array}$$

Note: Can still have polymorphic values as arguments.

$f(\underset{\forall \alpha .\alpha \to \alpha }{\underbrace{\lambda x.x}})$ is still valid, but $f$ can non longer demand polymorphism.

No type annotations $⟹$ types assigned purely by inference.

Type rules: Let $\tau$ range over monotypes, and $\sigma$ range over polytypes.

$$\begin{array}{rlr}& \frac{A(x)=\tau }{A⊢x:\tau }& [var]\\ & \frac{A⊢M:{\tau }_1\to {\tau }_{2}A⊢N:{\tau }_1}{A⊢MN:{\tau }_2}& [app]\\ & \frac{\{⟨x,{\tau }_1⟩\}+A⊢E:{\tau }_1}{A⊢\lambda x.E:{\tau }_1\to {\tau }_2}& [abs]\end{array}$$

New rules

$$\begin{array}{rlr}& \frac{A⊢E:\forall \alpha .\sigma }{A⊢E:\sigma [\tau /\alpha ]}& [spec]\\ & \frac{A⊢E:\sigma }{A⊢E:\forall \alpha .\sigma }& [gen]\end{array}$$

Can quantify any variable that is not being used in an enclosing expression (i.e. not free in $A$).

Question

How do we do type inference?

Rules are not syntax-directed. A set of rules is syntax-directed if

1. Exactly one rule for each element of abstract syntax.
2. Semantics (type) of an expression is completely determined by the semantics of its pieces.

Type rules not syntax-directed $⟹$ choices to make, inference is harder.

ML (Polymorphic)

fun f x = x + 1;
	val f = fn : int -> int
  
fun g (x, y) = x + y;
	val g = fn : int * int -> int
 
fun h x y = x + y;
	val h = fn : int -> int -> int

ML chooses int by default for arithmetic operators.

If you want real:

fun f ( x : real ) y = x + y
fun f x ( y : real ) = x + y
fun f x y = x + y : real

Polymorphism

fun id x = x
	val id = fn : 'a -> 'a   

Pattern matching

fun append (x,y) = 
	if x = nil then y 
	else hd x :: append(tl x, y)

Better

fun append ([], y) = y | appned (x :: xs, y) = x::append(xs, y)

fun merge([], N) = n 
| merge(M, []) = M 
| merge()M as m::ms, N as n::ns) = 
if m < n then m::merge(ms, N) 
else n::merge(M, ns)

Special pattern: _ wild-card “don’t-care” pattern.

fun empty [] = true 
| empty _ = false

Split a list:

fun split [] = ([], [])
| split[a] = ([a], [])
| split (a::b::cs) = 
let val (M, N) = split cs
in (a::M, b::N)
end

fun mergesort L = 
	let val (M,N) = split L
		val M' = mergesort M
		val N' = mergesort N
	in
		merge(M, N')
end

let 
	<decl1>
	.
	.
	<decl2>
in
	<body>
end

Establishes a local environment. decl1, $\dots$ , decln evaluate and bound in the order in which they appear. decli is visible in declj for $j>i$ and in <body>.

Higher-order functions:

fun foldl fe [] = e
| foldl f e (x::xs) = foldl f (f(x,e))xs

Building our own types:

type intpair = int * int (* creates a type synonym)

Construct a new type:

datatype suit = heart | spade | diamond | club;

Binary tree

datatype 'a tree = Empty | Node of 'a * 'a tree * 'a tree

fun dfs Empty _  = false
| dfs (Node(x,L,R)) y = x = y
	orelse dfs L y
	orelse dfs R y
 
	val dfs = fn : ''a tree -> ''a -> bool

Special type variable ''a can only be instantiated with an eqtype, a type that can be compared for equality.

eqtypes are int, bool, char, unit, tuples and lists of these, data types based on these.

Not eqtypes - real, functions.

Lecture 9

Definition

Let ${\tau }_1$ and ${\tau }_2$ be types, $S$ a unifier of ${\tau }_1$ and ${\tau }_2$. $S$ is a Most General Unifier (MGU) of ${\tau }_1$ and ${\tau }_2$ if for every unifier $S^{\prime }$ of ${\tau }_1$ and ${\tau }_2$ there exists a substitution $S^{\prime \prime }$ such that $S^{\prime }=S^{\prime \prime }\circ S$.

If ${\tau }_1$ and ${\tau }_2$ have a unifier, then they have an MGU.

Algorithm - Robinson’s Unification Algorithm

Given types ${\tau }_1$ and ${\tau }_2$, find an MGU if one exists

$$\begin{array}{rl}U(t,t)& =[]\\ U(t_1,t_2)& =\text{error}(t_1\ne t_2)\\ U(t,{\tau }_1\to {\tau }_2)& =U({\tau }_1\to {\tau }_2,t)=\text{error}\end{array}$$ $$\begin{array}{r}U({\tau }_1\to {\tau }_2\to {\tau }_3\to {\tau }_4)=\text{let}\\ s_1=U({\tau }_1,{\tau }_3)\\ s_2=U({\tau }_2{s}_1,{\tau }_4{s}_1)\\ {\text{in}}_{s_2{s}_1}\end{array}$$

int $\to \alpha$, $\beta \to$ bool [bool / $\alpha$, int / $\beta$] is a unifier $\alpha \to$ int, $\alpha \to$ bool - no unifier $\alpha \to$ int, $\beta \to$ int [int / $\alpha$, int / $\beta$] is a unifier, [$\alpha /\beta$] is a unifier.

$$\begin{array}{r}U(\alpha ,\tau )=U(\tau ,\alpha )=\{\begin{array}{ll}\text{error}& \text{if }\tau \text{ is a constructed type containing }\alpha \ast \\ [\tau /\alpha ]& \text{ otherwise}\end{array}\end{array}$$

Condition $\ast$ called the occurs-check.

Example

$\alpha$, $\alpha \to \beta$ can never represent the same type. Without the occurs-check, $U(\alpha ,\alpha \to \beta )=[\alpha \to \beta /\alpha ]$.

$$\begin{array}{rl}{\tau }_1=\alpha \to (\beta \to \gamma ){\tau }_2=(\gamma \to \beta )\to \alpha & \\ U({\tau }_1,{\tau }_2)& =U(\alpha \to (\beta \to \alpha ),(\gamma \to \beta )\to \alpha )\\ & =\text{let}\\ s_1& =U(\alpha ,\gamma \to \beta )=[\gamma \to \beta /\alpha ]\\ s_2& =U((\beta \to \gamma )[\gamma \to \beta /\alpha ],\alpha [\gamma \to \beta /\alpha ])\\ & =U(\beta \to \gamma ,\gamma \to \beta )\\ & =\text{let}\\ & =s_3=U(\beta ,\gamma )=[\gamma /\beta ]\\ s_4& =U(\gamma [\gamma /\beta ],\beta [\gamma /\beta ])\\ & =U(\gamma ,\gamma )=[]\end{array}$$ $$\begin{array}{rl}i{n}_{s_4\circ s_3}& =[]\circ [\gamma /\beta ]=[\gamma /\beta ]\\ i{n}_{s2\circ s_1}& =[\gamma /\beta ]\circ [\gamma \to \beta /\alpha ]\\ & =[\gamma \to \beta /\alpha ,\gamma /\beta ]{\tau }_1[\gamma \to \beta /\alpha ,\gamma /\beta ]\\ & =(\alpha \to (\beta \to \gamma ))[\gamma \to \beta /\alpha ,\gamma /\beta ]\\ & =((\gamma \to \beta )\to (\beta \to \gamma ))[\gamma /\beta ]\\ & =(\gamma \to \gamma )\to \gamma \to \gamma )\\ {\tau }_2[\gamma \to \beta /\alpha ,\gamma /\beta ]& =((\gamma \to \beta )\to \alpha )[\gamma \to \beta /\alpha ,\gamma /\beta ]\\ & =((\gamma \to \beta )\to (\gamma \to \beta ))[\gamma /\beta ]\\ & =(\gamma \to \gamma )\to (\gamma \to \gamma )\end{array}$$

Substitution across environments:

$$\begin{array}{rl}\{\}S& =\{\}\\ (⟨x,\tau ⟩+A)S& =⟨x,\tau S⟩+AS\end{array}$$

Algorithm $W$: takes a type environment and an expression. Returns a substitution and a type.

Variables: Look up in environment, return empty substitution. $W(A,x)=⟨[],A(x)⟩$.

Abstractions: Type the body with $x$ bound to a fresh type variable, then construct the type.

$$\begin{array}{rl}W(A,\lambda x.E)& =\text{let}\\ & ⟨S,\tau ⟩=W(⟨x,\alpha ⟩+A,E)quad\alpha \text{ is a fresh type var}\\ & \text{in}\\ & ⟨S,\alpha S\to \tau ⟩\end{array}$$

Applications:

• Type rator and rand
• Type of rand must match parameter type of rator (unification)
• Result is the result type of the rator

$$\begin{array}{rl}W(A,MN)& =\text{let}\\ & ⟨S_1,{\tau }_1⟩=W(A,M)\\ & ⟨S_2,{\tau }_2⟩=W(A{S}_1,N)\\ & S_3=U({\tau }_2\to \alpha ,{\tau }_1{S}_2)\alpha \text{ is a fresh type var}\\ & {\text{in}}_{⟨S_3\circ S_2\circ S_1,\alpha S_3⟩}\end{array}$$

Extensions: Milner

Conditionals: if $E_1$ then $E_2$ else $E_3$

• $E_1$ must have type bool
• $E_2$ and $E_3$ must have the same type
• result is the type of $E_2$ and $E_3$

$$\begin{array}{r}\frac{A⊢E_1:boolA⊢E_2:\tau uA⊢E_3:\tau }{A⊢\text{ if }{E}_1\text{ then }{E}_2\text{ else }{E}_3:\tau }\end{array}$$ $$\begin{array}{rlr}w(A,\text{if }{E}_1\text{ then }{E}_2\text{ else }{E}_3)& =\text{let}& \\ & ⟨s_1,{\tau }_1⟩& =w(A,E_1)\\ s_2& =U({\tau }_1,bool)& \\ ⟨s_3,{\tau }_3⟩& =w(A(s_2\circ s_1),E_2)& \\ ⟨s_4,{\tau }_4⟩& =W(A(s_3\circ s_2\circ s_1),E_3)& \\ s_5& =U({\tau }_3{s}_4,{\tau }_4)& \\ & {\text{in}}_{⟨s_5\circ s_4\circ s_3\circ s_2\circ s_1,{\tau }_4{s}_3⟩}& \end{array}$$

H-M calculus - strongly normalizing. $\therefore$ need explicit facilities for recursion. $(\text{fix }xE)$ computes the fixed point of $\lambda x.E$.

$$\begin{array}{r}\frac{⟨x,\tau ⟩+A⊢E:\tau }{A⊢(\text{fix }xE):\tau }\end{array}$$ $$\begin{array}{rl}w(A,\text{fix }xE)& =\text{let}\\ ⟨s_1,{\tau }_1⟩& =W(⟨x,\alpha ⟩+A,E)\alpha \text{ a fresh type var}\\ s_2& =U(\alpha s_1,{\tau }_1)\\ & {\text{in}}_{⟨s_2\circ s_1,\alpha (s_2\circ s_1)⟩}\end{array}$$

Name-binding $(\text{let }(x{E}_1)E_2)$

Evaluates $E_2$ with $x$ bound to the $E_1$.

Operationally equivalent to $(\lambda x.E_2)E_1$.

Milner’s observation: The argument $E_1$ is guaranteed to be present. So if $E_1$ is polymorphic, $E_2$ can take advantage of the polymorphism.

Consider

$$\begin{array}{r}\lambda f.\text{if}(ftrue)\text{then}(f0)\text{else}1\end{array}$$

But we can’t demand polymorphism in the H-M calculus. But if the argument is present

$$\begin{array}{r}(\lambda f.\text{if}(ftrue)\text{then}(f0)\text{else}1)(\lambda x.x)\end{array}$$

Then we could use the polymorphism

$$\begin{array}{rl}=(\text{let}(f(\lambda x.x))& \\ (\text{if }& (ftrue)\\ & \text{then }(f0)\text{else}1)))\end{array}$$

Lecture 10

(Missed the first 55 minutes of the lecture)

ML Exceptions

exception DivByZero;
fun safeDiv(_, 0) = raise DivByZero
	SafeDiv(x,y) = x div y
	
(* int x int -> int)

Handling exceptions

val quot = safeDiv(3,0) handle DivByZero => 0
	exn -> 'a

Parameterized exceptions

exception DivByZero of int *string
 
fun safeDiv(x,0) = raise DivByZero(x, "Division by Zero")
	safeDiv(x,y) = x div y
 
val quote = safeDiv(3,0) handle DivByZero(x,_) => x

Assignment is only permitted on reference variables.

val x = ref 5; (*mutable reference containing the value 5*)
	val x = ref 5 : int ref
 
val x = !x (*dereference*)
	val y = 5 : int
x := !x + 1; (* assignment - returns unit*)
 
val it = 6 : int

Also: mutable arrays, loops: while <expr> do <expr>.

I/O: print "Hello"

Real.toString
Int.toString

Real and Int are modules.

Sequencing: ( ; ; ; e) are evaluated sequentially, result is e.

use "file.sml, load a file.

Type Errors

Type mismatch (hd tl)lst

ML Error: Operator and operand don’t agree.

Operator domain: 'Z list

Operand: 'Y list -> 'Y list

In expression: hd tl

Circularity

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

Operator domain: 'Z list * 'Z list list

Operand: 'Z list * 'Z

Can’t unify 'Z with 'Z list list in expression xs::x.

Similarly, cannot type $\lambda x.xx$. Type is circular (self-referential).

Can create self-referential types with datatype

fun fred x = (x, fn () => fred(x+1))

ML: Cannot unify int * unit -> 'Z with 'Z.

Solution:

datatype fredtype = Fred of int * unit -> fredtype

fun fred x = Fred(x, fn() -> fred(x+1))
	val fred = fn : int -> fredtype

Lecture 11

Skipped for interview

Lecture 12

Hiding helper functions, e.g. gcd:

local 
	fun gcd(x,y) =
in 
	fun plus r1 r2 = 
	fun times r1 r2 = 
end
(*can use local inside and outside of abstract types)

SML Module System

Structure: Collection of values, types, etc. -

structure Rational = struct
datatype rational = Rat of int * int
fun mkRat x y = Rat(x,y)
fun plus r1 r2 =
fun times r1 r2 = 
fun gcd(x,y) = 
end

val x = Rational.Rat(3,4)

Signature - the type of a structure.

signature RATIONAL = sig
	type rational
	val mkRat : int -> int -> rational
	val plus : rational -> rational -> rational
	val tmies : rational -> rational -> rational
end
structure RestrictedRational : RATIONAL = Rational

RestrictedRational.gcd is not visible.

Implementation of type rational is still visible.

Opaque structures:

structure OpaqueRational :> RATIONAL = Rational

Functor: High-level function (turn structures into other structures).

E.g.

signature COMPARABLE = sig
	eqtype element
	val leq : element * element -> bool
end
signature ORDERFIND = sig
	eqtype element
	val find : element list *element -> bool
end
functor MkOrderedFind(C : COMPARBALE) : ORDEREDFIND = struct
	type element = C.element
	fun find([], _) = false
		find(x :: xs, y) = if x = y then true
							else if C.leq(x,y) then find (xs, y)
							else false
end

structure IntPair = struct
	type element = int * int
	fun leq((x1, y1), (x2, y2)) = x1 <= x2 or else
								(x1 = x2 and also y1 <= y2)
end
structure IntPairFind = MkOrderedFind(IntPair)
IntPairFind.find(__)

Sharing declarations: putting 2 or more modules together.

Sometimes the combination only works if certain types are forced to be equal.

Modify OrderedFind to print out its findings instead of returning bool.

sig/struct for printable elements

signature PRINTABLE = sig
	eqtype element
	val toString : element -> string
end
functor MkOrderedPrintFind(structure C:COMPARABLE and P:PRINTABLE sharing
				type C.element = P.element) = struct
	type element = C.element
	fun find([], _) = ()
		find(x::xs, y) = if x = y then print(P.toString x^"\n")
				else if C.leq(x, y) then find (xs, y)
				else()
end
 
structure PrintableIntPair = struct
	type element = int * int
	fun toString(m,n) = "("^Int.toString m ^","^Int.toString n^")"
end
structure IntPairPrintFind = MkOrderedPrintFind(structure C = IntPair and P = PrintableIntPair)
IntPairPrintFind.find(_)

Existential Types

$\forall \alpha .\tau$, for any type ${\tau }^{\prime }$, the item has type $\tau [{\tau }^{\prime }/\alpha ]$ (polymorphism)

Question

What can be said of a type like $\exists \alpha .\tau$?

For some type ${\tau }^{\prime }$, the item has type $\tau [{\tau }^{\prime }/\alpha ]$. But we don’t know what ${\tau }^{\prime }$ is.

Consider the type $\exists \alpha .\alpha$

$x:\exists \alpha .\alpha \equiv$ “for some type $\tau$, $x$ has type $\tau$“

Every typeable term has type $\exists \alpha .\alpha$. This tells us nothing useful.

Question

But what if we combine existentials with record types?

Type Nat = $\exists \alpha .\{z:\alpha ,s:\alpha \to \alpha ,n:\alpha \to int\}$

fun f(x : Nat) = 
let 
	(τ, {z, s, n}) = x
in 
	n(s(s(s z)))
end

Can use $x$ without knowing what $\tau$ is.

Existentials model Abstract Data Types

abstype rat = Rat of int * int
with 
	mkRat, lpus, times, num, denom, gcd
end

Let type RatType = $\exists \alpha .\{\text{mkRat}:int\to int\to \alpha ,\text{plus}:\alpha \to \alpha \to \alpha ,\text{times}:\alpha \to \alpha \to \alpha ,\text{num}:\alpha \to int,\text{denom}:\alpha \to int\}$

val x: RatType = (int * int, {mkRat = _, plus = _, denom= _, gcd = _})
let 
	(τ, {mkRat, plus, minus, num, denom}) = x
	fun equal (x : τ, y : z) = num x *denom y = num y *denom  x
in 
	equal (mkRat 12, mkRat 24)
end

Can be encoded as universals

$\exists \alpha .z\forall \beta .(\forall \alpha .\tau \to \beta )\to \beta$

Let $x$ be as before

Encode $x$ as

$$\begin{array}{rl}\Lambda \beta .\lambda f:& \forall \alpha .\{\text{mkRat}:int\to int\to \alpha ,\text{plus}:\alpha \to \alpha \to \alpha ,\dots \}\to \beta \\ & .f\{int\ast int\}\{\text{mkRat},\text{plus},\text{times},\text{num},\text{denom}\}\end{array}$$

Lecture 13

Lazy Evaluation

Arguments are substituted before they are evaluated. Potential inefficiency, argument used more than once $⟹$ evaluated more than once.

$$\begin{array}{rl}& (\lambda x.xx)((\lambda y.y)z){\to }_{\beta }^{AOR}(\lambda x.xx)z{\to }_{\beta }^{AOR}zz\\ & {\to }_{\beta }^{NOR}((\lambda y.y)z)(\lambda y.y)z)\\ & {\to }_{\beta }^{NOR}z((\lambda y.y)z)\\ & {\to }_{\beta }^{NOR}zz\end{array}$$

Scheme & ML - eager

Lazy evaluation in scheme (delay and force)

(delay <expr>) : <expr> is not evaluated. Returns a promise, suspended computation.

(force <promise>) : returns value computed by the suspended computation. Result is cached once it is forced. Subsequent force s just return the cached. This avoids NOR inefficiency, but side effects only happen once.

Or there is thunking, a body of abstraction is not evaluated, and we delay computation by wrapping it in an abstraction.

(define lazy-add (lambda x y)
	(lambda () (+ x y )))
 
(define x (lazy-add 3 4))
(x) (* addition occurs here)
=> 7

Lazy Data Structures

Lazy evaluation $⟹$ can have infinite data structures.

Infinite lists - streams

(define ones (cons 1 (lambda () ones)))
(defnie s-car car)
(define (s-cdr x) ((cdr x)))

(define make-seq (lambda (start)
	(letrec 
		((next (lambda (n)
			(cons n 
				(lambda () (next (+ n 1)))))))
		(next start))))
(define seq (make-seq 0))
(s-car seq) => 0
(s-car (s-cdr seq)) => 1
(s-car (s-cdr (s-cdr seq))) => 2

A Lazy Language: Haskell

Statically typed, pure functional, lazy evaluation.

Lexicographic rules: Case-sensitive, variables start with lowercase letters, types and constructors start with uppercase letters.

Offside rule:

1. Definitions all begin in the same column
2. Multi-line definitions (lines after the 1st) are indented.

add: Int -> Int -> Int
add = \ x -> \ y -> x + y

Types: Primitive: Int, Float, Char, Bool

Constructed:

• Int -> Bool (functions)
• [Int] (lists)
• (Float, Char) (tuples)

Polymorphism:

• id:: a-> a (pattern-matching, like ML)
• id x = x

Name-binding

sumSquares :: Int -> Int -> Int
sumSquares a b = 
	let 
		square x = 
			square x * x
	in
		square a + square b

OR

sumSquares :: Int -> Int -> Int
sumSquares a b = 
	square a + square b 
	where
	square x = x * x

Booleans: True, False, &&, ||, not

https://people.willamette.edu/~fruehr/haskell/evolution.html

3 ways to write factorial.

Pattern-match:

fact :: Int -> Int
fact 0 = 1
fact n = n * fact(n-1)

If-then-else:

fact:: Int -> Int
fact n = if n == 0 then 1
	else n * fact(n-1)

Guards:

fact:: Int -> Int
fact n
	n == 0 = 1
	otherwise = n * fact(n-1)

Lists:

• [] empty list
• : “cons”

Maps:

• map::(a -> b) -> [a] -> [b]
• map _ [] = []
• map f (x : xs) = f x : map f xs
• ++ = list concat{:haskell}

List comprehensions

$$\begin{array}{rl}& [x\ast x\mid x\underset{\in }{\underbrace{\leftarrow }}[1,2,3,4],x/=2]\\ & =[1,9,16]\end{array}$$ $$\begin{array}{rl}& [x\ast x+y\ast y\mid x\leftarrow [1,2,3],y\leftarrow [2,3,4]]\\ & =[5,10,17,8,13,20,13,18,25]\end{array}$$

qsort[] = []
qsort(x : xs) = 
	qsort[y | y <- xs, y < x]
	++ x : qsort[y | y <- xs, y >= x]

Type declarations:

Type - creates synonyms (like ML)

type String = [Char]

Data $\equiv$ datatype in ML

data Tree a = Empty | Node(a, Tree a , Tree a)

OR

data Tree a = Empty | Node a (Tree a) (Tree a)

Inorder:

• inorder:: Tree a -> [a]
• inorder Empty = []
• inorder (Node(a,b,c)) = inorder b ++ [a] ++ inorder c

Lazy Evaluation

Arguments to functions not evaluated until they are used. Arguments used more than once, result is cached (“call by need”).

Data structures realized only as much as needed for computation to proceed.

$\therefore$ can express algorithms as operations on large data structures.

Compute $1^2+2^2+\cdots +n^2$

Solution:

sum [] = 0
sum(x: xs) = x + sum xs

sumSquares:: Int -> Int
sumSquare n = sum(map sq [1..n])

sumSquare 4 = sum(map sq [1..4])
	= sum(map sq 1:[2..4])
	= sum(sq 1 : map sq[2..4])
	= sq1 + sum(map sq [2..4])
	= 1 + sum(map sq[2..4])
	= 1 + sum(map sq 2 : [3..4])
	= 1 + sum(sq 2 : map sq[3..4])
	= 1 + (sq2 + sum(map sq[3..4]))
	= 1 + (4 + sum(map sq[3..4]))
	= 1 + (4 + (9 + (16 + 0)))
	= 30

Notice: Entire list if never constructed, $\therefore$ no additional space overhead.

Extra unresolved computation due to not being tail recursive.

fact:: Int -> Int
fact n = fact' n 1
	where 
		fact' 0 a = a
		fact' n a = fact' (n-1) (n*a)

fact 5 = fact' 5 1
	= fact' (5 - 1) (5 * 1)
	= fact' 4 (5 * 1)
	= fact' (4-1) (4 * (5 * 1))
	= fact' 3 (4 * (5 * 1))
	= fact' (3-1) (3 * (4 * (5 * 1)))
	= fact' 2 (3 * (4 * (5 * 1)))

Suspended computation grows, tail recursive doesn’t help with lazy code. $\therefore$ this is not constant space.