Precise concrete type inference for object-oriented languages

AbstractFamily polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system. In this article, we propose a simpler solution oflightweightfamily polymorphism, based on the idea that families are represented by classes rather than by objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus, it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove that the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.

Download Full-text

Making Type Inference Practical

DAIMI Report Series ◽

10.7146/dpb.v21i385.6618 ◽

1992 ◽

Vol 21 (385) ◽

Cited By ~ 2

Author(s):

Nicholas Oxhøj ◽

Jens Palsberg ◽

Michael I. Schwartzbach

Keyword(s):

Image Compression ◽

Polynomial Time ◽

Object Oriented ◽

Type Inference ◽

Code Optimization ◽

Annotation Tool ◽

Inference Algorithm ◽

Exponential Time ◽

Type Information ◽

Object Oriented Languages

We present the implementation of a type inference algorithm for untyped object-oriented programs with inheritance, assignments, and late binding.The algorithm significantly improves our previous one, presented at OOPSLA'91, since it can handle collection classes, such as {\bf List}, in a useful way. Also, the complexity has been dramatically improved, from exponential time to low polynomial time. The implementation uses the techniques of incremental graph construction and constraint template instantiation to avoid representing intermediate results, doing superfluous work, and recomputing type information. Experiments indicate that the implementation type checks as much as 100 lines pr. second. This results in a mature product, on which a number of tools can be based, for example a safety tool, an image compression tool, a code optimization tool, and an annotation tool. This may make type inference for object-oriented languages practical.

Download Full-text

Efficient Inference of Object Types

BRICS Report Series ◽

10.7146/brics.v2i32.19935 ◽

1995 ◽

Vol 2 (32) ◽

Cited By ~ 1

Author(s):

Jens Palsberg

Keyword(s):

Object Oriented ◽

Type Systems ◽

Order Type ◽

Type Inference ◽

First Order ◽

Inference Problems ◽

Object Oriented Languages

Abadi and Cardelli have recently investigated a calculus of objects [2]. The calculus supports a key feature of object-oriented languages: an object can be emulated by another object that has more refined methods. Abadi and Cardelli presented four first-order type systems for the calculus. The simplest one is based on finite types and no subtyping, and the most powerful one has both recursive types and subtyping. Open until now is the question of type inference, and in the presence of subtyping the absence of minimum typings poses practical problems for type inference [2]. In this paper we give an O(n^3) algorithm for each of the four type inference problems and we prove that all the problems are P-complete. We also indicate how to modify the algorithms to handle functions and records.

Download Full-text

Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification?

Formal Verification of Object-Oriented Software - Lecture Notes in Computer Science ◽

10.1007/978-3-642-18070-5_3 ◽

2011 ◽

pp. 31-45 ◽

Cited By ~ 8

Author(s):

Davide Ancona ◽

Andrea Corradi ◽

Giovanni Lagorio ◽

Ferruccio Damiani

Keyword(s):

Object Oriented ◽

Type Inference ◽

Object Oriented Languages

Download Full-text

Type Inference with Selftype

BRICS Report Series ◽

10.7146/brics.v2i34.19937 ◽

1995 ◽

Vol 2 (34) ◽

Author(s):

Jens Palsberg

Keyword(s):

Polynomial Time ◽

Object Oriented ◽

Type Inference ◽

Inference Algorithm ◽

Type Checking ◽

Object Oriented Languages

The metavariable self is fundamental in object-oriented languages. Typing self in the presence of inheritance has been studied by Abadi and Cardelli, Bruce, and others. A key concept in these developments is the notion of selftype, which enables flexible type annotations that are impossible with recursive types and subtyping. Bruce et al. demonstrated that, for the language TOOPLE, type checking is decidable. Open until now is the problem of type inference with selftype. In this paper we present a type inference algorithm for a type system with selftype, recursive types, and subtyping. The example language is the object calculus of Abadi and Cardelli, and the type inference algorithm runs in nondeterministic polynomial time.

Download Full-text