Today’s lambda calculus

why static typing?

• find type errors when the program is written
• …which makes guarantees for all possible executions
• …which can leads to a faster execution because you don’t have to do runtime type checks (this is actually non-trivial!)

why (not) static typing

• you can detect type errors during execution—so it can be sound as well
• this is not untyped: you can still have types (untyped is raw bits)

implementation

every value has a “tag” — for instance, integers vs. functions

more Combinator Calculus and confluence

Lambda Calculus

Like SKI Calculus, its a language of functions; unlike SKI Calculus, there are variables.

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

meaning, we have:

• a variable \(x\)
• an abstraction \(\lambda x . e\) (a function definition)
• an application \(e_1 e_2\)

we call \((\lambda x . e)e’\) (a function and its argument, ready for reduction) a redex.

abstraction

def f(x) = e

can be written as:

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

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: