Monday, February 8, Volen 101, 3-5 p.m.
(This meeting continues a fortnightly research seminar at Brandeis on programming language theory and implementation. It is being run jointly with the Church group at Boston University---on alternate weeks we meet at BU.)
Intersection types form a type discipline where in declaring a datum x to be of type a/\b, we may assume that certain occurrences of x have type a, and that other occurrences of x have type b. This kind of polymorphic type is useful in programming---for example, in implementing an abstract data type (e.g., a stack) over various kinds of base types (stacks of integers, strings, etc.). Rank-bounded intersection types play a key role in the Church functional programming language, currently being implemented at Boston University; the idea is basically to bound how deeply nested the /\ can appear in type expressions.
We analyze two problems concerning the rank k-bounded intersection type system for the lambda calculus, the functional programmer's tabula rasa:
Typability: Given an untyped lambda term of length n, how hard is it to determine whether the term has a type?
Expressiveness: Given the type erasures of two typable lambda terms of length n, do they have the same normal form? (This is a simple form of detecting program equivalence.)
Let f(0,n)=n and f(k+1,n)=2^{f(k,n)}; we prove that the first problem is DTIME[f(k-1,n)]-hard and that the second problem is DTIME[f(f(k,n)-1,2)]-hard. (Note that f(4,2) is about 10^{19,500}, thus f(f(4,2)-1,2) is a stack of 2s about 10^{19,500} high.) These bounds can be made slightly sharper.
Both of the above results are ``old proofs of new theorems''---they modify known proof techniques for bounds on type inference for the polymorphic type system F-omega proved by Henglein and Mairson, and an expressibility result, due to Rick Statman, for the simply-typed lambda calculus.
What becomes very clear in this analysis is how these two results are intimately related. In particular, the key unifying idea is the construction of large polymorphic iterators. We can give identical examples of this relationship for other well-known type systems, such as simple types and ML types, but fails for System F and its generalizations. The correspondence gives rise to a conjecture concerning the essential relationship between deciding typability and language expressibility.