Lecture 3: Types and Functions.

In this lecture we motivate the advantages of a typing discipline. In essence, types summarize and approximate the meaning of a program or better the invariant it represents.

A compiler for a functional programming language such as Haskell or SML, in general, attempts to infer a type for the function currently compiled. In the case of failure, there are two possible causes. Either to little type information is known a priori which causes the type inference algorithm to give up, or a type could not be assigned because the algorithm fails to assign a unique type to some subterm.

With the concept of types at hand, we continue in this lecture to extend values, programs, evaluation and typing by rules that are concerned with functions, variables, abstraction, and application.

Suggested Reading Materials:

Previous lecture: Lecture 2
Next lecture: Lecture 4