Subtyping expresses safe substitutability between types. A judgment

$$S<:T$$

means that a value of type $S$ may be used wherever a value of type $T$ is expected.

A typing rule called subsumption captures this:

$$\frac{\Gamma\vdash e:S\qquad S<:T}{\Gamma\vdash e:T}.$$

For records, width subtyping often allows a record with more fields to stand in for one requiring fewer fields. If

$$S={x:\text{Int},y:\text{Int},color:\text{Color}}$$

and

$$T={x:\text{Int},y:\text{Int}},$$

then $S<:T$ when clients of $T$ use only x and y.

Subtyping is not the same as inheritance. Inheritance is a language mechanism for code or representation reuse; subtyping is a semantic relationship about safe replacement. Some languages connect them, but they need not coincide.

A sound subtype relation must respect the operations permitted by the supertype. Adding more capabilities can make a value more specific, while changing the accepted inputs of a function follows a different rule captured by variance.

Subtyping lets interfaces express partial knowledge: callers can rely on the guarantees of a general type without needing to know the concrete representation or every extra operation a value supports.