Tech Report CS-94-25

An Analysis of the Core-ML Language: Expressive Power and Type Reconstruction

Paris C. Kanellakis, Gerd G. Hillebrand, and Harry G. Mairson

May 1994

Abstract:

Core-ML is a basic subset of most functional programming languages. It consists of the simply typed (or monomorphic) $\lambda$-calculus, simply typed equality over atomic constants, and {\tt let} as the only polymorphic construct. We present a synthesis of recent results which characterize this ``toy'' language's expressive power as well as its type reconstruction (or type inference) problem. More specifically: (1)~Core-ML can express exactly the ELEMENTARY queries, where a program input is a database encoded as a $\lambda$-term and a query program is a $\lambda$-term whose application to the input normalizes to the output database. In addition, it is possible to express all the PTIME queries so that this normalization process is polynomial in the input size. (2)~The polymorphism of {\tt let} can be explained using a simple algorithmic reduction to monomorphism, and provides flexibility, without affecting expressibility. Algorithms for type reconstruction offer the additional convenience of static typing without type declarations. Given polymorphism, the price of this convenience is an increase in complexity from linear-time in the size of the program typed (without {\tt let}) to completeness in exponential-time (with {\tt let}). (3)~Fragments of Core-ML, based on the order of functionalities used, can be fairly expressive. For example, order $\leq 5$ suffices for the PTIME queries, even without {\tt let} or equality. Also, for each fixed order, type reconstruction is polynomial in program size. Programming by using low order functionalities and type reconstruction is common in functional languages. Thus, our analysis partly explains the wide use and efficiency of such programming practices.

(complete text in pdf or gzipped postscript)