Lambda Calculus 🧮

These are notes taken from Adam Jones introduction of Lambda Calculus

Intro to Lambda Calculus

Write an identity function that takes a 3

(\x -> x) 3

take x → return x

(\odd -> odd) 3

Literal = 3 Variable = Odd Abstraction/ Function Definition = ( \odd → odd) Application = (\odd → odd) 3

Parts of Expression

(\x -> (\y ->x)) 1 2
(\y -> 1) 2
(2 -> 1)
1

Exercise

(\odd -> odd 3)(\x -> equals (mod x 2 ) 1)
(\x -> equals (mod x 2) 1) 3
equals (mod 3 2) 1
equals 1 1
True

Step 1: Original Expression

$$(\lambda x.\lambda y.xy)(\lambda z.z)$$

Step 2: Apply the function to the argument

$$\lambda y.(\lambda z.z)y$$

Step 3: Simplify the inner expression

$$\lambda y.y$$

Final Simplified Expression

$$\lambda y.y$$

Grammar of the Lambda Calculus

e = x        --variable
  | e_1 e_2  --application
  | \x -> e  --abstraction

Free and Bound Variables in Lambda Calculus

1. Function abstraction binds variables
2. Variables that arenot bounds are considered free or unbound

(\x -> x) 3

x = bound by function abstraction 3 = unbounded

(\x -> (\z -> y)) h

y = unbounded h = unbounded

Free Variables Solutions

$FV(x)=\{x\}$ [variable] $FV(e_1{e}_2)=FV(e_1)\cup FV(e_2)$ [function application] $$\begin{gathered} FV( \\ x\to e)=FV(e)-\{x\} \end{gathered}$$ [function abstraction ]

---

$$\begin{gathered} FV(( \\ z\to z)y)=FV( \\ z\to z)\cup FV(y) \end{gathered}$$ $$\begin{gathered} FV( \\ z\to z)=FV(z)-\{x\} \end{gathered}$$ $FV(y)=\{y\}$ $FV(z)=\{z\}$

$$\begin{gathered} FV( \\ z\to z)=\{x\}-\{x\} \end{gathered}$$ $$\begin{gathered} FV(( \\ z\to z)y)=\{\}\cup \{y\} \end{gathered}$$ $$\begin{gathered} FV(( \\ z\to z)y)=\{y\} \end{gathered}$$

The free variables is only $y$

Let Expressions in Lambda Calculus

let x = 3 in odd x
(\x -> odd x) 3

Let Expressions and Polymorphism

let x = (\x -> x)
  in x (odd (x 3))

e = x        --variable
  | e_1 e_2  --application
  | \x -> e  --abstraction
  | let x = e_1 in e_2 --let

Type Inference

Example	Type
3	Int
True	Bool
odd	function from Int to Bool
odd 3	Bool
odd True	not well-typed
\x → x	function, which for an $\alpha$ , is from $\alpha$ to $\alpha$

Types in Hindley-Milner

A type system for the lambda calculus with let statements

1. Type Variables
   1. $\alpha$
   2. $\beta$
2. Type Function Applications
   1. List Bool
   2. Int → Bool
   3. Bool
   4. $\alpha \to \alpha$
   5. List $\alpha$

Monotypes in Hindley-Milner

$$\begin{array}{r}\tau =\alpha [variable]\\ |C{\tau }_1\dots {\tau }_n[application]\end{array}$$

where $C$ is the set of type functions, which must contain → For example $C$= → , Int, Bool, List, Map, 2-Tuple, 3-Tuple

For-all Quantifiers

$\forall \alpha .\alpha \to \alpha$

<T>(arg: T): T

T = TypeVar('T')
Callable[[T],T]

$\forall \alpha .\alpha \to \alpha$ $\beta \to \beta$

id (odd (id 3))

Hindley-Milner Types Syntax

$$\begin{array}{r}\tau =\alpha [variable]\\ |C{\tau }_1\dots {\tau }_n[application]\end{array}$$ $$\begin{array}{r}\sigma =\tau [monotype]\\ |\forall \alpha .\sigma [quantifier]\end{array}$$

Assignments, Contexts, Typing Judgement and Rules in Type Systems

Expression : Type Assignment = $e:\sigma$ Age : Int

age :: Int

context = $\Gamma$ → a list of assignments $\Gamma =$ $\text{age}:\text{Int},$ $\text{odd}:\text{Int}\to \text{Bool}$

