Subtyping

Concept in type theory

Subtyping is a concept in type theory and programming languages that allows a given type to be substituted for another type. This is a fundamental aspect of polymorphism in object-oriented programming. Subtyping is often used to ensure that a program can handle different types of data in a flexible and reusable manner.

Definition

Subtyping is a relation between types, where one type (the subtype) is considered to be a specialized version of another type (the supertype). If a type S is a subtype of a type T, then an object of type S can be used wherever an object of type T is expected. This is known as the Liskov substitution principle.

Formalization

In formal type systems, subtyping is often defined using a set of rules that describe how types relate to each other. These rules are typically expressed in terms of a subtype relation, often denoted as S ≤ T, meaning S is a subtype of T.

Subtyping in Programming Languages

Subtyping is implemented in various ways across different programming languages. In Java, for example, subtyping is achieved through inheritance and interfaces. In C++, subtyping is implemented using classes and virtual functions.

Inheritance hierarchy

Nominal vs. Structural Subtyping

Subtyping can be classified into two main categories: nominal subtyping and structural subtyping.

• Nominal subtyping is based on explicit declarations. A type is a subtype of another if it is explicitly declared to be so. This is common in languages like Java and C++.
• Structural subtyping is based on the structure of the types. A type is a subtype of another if it has the same structure or a compatible structure. This is used in languages like TypeScript and Go.

Covariance and Contravariance

Subtyping interacts with variance in type systems, particularly in the context of generic programming.

• Covariance allows a type to be substituted with a subtype. For example, if List<Dog> is a subtype of List<Animal>, then covariance is supported.
• Contravariance allows a type to be substituted with a supertype. For example, if Function<Animal> is a subtype of Function<Dog>, then contravariance is supported.

Applications

Subtyping is crucial in designing flexible and reusable software components. It allows developers to write code that can operate on objects of different types, enhancing code reuse and maintainability. Subtyping is also essential in design patterns such as the factory method pattern and the strategy pattern.

Related pages

• Type theory
• Polymorphism (computer science)
• Inheritance (object-oriented programming)
• Liskov substitution principle