Fixed Points and Extensionality in Typed Functional Programming Languages

We consider the interaction of recursion with extensional data types in several typed functional programming languages based on the simply-typed lambda calculus. Our main results concern the relation between the equational proof systems for reasoning about terms and the operational semantics for evaluating programs. We also present several results about the expressivity of the languages, compared according to both the functions and the data types definable in them. The methods used are those of classical lambda calculus and category theory. The first language discussed is a variant of Scott and Plotkin's PCF, which adds to the simply-typed lambda calculus products, fixed points of functions, and algebraic data types specified by a signature and a set of equations. PCF is able to express all partial computable functions over the given basic types, but the corresponding reduction system is not confluent if we include the usual surjective pairing rule, which expresses the extensionality o..