age is an integer contained in the context $\text{age}:\text{Int}\in \Gamma$

$\Gamma =\text{(empty)}$ $|\Gamma ,e:\sigma$

Typing Judgements

when an assignment follows given the context, we can make a typing judgement

$\Gamma ⊢e:\sigma$

From the context gamma, the expression e has type $\sigma$

Context	Judgements
$\Gamma =$ $\text{age}:\text{Int},$ $\text{odd}:\text{Int}\to \text{Bool}$	$\Gamma ⊢\text{age}:\text{Int}$ $\Gamma ⊢\text{odd age}:\text{Bool}$
Premise ⇒ Conclusion (judgement)
$x:\sigma \in \Gamma$ ⇒ $\Gamma ⊢x:\sigma$

Free and Bound Type Variables in Type Systems

Free Variables in Types

$FV(\alpha )=\{\alpha \}$ [var] $FV(C{\tau }_1\cdots {\tau }_n)=FV({\tau }_1)\cup \cdots \cup FV({\tau }_n)$ [app] $FV(\forall \alpha .\sigma )=FV(\sigma )-\{\alpha \}$ [quantifier]

Free Variables in Contexts

$FV((\text{empty}))=\{\}$ $FV(\Gamma ,e:\sigma )=FV(\Gamma )\cup FV(\sigma )$

Exercise 1

What are the free variables in this type ? $\forall \beta .\text{List}(\beta \to (\gamma \to \beta ))$

Use rules $FV(\forall \beta .\text{List}(\beta \to (\gamma \to \beta )))$ $=FV(\text{List}(\beta \to (\gamma \to \beta )))-\{\beta \}$ by quantifier: $\sigma =\text{List}(\beta \to (\gamma \to \beta )),\alpha =\beta$ $=FV(\beta \to (\gamma \to \beta ))-\{\beta \}$ by app: $C=\text{List},{\tau }_1=\beta \to (\gamma \to \beta )$ $=(FV(\beta )\cup FV(\gamma \to \beta ))-\{\beta \}$ by app: $C=\to ,{\tau }_1=\beta ,{\tau }_2=\gamma \to \beta$ $=(FV(\beta )\cup FV(\gamma )\cup FV(\beta ))-\{\beta \}$ $=(\{\beta \}\cup \{\gamma \}\cup \{\beta \})-\{\beta \}$ $=\{\beta ,\gamma \}-\{\beta \}$ $=\{\gamma \}$

Substitutions in Logic

 A map from variables to terms

$S=\{h\mapsto j,o\mapsto y\}$ $S(\text{hello})=\text{jelly}$

Applying Substitutions to Type Systems

$S=\{\alpha \mapsto \text{Int}\}$ $S(\alpha \to \text{Bool})=\text{Int}\to \text{Bool}$

$S=\{\alpha \mapsto \beta ,\beta \mapsto \text{Int}\}$ $S(\alpha \to \beta )=\beta \to \text{Int}$ $S(S(\alpha \to \beta ))=\text{Int}\to \text{Int}$

Combining Substitutions in Logic

$S_1=\{\alpha \mapsto \gamma ,\beta \mapsto \delta \}$ $S_2=\{\alpha \mapsto \beta \}$ $\text{combine}(S_1,S_2)(thing)=S_1(S_2(thing))$ $\text{combine}(S_1,S_2)=\{\alpha \mapsto \delta ,\beta \mapsto \delta \}$

Unifying Substitutions and the Unification Process

A substitution unifies two values if when applied to both it results in equal results

$S=\{r\mapsto y,s\mapsto y,d\mapsto s\}$ $a=\text{red},b=\text{yes}$ $S(\text{red})\ne S(\text{yes})$ → S is a not a unifying substitution

---

$a=3,b=y$ $S=\{y\mapsto 3\}$ $S(a)=S(b)=3$ → S is a unifying substitution

---

$a=3\ast 7$ $b=3+z$ There is no unifying substitution as they are of different structure.

---

$a=1+z$ $b=z$ $S=\{z\mapsto 1+1+1+\cdots \}$ $S(a)=S(b)=1+1+1+\cdots$

Algorithm Signature

$S=\text{unify}(a,b)$ $S(a)=S(b)$ A unifying S may not exist at all, or may not be finite.

