|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
 ABSTRACT
The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central construct, and type matching is therefore a principal program correctness check. In practice, however, assigning a type to each and every expression in a functional program can be prohibitively cumbersome. As expressions are compounded, the task of assigning a type to each expression and subexpression becomes practically impossible, even more so because the type-expressions themselves grow longer. It becomes imperative therefore to design friendly programming environments that permit the user type-free programming, but that generate fully typed programs in which the types of all expressions are inferred by the system from the program. For interactive functional programming environments of the kind implemented for the Edinburgh functional programming language ML, a type-inference system is an invaluable tool for on-line parse-time error detection and debugging. The issue of type inference leads naturally to type-schemes. If all one has of a functional program is a definition statement such as f(x)=3, then all one can say of the type of f is that it must be of the form ’Ѩint, i.e. --- an instance of the type scheme t ¨ int, where t is a type variable. As more of the program appears, say x(true)=z, t may be restricted, to bool¨s. We are therefore interested in type-schemes, using type parameters (free type variables). All one needs then to obtain a rudimentary form of generic procedures is a device for type instantiation. This function is fulfilled in ML by the construct let. Other methods are described in Ü4 below. During the process of inferring a type for a given program, one would like at each step to find a most general (so-called principal) type scheme for each subexpression, so that types to be assigned to variables and subexpressions in the sequel may be assumed to be instances of those assigned earlier. The notion of principal type was introduced by Curry and Feys [CF] for Combinatory Logic, and Hindley [Hin] showed that the principal type exists for any Combinatory Logic expression and that it can be found using J.A. Robinson's Unification algorithm [Rob].The seminal paper on type-inference for functional programs is Milner's [Mil], where an algorithm W is defined for inferring a type for any ML program (without recursively defined types). More recently, Damas and Milner [DM] defined a simple formal calculus of type inference, with respect to which W is proved complete. In this paper we study several aspects of type inference for polymorphic type disciplines. First, we deal with type inference for parametric type systems, that is --- type systems that include simple types defied over constant types and type variables. We recast Milner's algorithm W in a general "algebraic" form, which applies to a variety of generic type disciplines (Ü2). In Ü3 we present an alternative algorithm V for type inference, fundamentally different from W, which easily accommodates type coercion and overloading, allows efficient local updates to the user program, and is more efficient than W for implementations that allow concurrency. In Ü4 we briefly describe four polymorphic disciplines: type abstraction, type quantification, type conjunction (intersection) and the ML construct let. In Ü5 type inference for the abstraction and quantification disciplines is discussed. We point out that the two disciplines are combinatorially isomorphic, and we outline a type inference algorithm for them. Ü6 is devoted to type inference for the conjunctive discipline. We mention some limitations to type inference here, in particular --- the fact that the set of typable expressions is not effectively decidable. Moreover, there is no feasible algorithm that would type expressions even when these are given with a quantificational typing. This kind of non-effectiveness motivates our considering a restriction to types where type conjunction is permitted only at low levels of functionality. Here the level of functionality of a function (or procedure) is recursively defined as one plus the greatest level of functionality of its arguments. This gives rise to a hierarchy on polymorphic types, a notion that is equally natural for the type abstraction and type quantification disciplines. We show that our algorithm V (of Ü3) can be naturally extended to the restriction of the conjunctive discipline to types of rank 2 in the hierarchy, and we outline an argument showing that already for a low rank, seemingly 3, type inference is not effectively decidable. In Ü7 we discuss the ML construct let in light of our previous results. We point out that the polymorphic discipline of ML is isomorphic to the restriction to rank 2 of each one of the other disciplines. This gives weight to the particular choice of polymorphism in ML, and to the completeness of Milner's algorithm W for that choice. At the same time, the equivalence suggests more flexible representations of this discipline (namely --- either the conjunctive or the quantificational disciplines restricted to rank 2) in which the anomaly in ML, of legal expressions with well-formed illegal subexpressions, is avoided. REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage Privacy Policy Code of Ethics Contact Us Useful downloads:  Adobe Acrobat
 QuickTime
 Windows Media Player
 Real Player
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Pdf