Lambda Calculus, typing

hyperstrict

aggressively reduce everything

call-by-value

we recursively evaluate the argument before reducing the function application

implementing lambda calculus

we can implement Lambda Calculus through abstracting it into SKI Calculus:

observe that \(\lambda x.e \implies A(E, x)\); for each expression \(e\), we replace the innermost lambda expression \(\lambda x.e’\) in \(e\) by \(A(e’, x)\).

simply typed Lambda Calculus

Recall normal lambda calculus:

\begin{equation} e \to x | \lambda x.e | e e \end{equation}

more on types

Remember: when we say \(e: t\), this means that as we evaluate \(e\), after all reductions we will get a thing of type \(t\).

type checking

1. start at the leaves, integers and variables
2. for each one above, match the expression to the type rules

a* type inference

1. for every distinct lambda variable, we name a new type
2. then, for function applications, we have then also substitute the output type of the function with a type variable

then, to saturating the constraint, we solve them using:

Lambda Calculus, review

Grammar:

\begin{equation} e \to (x | \lambda x.e | e e) \end{equation}

and beta reductions:

\begin{equation} (\lambda x . e_1) e_2 \to e_1 [x := e_2] \end{equation}

structural operational semantics

“why can’t we have logical rules to explain how programs execute?”

bold

type judgment

\begin{equation} A \vdash e :t \end{equation}

“under environment \(A\) for the free variables of \(e\), the entirety of \(e\) has type \(t\)”

value judgment

\begin{equation} E \vdash e \to v \end{equation}

Lambda calculus, now with sums:

\begin{equation} e \to (x | \lambda \lambda x.e | e e | i | e+e) \end{equation}

explicit evaluation order

write \(e + e’\) as….

\(( \lambda x . ((\lambda y . (\lambda z.z) (x + y)) e’)) e\)

in a call by value world, this would explicitly specify the order that we add \(x\) and \(y\) together.

Notice! We can also write this with let notation:

pairs

• Constructor: \(\qty(e,e’)\)
• Destructor: \(p.l, p.r\) or \(fst\ p\), \(snd\ p\)
• Type: \(A * B\)

currying

Consider a function from pairs to a thing: \(A * B \to C\)

We can instead construct a function: \(A \to B \to C: \lambda a . \lambda b. f(a,b)\)

state and exception

Both state and exceptions create “side information”—-the side information is threaded through computation in a specific order; we create new primitives for manipulating side information.