Applying Unification to Type Systems

$a=\text{Int}\mapsto \alpha$ $b=\beta \mapsto \text{Bool}$ $S=\{\alpha \mapsto \text{Bool},\beta \mapsto \text{Int}\}$ $S(a)=S(b)=\text{Int}\mapsto \text{Bool}$

$a=\text{List}\alpha$ $b=\beta \mapsto \text{Bool}$ No unifying substitution exists

---

$a=\alpha \mapsto \text{Int}$ $b=\alpha$ $S=\{\alpha \mapsto \text{Int}\to \text{Int}\to \cdots \to \text{Int}\}$ $S(a)=S(b)=\text{Int}\to \cdots \to \text{Int}\to \text{Int}$

Unification can 'merge' types while preserving all type constrainsts

Unification Algorithm for Hindley-Milner Types

The Algorithm

unify(a: MonoType, b: MonoType) → Substitution: if a is a type variable: if b is the same type variable: return {} if b contains a: throw error “occurs check failed, cannot create infinite type” returns {$a\mapsto b$} if b is a type variable: return unify(b,a) if a and b are both type function applications: if a and b have different type functions: throw error “failed to unify, different type functions” let S = {} for i in range(number of type function arguments): S = combine(S,unify(S(a.arguments[i]),S(b.arguments[i]))) return S

function unify(a: MonoType, b: MonoType): Substitution {
    if (a instanceof TypeVar) {
        if (b instanceof TypeVar && a.name == b.name)
            return {};
        if (contains(b, a))
            throw new TypeInferenceError('occurs check failed,' +
                ' cannot create infinite type');
        return { [a.name]: b }
    }
 
    if (b instanceof TypeVar)
        return unify(b, a);
 
    if (a instanceof TypeFuncApp && b instanceof TypeFuncApp) {
        if (a.constructorName !== b.constructorName)
            throw new TypeInferenceError('failed to unify,' +
                ' different type functions');
        let S: Substitution = {};
        for (let i = 0; i < a.args.length; i++) {
            S = combine(S, unify(apply(S, a.args[i]), apply(S, b.args[i])));
        }
        return S;
    }
}

Type Order and the $⊑$ Relation in Hindley-Milner

More General
$\forall \alpha .\forall \beta .\alpha \to \beta$
$\forall \alpha .\alpha \to \text{Bool}$
$\text{Int}\to \text{Bool}$
Less General

Type on left is more general than type on right $\forall \alpha .\forall \beta .\alpha \to \beta .⊑\text{Int}\to \text{Bool}$

Syntax for Type Order

$\sigma ⊑\sigma$ $\forall \alpha .\alpha ⊏\text{Int}$

Formal Definition

${\sigma }_1$ is more general than ${\sigma }_2$ if there is a substitution $S$ that maps the for-all quantified variables in ${\sigma }_1$, and $S({\sigma }_1)={\sigma }_2$

Instantiation in Type Systems and Hindley-Milner

find typs that are less generals

$\forall \alpha .\forall \beta .\alpha \to \beta$ ⇒ $\text{Int}\to \text{List}\gamma$ with $S=\{\beta \mapsto \text{List}\gamma ,\alpha \mapsto \text{Int}\}$

If ${\sigma }_1⊑{\sigma }_2$, an expression of type ${\sigma }_2$ can be used where one of type ${\sigma }_1$ is needed.

Generalisation of Types in Hindley-Milner

Add for all quantifier into a free type variable in a type

$\forall \beta .\alpha \to \beta$ $\downarrow$ $FV(\forall \beta .\alpha \to \beta )=\alpha$ $\downarrow$ $\forall \alpha .\forall \beta .\alpha \to \beta$

Can only generalise a type when the type variable is not free in the context

generalise$(\Gamma ,\sigma )$ returns the most generalised version of the type $\sigma$

Intro to Hindley-Milner Typing Rules

Variable Typing Rule

$\frac{x:\sigma \in \Gamma }{\Gamma ⊢x:\sigma }$

1. If “the variable '$x$' has type of polytype '$\sigma$'” is in context $\Gamma$
2. then from the context '$\Gamma$' it follows that “the variable '$x$' has type of polytype '$\sigma$'”

$\Gamma =$ $\text{age}:\text{Int},$ $\text{odd}:\text{Int}\to \text{Bool}$

