1
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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).

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I wouldn't say that Bool and Two are "actually the same type". At best they are isomorphic, or propositionally equal in a type theory with univalence. An additional problem is that they are equal/isomorphic in two different ways, so you'd immediately break coherence of subtyping. Have you seen any actually subtyping systems that equate the two? $\endgroup$ – Andrej Bauer Sep 20 at 8:56
  • $\begingroup$ Well, I'm not talking about e.g. homotopy type theory. I'm talking about a "structural type system" that makes these two types automatically interchangeable. This necessarily involves something kind of ad-hoc, like making False = Zero because they're both the first constructor. Univalence is kind of another angle on what a 'structural' theory could be, but I'm not sure it fits the wiki article linked. $\endgroup$ – Dan Doel Sep 20 at 18:48
  • $\begingroup$ I actually do work on a language (unison) that would enable you to do my example, basically because it is just two different naming schemes applied to the same data declaration structure, and the system recognizes this. However, you can also declare nominal types, because enum examples like this easily lead to confusion. Also there isn't any subtyping involved; it is just structural in the sense that the exact structure determines the type, rather than the names used. $\endgroup$ – Dan Doel Sep 20 at 18:51
  • $\begingroup$ This is kind of tangential, but does Unison have any effect polymorphism? If not, what's the type of iter : ('a -> unit) -> 'a list -> unit? I've been wondering ever since I heard of Unison. $\endgroup$ – Andrej Bauer Sep 20 at 20:41
  • $\begingroup$ Would you actually recommend identifying False and Zero as good PL design? Cause I sure wouldn't. $\endgroup$ – Andrej Bauer Sep 20 at 20:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.