A Nominal Theory of Objects with Dependent Types

Vincent Cremet, Martin Odersky, Matthias Zenger
2002
Rapport ou document de travail

Résumé

We design and study newObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of Java's inner classes as well as virtual types and family polymorphism found in BETA or gbeta. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The technical report presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.

Official source

https://infoscience.epfl.ch/record/64407?ln=fr

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés

Chargement

Publications associées

Chargement

A Nominal Theory of Objects with Dependent Types

Vincent Cremet, Martin Odersky, Matthias Zenger

We design and study newObj, a calculus and dependent type system forobjects and classes which can have types as members. Type members canbe aliases, abstract types, or new types. The type system can modelthe essential concepts of Java's inner classes as well as virtual typesand family polymorphism found in BETA or gbeta. It can also model mostconcepts of SML-style module systems, including sharing constraintsand higher-order functors, but excluding applicative functors.The type system can thus be used as a basis for unifying conceptsthat so far existed in parallel in advanced object systems and inmodule systems. The technical report presents results on confluenceof the calculus, soundness of the type system, and undecidability oftype checking.

2002

Chargement

This paper studies the interplay between inner classes and virtual types. The combination of these two concepts can be observed in object-oriented languages like Beta or Scala. This study is based on a calculus of classes and objects composed of a very limited number of constructs. For example the calculus has neither methods nor class constructors. Instead it has a more general concept of abstract inheritance which lets a class extend an arbitrary object. Thanks to an interpretation of terms as types the calculus also unifies type fields and term fields. The main contribution of this work is to show that typing virtual types in the presence of inner classes requires some kind of alias analysis and to formalize this mechanism with a simple calculus.

2005

Chargement

Type Inference with Constrained Types

Martin Odersky

In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constrained logic programming. We show that the type system is sound with respect to a standard untyped compositional semantics. We present sufficient conditions on the constraint domain X so that the principal types property carries over to HM(X). The conditions turn out to be fairly simple and natural.

1999

Chargement