Subtyping & inheritance

LANG

In OOP, subtyping generally goes hand-in-hand with inheritance. If some class Cat inherits from another class Fluffy, then the former is a subtype of the latter. This follows from the Liskov substitution principle which defines subtypey-ness in terms of substitutability. Since inheritance implies, well, inheritance, then any method you can call on Fluffy you can also call on Cat without issue.

This could be seen as a specific case of a more general principle of record subtyping: if a have a record R, then any record which has at least all of R's fields is a subtype. For instance, if I have some type

type Pet = {
  name : String,
  age  : Nat,
}

then the only thing I can do with a value of that type is access its name or access its age. As such, a type like

type Cat = {
  name       : String,
  age        : Nat,
  fluffiness : Float,
}

can also be used as a Pet since accessing its name or its age are valid operations on this type too.

Inheritance is a different concept, and has to do with one type copying properties from another. In the Cat/Pet example, we could let Cat inherit some fields from Pet to minimize duplication:

type Cat = {
  fluffiness : Float,
  with Pet
}

For records and classes, this kind of inheritance does seem to imply subtyping – since inheriting guarantees we have at least all of the fields of the parent class.

This doesn't have to be the case. Consider an enum like this:

type Bool =
  true,
  false,

What would it mean for some other type to be a subtype of this? Following the principle of substitutability, some type HappyBool is a subtype of Bool if we can give a HappyBool to anything expecting a Bool.

A simple example of something expecting a Bool is an exhaustive pattern match:

fun to_string(self: Bool): String
  return case self
    is true  => "happy"
    is false => "sad"
  end
end

If HappyBool is to be a subtype of Bool, then to_string must work for all values of HappyBool, which means it must return some string, which means the current branches in the case expression must be exhaustive – all of which means that HappyBool must have at most all of Bool's variants.

Therefore, HappyBool is a subtype:

type HappyBool =
  true,

while ProperBool is in fact a supertype:

type ProperBool =
  true,
  false,
  file_not_found,

This has the fun consequence that sum types actually flip the subtyping relationship when inheriting:

type ProperBool =
  file_not_found,
  with Bool

In general, inheriting from a product-like type makes you the subtype, while inheriting from a sum-like type makes it the subtype.

All in all, subtyping and inheritance are two orthogonal concepts, but which are easy to confuse since the latter concept is most common in object-oriented languages where only product-like subtyping is available. There are some languages which feature sum-like subtyping and inheritance (like the in-development Star) and some which feature an explicit distinction between inheritance and subtyping (like in Ada where types may derive or be a subtype) .