What's the difference between Row Polymorphism and Structural Typing?

Question

The definitions I've stumbled across seem to indicate they express the same idea. That's that the relationship between record types is determined by their fields (or properties) rather than their names. Their Wikipedia pages also seem to indicate the same idea:

A structural type system (or property-based type system) is a major class of type system in which type compatibility and equivalence are determined by the type's actual structure or definition and not by other characteristics such as its name or place of declaration.

In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are polymorphic on record field types (also known as rows, hence row polymorphism).

Are there any differences between them?

Answer 1

Structural type systems don't necessarily have anything to do with records. For instance, you could have a system where:

data Bool = False | True
data Two = Zero | One

are actually the same type, because they are both types with two nullary constructors. It also doesn't necessarily tell you much about records, because even though types are determined by their structure, the two records:

{s : S ; t : T}
{s : S ; t : T ; u : U}

are not the same structure, so you could have structural typing without there being anything convenient about these two types.

Similarly, row polymorphism in isolation doesn't tell you much---just that you can quantify over rows, and probably use them with e.g. a record type parameterized by a row. But there are all sorts of variations on what you can do with rows that really specify the capabilities of the system.

Usually with structural records people at least want subtyping. That allows you to say that my second record type above is a subtype of the first, so that you can pass the latter to anything expecting the former. A typical way to do this with row polymorphism is to instead quantify over the extra fields that may be present, and use some kind of row concatenation.

So perhaps a more targeted question is what is the difference between subtyping and quantifiers. The answer to that is generally that subtyping cannot express quantified types unless the quantified variable only occurs exclusively covariantly or contravariantly. So we could say:

(forall a. a -> T) ~= Top -> T
(forall a. T -> a) ~= T -> Bot

But for a type like forall a. a -> a, there is no one type to pick for a without losing information.

This extends to systems with just record subtyping vs. (appropriate) row polymorphism. However, if you have a system with subtyping and quantifiers, and subtyping can apply to quantified types, then the differences might be a lot more subtle. Having both quantifiers and subtyping can get quite tricky, though (not that row polymorphism is easy to get right, either).