1,721,090 research outputs found
Divergence of Fsub type checking
No full textSystem F-less than or equal to is an extension of second-order typed lambda calculus, where a subtype hierarchy among types is defined, and bounded second-order lambda abstraction is allowed. This language is a basis for much of the current research on integration of typed functional languages with subtypes and inheritance. An algorithm to perform type checking for F-less than or equal to expressions has been known since the language Fun was defined. The algorithm has been proved complete, by the author acid Curien, which means that it is a semi-decision procedure for the type-checking problem. In this paper we show that this algorithm is not a decision procedure, by exhibiting a term which makes it diverge. This result was the basis of Pierce's proof of undecidability of typing for F-less than or equal to. We study the behavior of the algorithm to show that our diverging judgement is in some sense contained in any judgement which makes the algorithm diverge. On the basis of this result, and of other results in the paper, we claim that the chances that the algorithm will loop while type-checking a ''real program'' are negligible. Hence, the undecidability of F-less than or equal to type-checking should not be considered as a reason to prevent the adoption of F-less than or equal to as a basis For defining programming languages of practical interest. Finally, we show the undecidability of an important subsystem of F-less than or equal to
Foundations for extensible objects with roles
No full textObject-oriented database systems are an emerging. promising technology, underpinned by the integration of ideas from object-oriented languages alone with the specific needs of database applications. The fundamental reason for using such systems is that any real-world entity can be modeled by one object which matches its structure and behavior. To this end, the standard notion of object must be augmented so that it can model the fact that an entity may acquire new pieces of structure and behavior during its existence without changing its identity. To allow this extensibility in a statically typed system. a notion of context-dependent behavior (role playing) must be added to the basic features of object-oriented languages. This feature is also a useful modeling device. Languages with role mechanisms have already been proposed. However, their design is full of choices which cannot be easily justified. A strong foundation for the object-with-roles notion would be extremely helpful to justify these choices and to understand. and prove, the properties of such a mechanism. In this paper we describe such a foundation, building on the object model proposed by Abadi and Cardelli
Termination of system F-bounded: a complete proof
No full textSystem F-bounded is a second-order typed lambda-calculus with subtyping which has been defined to carry out foundational studies about the type systems of object-oriented languages. The almost recursive nature of the essential feature of this system makes one wonder whether it retains the strong normalization property, with respect to first- and second-order beta eta reduction of system F-less than or equal to. We prove that this is the case. The proof is carried out to the last detail to allow the reader to be convinced of its correctness
Modelling features of object-oriented languages in second order functional languages with subtypes
No full textObject oriented languages are an important tool to achieve software reusability in any kind of application and can increase dramatically software productivity in some special fields; they are also considered a logical step in the evolution of object oriented languages. But these languages lack a formal foundation, which is needed both to develop tools and as a basis for the future evolution of these languages; they lack also a strong type system, which would be essential to assure that level of reliability which is required to large evolving systems. Recently some researches have tried to insulate the basic mechanisms of object oriented languages and to embed them in strongly typed functional languages, giving to these mechanism a mathematical semantics and a set of strong type rules. This is a very promising approach which also allows a converging evolution of both the typed functional and the object oriented programming paradigms, making it possible a technology transfer in both directions. Most works in this field are very technical and deal just with one aspect of object oriented programming; many of them use a very similar framework. In this work we describe and exemplify that common framework and we survey some of the more recent and promising works on more specific features, using the framework introduced. We describe the results achieved and point out some problems which are still open, especially those arising from the interactions between different mechanisms
A STATIC TYPE SYSTEM FOR MESSAGE PASSING
No full textMuch research has been performed with the aim of isolating the basic notions of object-oriented languages and of describing them by basic operators which can be embedded in strongly-typed languages. In this context we define an atomic linguistic construct to capture the notion of message passing, and we define a static and strong type system, based on subtyping, for this construct. Message passing is modelled as the application of an overloaded function, whose behavior is determined only at compile-time on the basis of the class which created a distinguished argument, the object "receiving" the message. By embedding this mechanism in a strongly-typed language with subtyping and abstract data types we can obtain the full functionality of object-oriented languages. We show that this approach is strictly more expressive then the usual interpretation of message passing as selection plus application of a functional record field
A class abstraction for a hierarchical type system
No full textIn object oriented database languages and in languages supporting the semantic data model the construct used to collect sets of homogeneous entities is usually enriched with the possibility of imposing a set-inclusion relation among different collections. We call "class" such a data structure characterized by its ability of collecting values and of being in a containment relation with other classes. In many languages the class notion is not realized by a first class data type but is defined in some special way and the definition of a class is overloaded with constraints, and tightly linked to the definition of types. In this paper we embed in a strongly typed language with type inclusion a basic, but powerful, notion of a class data type which is just a first class data type orthogonal to the other notions of the language. In this context we study one of the most problematic issues in class data types, migration of objects from superclasses to subclasses
Complexity of kernel Fun subtype checking
No full textSystem kernel Fun is an abstract version of the system Fun defined by Cardelli's and Wegner's seminal paper [CW85], and is strictly related to system F less than or equal to. Extensions of these two systems are currently the basis of most proposals for strong type systems for object-oriented languages. We study here the problem of subtype checking for system kernel Fun, presenting the following results. We show that the standard kernel Fun subtype checking algorithm has an exponential complexity, and generates an exponential number of different subproblems. We then present a new subtype checking algorithm which has a polynomial complexity. In the process we study how variable names can be managed by a kernel Fun subtype checker which is not based on the De Bruijn encoding, and we show how to perform kernel Fun subtype checking with a ''constraint generating'' technique. The algorithm we give is described by a set of type rules, which we prove to be equivalent to the standard one. This new presentation of kernel Fun type system is characterized by a ''multiplicative'' behaviour, and it may open the way to new presentations for system F less than or equal to as well
- …
