Fundamenta Informaticae

In programming languages that feature unrestricted recursion, the equational theory corresponding to evaluation of data type expressions must be distinguished from the classical theory of the data as given by, say, algebraic specifications. Aiming to preserve classical reasoning about the underlying data types, that is, for the equational theory of the programming language to be a conservative extension of the theory given by the data type specification, we investigate, alternative computational settings given by typed lambda calculi, specifically here by the Girard-Reynolds polymorphic lambda calculus ( λ ∀ ). We prove that the addition of just the λ ∀ -constructions to arbitrary specifications, as given by algebraic theories, and even simply typed lambda theories, is conservative. This suggests that polymorphic constructs and reasoning can be superimposed on familiar data-type definition features of programming languages without changing the behavior of these features.

Using purely syntactic methods, we give transformational proofs of these results for certain systems of equational reasoning. A new technique for analyzing polymorphic equational proofs is developed to this purpose.

Finally, we prove, with a semantics argument, that it is possible to combine arbitrary algebraic data type specifications and the λ ∀ -constructions into functional programming languages that both conserve algebraic reasoning about data. and ensure, over arbitrary algebraically specified observables, a computing power equivalent to that of the pure λ ∀ . The corresponding problem for simply typed specifications remains open.

In this paper we investigate the type inference problem for a large class of type assignment systems for the λ-calculus. This is the problem of determining if a term has a type in a given system. We discuss, in particular, a collection of type assignment systems which correspond to the typed systems of Barendregt’s “cube”. Type dependencies being shown redundant, we focus on the strongest of all, Fω, the type assignment version of the system F ^ω of Girard. In order to manipulate uniformly type inferences we give a syntax directed presentation of Fω and introduce the notions of scheme and of principal type scheme. Making essential use of them, we succeed in reducing the type inference problem for Fω to a restriction of the higher order semi-unification problem and in showing that the conditional type inference problem for Fω is undecidable. Throughout the paper we call attention to open problems and formulate some conjectures.

We study a type system, in the spirit of ML and related languages, with two novel features: a general form of record pattern matching and a provision for user-declared subtypes. Extended pattern matching allows a function on records to be applied to any record that contains a minimum set of fields and permits the additional fields of the record to be manipulated within the body of the function. Together, these two enhancements may be used to support a restricted object-oriented programming style. We define the type system using inference rules, and develop a type inference algorithm. We prove that the algorithm is sound with respect to the typing rules and that it infers a most general typing for every typable expression.

We consider typed λ-calculi with pairing over the algebra W of words over {0, 1}, with a destructor and discriminator function. We show that the poly-time functions are precisely the functions (1) λ-representable using simple types, with abstract input (represented by Church-like terms) and concrete output (represented by algebra terms); (2) λ-representable using simple types, with abstract input and output, but with the input and output representations differing slightly; (3) λ-representable using polymorphic typing with type quantification ranging over multiplicative types only; (4) λ-representable using simple and list types (akin to ML style) with abstract input and output; and (5) λ-representable over the algebra of flat lists (in place of W), using simple types, with abstract input and output.

We prove that partial type reconstruction for the pure polymorphic λ-calculus is undecidable by a reduction from the second-order unification problem, extending a previous result by H.-J. Boehm. We show further that partial type reconstruction remains undecidable even in a very small predicative fragment of the polymorphic λ-calculus, which implies undecidability of partial type reconstruction for λ M L as introduced by Harper, Mitchell, and Moggi.

We consider computability over abstract structures with help of primitive recursive definitions (an appropriate modification of Gödel’s system T). Unlike the standard approach, we do not assume any fixed representation of integers, but instead we allow primitive recursion to be polymorphic, so that iteration is performed with help of counters viewed as objects of an abstract type Int of arbitrary (hidden) implementation. This approach involves the use of existential quantification in types, following the ideas of Mitchell and Plotkin. We show that the halting problem over finite interpretations is primitive recursive for each program involving primitive recursive definitions. Conversely, each primitive recursive set of interpretations is defined by the termination property of some program.