IFX(ID:1490/ifx001)Hybrid of generic and first class polymorphic data typing approaches Related languages
References: Combining Generic and First-Class Polymorphism Type reconstruction relieves the programmer of the burden of providing type information while retaining the benefits of strongly-typed languages, including superior performance, documentation, and safety. However, present systems for type reconstruction, such as the ML type system [Milner78], do not permit the use of firstclass polymorphic values. Explicitly-typed languages, such as FX-87 [GiffordS?I], do permit first-class polymorphic values, but they do not provide the progrsmmer with the convenience of implicitly-typed languages such as ML. The FX-89 programming language is a revision and extension of FX-87. FX-89 is based on a type reconstruction system that combines the flexibility of ML with the full typing ability of the explicitly typed second order lambda calculus. This reconstruction system will accept ML-style programs, explicitly-typed programs, and programs that use explicit types for all first-class polymorphic values. In thii paper we describe both the theoretical basis of the FX-89 type reconstruction system and our type reconstruction algorithm. The algorithm described in the paper has been implemented. In order to simplify our presentation we will restrict our attention to a simplified version of FX-89 which we will call IFX. The full FX-89 language includes side-effects, modules, oneofs, references, and other data types. These constructs can be added to the type inference system described below. In the remainder of this paper we discuss the previous work in this area (Section 2), introduce IFX (Section 3), present a system of type reconstruction rules (Section 4), describe an algorithm which reconstructs IFX types (Section 5), prove the correctness of the algorithm (Section 6), briefly discuss possible extensions (Section 7), and conclude with some observations on our result (Section 8). Extract: Previous Work Previous Work [Mimer781 presents a typing system based on type schemes in which the let construct provides generic polymorphism. ML, as presented in [Damas82], uses generic type variables to express polymorphism. The ML type discipline is not as powerful as the type discipline of the second-order polymorphic lambda calculus [Fortune83]. Type quantifiers are not explicit in ML, and it is therefore not possible to express the type of a function which expects a polymorphic value as an argument. For thii reason, we say that ML does not provide first-class polymorphism. [McCracken841 introduced a type reconstruction system for the second-order polymorphic lambda calculus. McCracken?s system did not provide the generic let construct of ML, although it did attempt to support the automatic instantiation of explicitly typed polymorphic functions in application position. Both [McCracken84] and [Leivant83] attempted to provide automatic type abstraction in more general type systems, but these results are flawed (see sections 4.5 and 4.6). The general partial polymorphic type inference problem was shown to be undecidable by poehm85]. More recent work [Kfoury88] has shown that conservative extensions to ML providing restricted polymorphism are possible, but has not provided a practical type reconstruction algorithm. Recently, [Pfenning88] related the complexity of the partial type reconstruction problem for the second-order polymorphic lambda calculus to that of second-order unification, which is well-known to be undecidable [Goldfarb81]. We believe our type reconstruction method is the first to combine the implicit typing of ML with the full power of the second-order polymorphic lambda calculus. We accomplish this flexibility by providing both generic and explicitly-quantified polymorphic types, ss well as operators which convert between these two forms of polymorphism. The difficulty of second-order unification is avoided via syntactic restrictions that define the types which may be omitted by the programmer. Below are some examples which illustrate the relative power of the ML typing system, McCracken?s typing system (MTS), and our system (IFX). The let binding construct of ML permits generic type abstraction and instantiation of twice and id: (let ((twice (lambda (f x) (f (f I))) ) (id (lambda (x) x))) (cons (twice id 0) (twice id true))) This example is not well-typed in MTS because no generic polymorphism is provided. This example is welltyped in ML because the variables twice and id are assigned generic types, and these generic types are automatically instantiated as necessary. In general, ML programs cannot be typed by MTS without the addition of extensive explicit type abstraction and instantiation information. The explicit typing of MTS, and the implicit instantiation of the functions cons and f, permit: (lambda (f : Vt.t + t 1 (cons (f 0) (f true))) The second example is not well-typed in ML, because the lambda-bound variable f must have two incompatible types within the body of the lambda. In ML, A lambd+bound variable cannot be given a generic type within the body of the lambda because the type language is not capable of expressing the resulting function type of the lambda, which must contain an explicit type quantifier. First-class polymorphism allows the variable f to be assigned an explicitly quantified polymorphic type. Our system permits both of the above examples. Mcr Cracken introduced the close operator to allow the programmer to indicate where type abstraction should occur without having to specify precisely what those type abstractions should be. A discussion of the formal typing rule for the close operator and why our modification to the rule in pcCracken841 is necessary appears in sections 4.5 and 4.6. Unlike McCracken?s system, our type system contains both ML-style generic types and explicitly quantified types, and we therefore require that the programmer indicate where explicit quantifiers should be removed from a type. The following example illustrates the use of both explicit and generic polymorphism: (lambda (g : Vt.t --+ t) (let ((twice (lambda (f x) (f (f I)))) (g (open g))) (cons (twice g 0) (twice g true)))) The open operator is used to convert an explicitly quantified polymorphic type into an ML-style generic polymorphic type, and close is used to make the op posite conversion. 208 In aum, the major advantages of our type reconstruction system are: l Programmers may write without using explicit type specifications. Mb-style programs may be used without modification in our type system. l Programmers may write using fully explicit type specifications. Explicitly-typed programs may be used without modification in our type system. l Programmers may use explicit types where desirable for documentation or other purposes, and omit them where they would decrease readability. l First-class polymorphic values can be used, pro vided that their types are declared. Thus, modules can be first-class values in our system. Programmers may use the open and close operators to simplify the use of first-class polymorphic values. Extract: IFX: A Typed Language IFX: A Typed Language For pedagogical purposes we will study type reconstruction for IFX, a simplified version of FX-89. FX-89 is a polymorphic typed language that allows side-effects and first-class functions. Its syntax and moat of its standard operations are strongly inspired by Scheme WsSSj. in SIGPLAN Notices 24(07) July 1989 includes Proceedings of the SIGPLAN '87 symposium on Interpreters and interpretive techniques view details in SIGPLAN Notices 24(07) July 1989 includes Proceedings of the SIGPLAN '87 symposium on Interpreters and interpretive techniques view details |