Subtyping

Résumé

In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation (written as S <: T, S ⊑ T, or S ≤: T ) means that any term of type S can safely be used in any context where a term of type T is expected. The precise semantics of subtyping here crucially depends on the particulars of how "safely be used" and "any context" are defined by a given type formalism or programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial, should the language support no (or very little) conversion mechanisms. Due to the sub

Source officielle

https://en.wikipedia.org/wiki/Subtyping

À 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.

Publications associées (20)

Publications associées

Chargement

Personnes associées (3)

Personnes associées

Chargement

Unités associées (2)

Unités associées

Chargement

Concepts associés (33)

Concepts associés

Chargement

Cours associés (5)

Cours associés

Chargement

Séances de cours associées (11)

Séances de cours associées

Chargement

Flexible subtyping relations for component-oriented formalisms and their verification

David Huerzeler

In this thesis we address the problem of safe substitutability in mobile component-oriented formalisms. We try to give a solution for different definitions of "safe" through a new notion of subtyping based on flexibility and observation. The aim is to have a definition which is applicable to a large numbers of existing formalisms, and which itself may be seen as an abstraction of many existing definitions of subtyping. In a similar way, we also try to see the verification of such relations in a way that may be applicable to many formalisms, and which may be seen as "containing" many existing techniques. Our hope is that our work may link these subtype definitions or verification techniques to formalisms they were not originally designed for. The contribution of this thesis can be divided in several points. First of all, the full formal definition of a "descriptive" component-oriented formalism based on concurrency, non determinism, complex composition and mobility. Also, the definition of a general flexible notion of subtyping, as well as a more particular example. Verification techniques for these subtyping relations are also grouped under the concept of component transformation, which is shown to include many other works. Finally, to illustrate the main concepts of our work, we provide a case study with a model of a "mobile" drinks dispenser.

EPFL2004

Chargement

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this report we take advantage of the fact that the Featherweight Generic Java (FGJ) calculus can be seen as a subset of Scala (you just have to squint a little bit!) and present a compilation scheme from cast-less FGJ into DOT as well as a proof that a well-typed cast-less FGJ program compiles down to a well-typed DOT term. Due to limitations in DOT subtyping rules, this requires imposing one limitation on our source program: the type parameters of the base types of a class can never refer back to the class itself (this excludes class C extends B[C] as well as class D extends B[E]; class E extends D). While this result is not especially interesting by itself given that FGJ is already known to be sound, it is a first step towards establishing soundness for larger subsets of Scala like the Pathless Scala calculus, the author plans to pursue this in his thesis (currently under preparation) which will also include the content of this report. It also clearly illustrates limitations in DOT that future work may wish to focus on.

2022

Chargement

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. In particular, objects can contain type members, which can be selected as types, called path-dependent types. Focusing on path-dependent types, we develop a type-theoretic foundation for Scala: the calculus of Dependent Object Types (DOT). We derive DOT from System F

EPFL2016

Chargement