Abstract
The lecture began with an overview of data types in programming languages: arrays in Fortran,records in Cobol, disjoint unions in Algol 68, references and pointers in Algol W, as well as the universal types of S-expressions in Lisp and terms in Prolog. Algebraic types, introduced in the HOPE language and popularized by ML and Haskell, unify all these notions. Algebraic types are recursive, named sums of products. They can express many computer data structures, as well as conjunction and disjunction in a Curry-Howard approach.
The lambda-calculi studied in previous lectures do not provide data types, as they can be defined in terms of functions, generalizing the clever functional encoding of integers introduced by Church. This encoding is well typed in the F and Fω systems, but with restrictions on the case analyses that can be performed on the data. Thus, we can't prove 0 ≠ 1 with Church's typed encoding !
