scholarly journals Three Discussions on Object-Oriented Typing

1991 ◽  
Vol 20 (362) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Object Oriented ◽  
Type Inference ◽  
Dynamic Typing ◽  
Static Versus Dynamic

<p>This paper summarizes three discussions conducted at the ECOOP'91 W5 Workshop on ''Types, Inheritance, and Assignments'' Tuesday July 16, 1991 in Geneva, Switzerland, organized by the authors.</p><p> </p><p>The three discussions were entitled ''Classes versus Types'', ''Static versus Dynamic Typing'', and ''Type Inference''. All these topics were assumed to be volatile and controversial; indeed, a broad range of diverging opinions were represented. However, much superficial disagreement seemed to be rooted in confusions about terminology. When such issues were resolved, there appeared a consensus about basic definitions and the - often incompatible - choices that one is at liberty to make. This clarification, which we hope to have described below, was the most important achievement of the workshop.</p>

scholarly journals Object-Oriented Type Inference

1991 ◽  
Vol 20 (345) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Fixed Point ◽  
Object Oriented ◽  
Type Inference ◽  
Finite Sets ◽  
New Approach ◽  
Optimizing Compiler ◽  
Point Derivation ◽  
Set Inclusion ◽  
Least Solution ◽  
Type Information

We present a new approach to inferring types in untyped object-oriented programs with inheritance, assignments, and late binding. It guarantees that all messages are understood, annotates the program with type information, allows polymorphic methods, and can be used as the basis of an optimizing compiler. Types are finite sets of classes and subtyping is set inclusion. Using a trace graph, our algorithm constructs a set of conditional type constraints and computes the least solution by least fixed-point derivation.

Precise concrete type inference for object-oriented languages

1994 ◽  
Vol 29 (10) ◽  
pp. 324-340 ◽  
Author(s):  
John Plevyak ◽  
Andrew A. Chien
Keyword(s):  
Object Oriented ◽  
Type Inference ◽  
Concrete Type ◽  
Object Oriented Languages

scholarly journals Object-oriented type inference

1991 ◽  
Vol 26 (11) ◽  
pp. 146-161 ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Object Oriented ◽  
Type Inference

Lightweight family polymorphism

2008 ◽  
Vol 18 (3) ◽  
pp. 285-331 ◽  
Author(s):  
CHIERI SAITO ◽  
ATSUSHI IGARASHI ◽  
MIRKO VIROLI
Keyword(s):  
Type System ◽  
Object Oriented ◽  
Expressive Power ◽  
Type Inference ◽  
Design Decision ◽  
Dependent Types ◽  
Parametric Methods ◽  
Complex Type ◽  
Original Proposal ◽  
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.

scholarly journals Decidable linear list constraints

10.29007/d7t4 ◽  
2018 ◽  
Author(s):  
Sabine Bauer ◽  
Martin Hofmann
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Object Oriented ◽  
Type Inference ◽  
Additional Restriction ◽  
Original Formulation ◽  
Amortized Analysis ◽  
Infinite Tree ◽  
Linear List

We present new results on a constraint satisfaction problem arising from the inference of resource types in automatic amortized analysis for object-oriented programs by Rodriguez and Hofmann.These constraints are essentially linear inequalities between infinite lists of nonnegative rational numbers which are added and compared pointwise. We study the question of satisfiability of a system of such constraints in two variants with significantly different complexity. We show that in its general form (which is the original formulation presented by Hofmann and Rodriguez at LPAR 2012) this satisfiability problem is hard for the famous Skolem-Mahler-Lech problem whose decidability status is still open but which is at least NP-hard. We then identify a subcase of the problem that still covers all instances arising from type inference in the aforementioned amortized analysis and show decidability of satisfiability in polynomial time by a reduction to linear programming. We further give a classification of the growth rates of satisfiable systems in this format and are now able to draw conclusions about resource bounds for programs that involve lists and also arbitrary data structures if we make the additional restriction that their resource annotations are generated by an infinite list (rather than an infinite tree as in the most general case). Decidability of the tree case which was also part of the original formulation by Hofmann and Rodriguez still remains an open problem.

Making Type Inference Practical

1992 ◽  
Vol 21 (385) ◽  
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.

Type Inference with Extended Pattern Matching and Subtypes

1993 ◽  
Vol 19 (1-2) ◽  
pp. 127-165
Author(s):  
Lalita A. Jategaonkar ◽  
John C. Mitchell
Keyword(s):  
Pattern Matching ◽  
Type System ◽  
Object Oriented ◽  
Type Inference ◽  
The Body ◽  
Object Oriented Programming ◽  
Inference Rules ◽  
Inference Algorithm

We study a type system, in the spirit of ML and related languages, with two novel features: a general form of record pattern matching and a provision for user-declared subtypes. Extended pattern matching allows a function on records to be applied to any record that contains a minimum set of fields and permits the additional fields of the record to be manipulated within the body of the function. Together, these two enhancements may be used to support a restricted object-oriented programming style. We define the type system using inference rules, and develop a type inference algorithm. We prove that the algorithm is sound with respect to the typing rules and that it infers a most general typing for every typable expression.

Sign in / Sign up

Export Citation Format

Share Document