In computer science, a subtype of a given type is another type such that an element of the subtype may be used anywhere an element of the given type (the supertype) is allowed. This general semantic definition is known as the Liskov substitution principle. In practice, any given programming language may define its own notion of subtyping, or none at all.

For example, in most class-based object-oriented languages, subclasses give rise to subtypes: if A is a subclass of B, then an instance of class A may be used in any context where an instance of type B is expected; thus we say A is a subtype of B. A consequence of this is that any variable or parameter declared as having type B might, at run time, hold a value of class A; in this situation many object-oriented programmers would say that B is the variable's static type and A is its dynamic type.

As another example, a language might allow integer values to be used wherever floating-point values are expected, or it might define a type number containing both the integers and the reals. In the first instance, the integer type would be a subtype of the floating-point type; in the second, those two types might be unrelated to each other by subtyping but both would be subtypes of number.

Programmers may take advantage of subtyping to write code in a more abstract manner than would be possible without it. Consider the following example:

function max (x as number, y as number) is
  if x < y then
    return y
  else
    return x
end

If integer and real are both subtypes of number, then values of either type can be passed to this function. Because of this, subtyping is often considered a form of polymorphism.

In type theory, the subtype relation is often written <:, so that A<:B means that A is a subtype of B. Subtyping in type theory is characterized by the fact that any expression of type A may also be given type B if A<:B; the formal typing rule that codifies this is known as the subsumption rule.

Type theorists make an important distinction between nominal subtyping, in which only types declared in a certain way may be subtypes of each other, and structural subtyping, in which the structure of two types determines whether or not one is a subtype of the other. The class-based object-oriented subtyping described above is nominal; a structural subtyping rule for an object-oriented language might say that if objects of type A can handle all of the messages that objects of type B can handle (that is, if they define all the same methods), then A is a subtype of B regardless of whether either inherits from the other. Sound structural subtyping rules for types other than object types are also well known.

Implementations of programming languages with subtyping fall into two general classes: inclusive implementations, in which the representation of any value of type A also represents the same value at type B if A<:B, and coercive implementations, in which a value of type A can be automatically converted into one of type B. The subtyping induced by subclassing in an object-oriented language is usually inclusive; subtyping relations that relate integers and floating-point numbers, which are represented differently, are usually coercive.

In almost all type systems that define a subtyping relation, it is reflexive (meaning A<:A for any type A) and transitive (meaning that if A<:B and B<:C then A<:C). This makes it a preorder on types.