Q: what is the type of age given the context of '$\Gamma$'? $\Gamma ⊢\text{age}:???$ $x=\text{age},\sigma =\text{Int}$ $\frac{\text{age}:\text{Int}\in \Gamma }{\Gamma ⊢\text{age}:\text{Int}}$ A: Int

Application Typing Rule

$\frac{\text{premise}}{\text{conclusion}}$ $\frac{\Gamma ⊢e_0:{\tau }_a\to {\tau }_b\Gamma ⊢e_1:{\tau }_a}{\Gamma ⊢e_0{e}_1:{\tau }_b}$

1. If $e_0$ is of type ${\tau }_a\to {\tau }_b$ and $e_1$ is of type ${\tau }_a$

2. $e_0$ applied to $e_1$ is type ${\tau }_b$

3. If premise

4. Then conclusion

$\Gamma =$ $\text{age}:\text{Int},$ $\text{odd}:\text{Int}\to \text{Bool}$ $\Gamma ⊢\text{odd age}:\text{Bool}$ ← inference

$\frac{\frac{\text{odd}:\text{Int}\to \text{Bool}\in \Gamma }{\Gamma ⊢\text{odd}:\text{Int}\to \text{Bool}}\text{[var]}\frac{\text{age}:\text{Int}\in \Gamma }{\Gamma ⊢\text{age}:\text{Int}}\text{[var]}}{\Gamma ⊢\text{odd age}:\text{Bool}}\text{[app]}$

Conclusion $[\text{rule}]$ (premise)

1. $\Gamma ⊢\text{odd}:\text{Int}\to \text{Bool}[\text{var}](\text{odd}:\text{Int}\to \text{Bool}\in \Gamma )$
2. $\Gamma ⊢\text{age}:\text{Int}[\text{var}](\text{age}:\text{Int}\in \Gamma )$
3. $\Gamma ⊢\text{odd age}:\text{Bool}[\text{app}](1,2)$

Unifying Constraints with Typing Rules

$$\frac{\frac{\text{odd}:t4\in \Gamma }{\Gamma ⊢\text{odd}:t1\to t2}\frac{\text{age}:t5\in \Gamma }{\Gamma ⊢\text{age}:t3}}{\Gamma ⊢\text{odd age}:t0}$$

• t0 ~ t2
• t1 ~ t3
• t1 → t2 ~ t4
• t4 ~ Int → Bool
• t3 ~ t5
• t5 ~ Int

Finding Type Errors with Typing Rules

$$\frac{\frac{\text{odd}:t4\in \Gamma }{\Gamma ⊢\text{odd}:t1\to t2}\frac{\text{hungry}:t5\in \Gamma }{\Gamma ⊢\text{hungry}:t3}}{\Gamma ⊢\text{odd hungry}:t0}$$

• t0 ~ t2
• t1 ~ t3
• t1 → t2 ~ t4
• t4 ~ Int → Bool
• t3 ~ t5
• t5 ~ Bool

---

$\Gamma ⊢\text{odd hungry}:t0$

1. $\text{unify}(t0,t2)=\{t0)\mapsto t2\}$ $\Gamma ⊢\text{odd hungry}:t2$
2. $\text{unify}(t1,t3)=\{t1)\mapsto t3\}$ t3 → t2 ~ t4 t4 ~ Int → Bool t3 ~ t5 t5 ~ Bool
3. $\text{unify}(t3\to t2,t4)=\{t4)\mapsto t3\to t2\}$ t3 → t2 ~ Int → Bool
4. $\text{unify}(t3\to t2,\text{Int}\to \text{Bool})=\{t3\mapsto \text{Int},t2\mapsto \text{Bool}\}$ $\Gamma ⊢\text{odd hungry}:\text{Bool}$ Int ~ t5 t5 ~ Bool 5)$\text{unify}(\text{Int},t5)=\{t5\mapsto \text{Int}\}$ Int ~ Bool ⇒ Type Error

Function Abstraction Typing Rule

$\frac{\Gamma ,x:{\tau }_a⊢e:{\tau }_b}{\Gamma ⊢\backslash x\to e:{\tau }_a\to {\tau }_b}$ $\frac{\text{premise}}{\text{conclusion}}$ If from the context '$\Gamma$' plus the assignment “variable ‘x’ has type '${\tau }_a$'” if follows that expression ‘e’ has type '${\tau }_b$'

then from the context '$\Gamma$' it follows that the expression '$\backslash x\to e$' has type '${\tau }_a\to {\tau }_b$'

The function parameters get replaced by the types

$\Gamma =$ $\text{gt: Int}\to \text{(Int}\to \text{Bool)}$

Q: What is the type of ’$\backslash n\to \text{gt 3 n}$ given the context '$\Gamma$' ?

$x=n$ $\text{e = gt 3 n}$ ${\tau }_a=\text{Int}$ ${\tau }_b=\text{Bool}$

$\Gamma ⊢\backslash n\to \text{gt 3 n: ???}$

$$\frac{\Gamma ,n:\text{Int}⊢\text{gt}3n:\text{Bool}}{\Gamma ⊢\backslash n\to \text{gt}3n:\text{Int}\to \text{Bool}}$$

Reading the Rule

The whole rule is saying:

1. Premise: If, in a context where n has type Int, the expression \text{gt}\ 3\ n has type Bool…
2. Conclusion: …then the function \n \rightarrow \text{gt}\ 3\ n has the type \text{Int} \rightarrow \text{Bool}, i.e., it is a function that takes an integer and returns a boolean.

$$\text{Practical Example:}$$ $$\Gamma =\text{gt}:\text{Int}\to (\text{Int}\to \text{Bool})$$ $$\begin{array}{rl}1.& \Gamma ,n:\text{Int}⊢n:\text{Int}[\text{var}](n:\text{Int}\in \Gamma ,n:\text{Int})\\ 2.& \Gamma ,n:\text{Int}⊢\text{gt}:\text{Int}\to (\text{Int}\to \text{Bool})[\text{var}](\text{gt}:\text{Int}\to (\text{Int}\to \text{Bool})\in \Gamma ,n:\text{Int})\\ 3.& ⊢3:\text{Int}[\text{literal}]\\ 4.& \Gamma ,n:\text{Int}⊢\text{gt}3:\text{Int}\to \text{Bool}[\text{app}](2,3)\\ 5.& \Gamma ,n:\text{Int}⊢\text{gt}3n:\text{Bool}[\text{app}](1,4)\\ 6.& \Gamma ⊢\backslash n\to \text{gt}3n:\text{Int}\to \text{Bool}[\text{abs}](5)\end{array}$$

Let Typing Rule

$$\frac{\Gamma ⊢e_0:\sigma \Gamma ,x:\sigma ⊢e_1:\tau }{\Gamma ⊢\text{let}x=e_0\text{in}{e}_1:\tau }$$

If we bind an expression $e_0$ to a variable x with type $\sigma$ and doing so results in the let body $e_1$ having type $\tau$

then the let statement as a whole has type $\tau$

$\Gamma$ = gt : Int → (Int → Bool)

$\Gamma ⊢$ let a = 2 in gt 3 a : Bool

$e_0$ = 2 $e_1$ = gt 3 a x = a $\sigma$ = Int $\tau$ = Bool

$\frac{\Gamma ⊢2:\text{Int}\Gamma ,\text{a}:\text{Int}⊢\text{gt 3 a}:\text{Bool}}{\Gamma ⊢\text{let a = 2 in gt 3 a : Bool}}$

Instantiation Typing Rule

If ${\sigma }_1⊑{\sigma }_2$, an expression of type ${\sigma }_2$ can be used where one of type ${\sigma }_1$ is needed.

$\frac{\Gamma ⊢e:{\sigma }_a{\sigma }_a⊑{\sigma }_b}{\Gamma ⊢e:{\sigma }_b}$ If from $\Gamma$ it follows that $e$ has type ${\sigma }_a$ and ${\sigma }_a$ is more general than ${\sigma }_b$, then from the context it follows that $e$ has type ${\sigma }_b$

$\Gamma =$ reverse: $\forall \alpha .$ $\text{List}\alpha \to \text{List}\alpha ,$ ages: $\text{List Int}$

What is the type of ‘reverse ages’ given the context ? $\Gamma ⊢\text{reverse ages}:\text{List Int}$

Generalization Typing Rule

$\frac{\Gamma ⊢e:\sigma \alpha \notin FV(\Gamma )}{\Gamma ⊢e:\forall \alpha .\sigma }$

If e has type $\sigma$ and type variable $\alpha$ is not free in the context

then for-all quantify e’s type $\sigma$ with variable $\alpha$