<p>In a structurally-typed language, one type is a subtype of another iff it has all of the fields/methods of the other with compatible types, meaning that field or return types are subtypes, parameter types are supertypes, arities match, and so on recursively for all the types mentioned. Every object or record defines an exact type for itself, and type declarations set out the attributes that any member of that type must provide.</p>
<p>The formal description of the system is pretty straightforward, but <strong>how do you actually implement that check in practice</strong> when types can have deep recursive references to themselves and other types? There is no predeclared definitive answer like in a nominal system, so it needs to be figured out each time, but <strong>figuring out whether type A <code>{ id -&gt; A }</code> subtypes type B <code>{ id -&gt; B }</code> seems to require knowing whether A is a subtype of B already!</strong></p>
<p>How does the compiler resolve these questions? That is, given an assignment of a value of a arbitrary structural type X to a variable of type Y, how does a practical typechecker decide whether it is allowed or not?</p>

<implementation><types><type-checker><structural-types>
How do you implement a structural subtyping checker?
CC BY-SA 4.0
2023-08-30T23:50:43.813Z
Sum types also can be subtypes of each other (interestingly, in an inverse to product types, one type is a subtype of the other iff the *other* type has all the variants of the first). This doesn't seem to occur much in practice.
apropos
CC BY-SA 4.0
2023-08-30T23:56:04.123Z
Yeah, I'm trying to confine this question to the smallest range I can for the moment so that answers can be well-scoped.
Michael Homer
CC BY-SA 4.0
2023-08-31T00:00:47.470Z
I think Typescript used to give up on such cases and say they aren't assignable. But as far as I know, it's fine to assume that `A <: B` is true when you're recursively checking the properties of `A` and `B` to determine whether `A <: B`. Think of it as making an assumption that `A <: B` is true, then searching through the structures of the two types to see if that assumption leads to a contradiction. Perhaps it gets messy when you introduce generic types, where you want to know if `A <: B<T>` and that depends on whether `A <: B<B<T>>` and that depends on `A <: B<B<B<T>>>` and so on.
kaya3
CC BY-SA 4.0
2023-08-31T00:31:44.743Z
@apropos I don't know about you, but as a regular Typescript user, I find structural subtyping relations between sum types useful quite often. A typical example comes from compiler development itself; you might have a sum type representing various kinds of expressions, and a subtype for the kinds which are valid assignment targets (lvalues). But more generally, control-flow type narrowing of sum types (e.g. if you check for one variant in one branch, then you can eliminate that variant from the type in the other branch) depends on the narrowed version of the type being a subtype.
kaya3
CC BY-SA 4.0
2023-09-06T21:21:23.290Z
And it's not as straightforward as you might think for nominal subtyping either. Unrestricted nominal subtyping in a language with contravariant generic conversions (C#, Java...) is undecidable! Turns out you can encode a Turing machine into your interface definitions and make the compiler simulate the machine to compute whether one interface is convertible to another.
Eric Lippert
CC BY-SA 4.0
2023-09-06T21:22:46.690Z
See https://www.cis.upenn.edu/~bcpierce/papers/variance.pdf which was written when it was still an open question as to whether it was undecidable.
Eric Lippert
<p>There is a straightforward but suboptimal approach that is suitable when there are relatively few types, and is fairly easy to implement. It involves an <span class="math-container">$N \times N$</span> matrix of presumed subtyping relationships that are iteratively falsified. At the end, there's a lookup table of every possible pair of types and whether they're compatible or not.</p>
<hr />
<p>First, collect all the types that appear in the program: this means type declarations, anonymous types, object or record construction sites, and anywhere else that creates a new type. Some of them may be duplicates, but that's ok. Give each of them a number <span class="math-container">$1..N$</span>.</p>
<p>Create a two-dimensional array of booleans with <span class="math-container">$N$</span> rows and <span class="math-container">$N$</span> columns. Each cell will represent whether the type of that row is a subtype of the type of that column.</p>
<p>To start with, fill the entire array with trues. We're going to begin by presuming that every type is compatible with every other type, and then repeatedly check each pair of types to find reasons to falsify the assumption until we run out of mismatches.</p>
<p>For each cell that is currently true, call the column type X and the row type Y. Loop over every member of type X, and</p>
<ul>
<li>Check whether a member of the same name is in Y. If not, we know that this is not a subtype, so put a false in this cell and move on to the next cell.</li>
<li>Check whether the number of parameters matches in both members (if applicable). If not, put a false in this cell, and move on to the next one.</li>
<li>Call the return type (or field type) of X's member P and the return type of Y's member C. Look up the cell in the row of C and the column of P: if it's false, we know that this can't be a subtype either, so put a false in this cell and move on. If it's true, we still think that <em>might</em> be a subtype, so continue.</li>
<li>Do the same thing for the parameters of the method, if applicable, swapping the row and column you look up.</li>
</ul>
<p>If nothing has proved that Y is <em>not</em> a subtype of X, the cell will still be true. Do the same for every cell of the array, and then start again from the beginning: there will be more false cells this time and so fewer to look at, and some of the return/parameter types that were presumed compatible last time won't be any more, so there will be more subtype relationships falsified each time. As soon as you find out that a type can't be a subtype of the other, you stop looking at it further and never need to come back to it.</p>
<p>Repeat until you make it all the way through the entire grid without making any changes. At this point, every pair that has been proved not to be a subtype contains false, and the remaining true cells represent genuine subtyping relationships. This array can be used as a lookup table for subtyping wherever it's required in the compiler or interpreter, like in variable assignments.</p>
<hr />
<p>This algorithm is guaranteed to complete and gives a sound subtyping, but it's doing a lot of work by examining every pair of types, and potentially every method of them, over and over again. For very large numbers of types and very large types this can be quite expensive, but it is cacheable and adding a new type requires only adding one row and column. There are some obvious optimisation steps (e.g. run only the cheap member/arity checks in the first pass), but beyond that more complex approaches are needed for meaningful savings. For a moderate number of types, this approach is fine for many practical use cases.</p>
<p>Any pair of types with no reason to believe that there <em>isn't</em> a subtype relationship will be left marked as true, correctly. In the <code>A { id -&gt; A }</code> &amp; <code>B { id -&gt; B }</code> case from the question, nothing will have falsified this relationship so A and B will correctly be considered subtypes of each other (synonyms). If A had additional members, it would still be considered a subtype of B, but not the reverse because a member wouldn't have been found.</p>

CC BY-SA 4.0
2023-08-31T01:21:41.120Z
2023-08-31T01:21:41.120Z
Michael Homer
CC BY-SA 4.0
2023-08-31T04:52:46.153Z
Curious, could you elaborate on the history (or lack thereof, if "folklore") of this algorithm?
apropos
CC BY-SA 4.0
2023-08-31T06:43:51.557Z
This is just the most naïve direct approach & it's somewhat *worse* than Cardelli's, let alone the more optimised approaches. I'm hoping someone with the experience will answer about the better ways.
Michael Homer
CC BY-SA 4.0
2023-09-01T08:50:00.847Z
I haven't implemented it yet, but I intend to look into exposing the structural plane explicitly in a future version of Tyr. As Tyr incorporates many paradigms, going with an O(n²) mem solution will not work. I guess the solution will be to use a canonical memory layouting algorithm and do a string prefix comparison. And recursive decent into types like functions. Ask again in ten years or so ;)
feldentm
CC BY-SA 4.0
2023-09-01T09:40:16.680Z
@feldentm Yes, type canonicalisation is a key part of the more-efficient algorithms, though they also take a pretty different approach to this overall. A good overview of the algorithmic situation a decade ago is [here](https://ecs.wgtn.ac.nz/foswiki/pub/Main/TechnicalReportSeries/ECSTR11-10.pdf) (I'm not sure whether/where it ended up in archival publication).
Michael Homer
# How do you implement a structural subtyping checker?
Posted by: username_0 on 2023-08-30
In a structurally-typed language, one type is a subtype of another iff it has all of the fields/methods of the other with compatible types, meaning that field or return types are subtypes, parameter types are supertypes, arities match, and so on recursively for all the types mentioned. Every object or record defines an exact type for itself, and type declarations set out the attributes that any member of that type must provide.

The formal description of the system is pretty straightforward, but **how do you actually implement that check in practice** when types can have deep recursive references to themselves and other types? There is no predeclared definitive answer like in a nominal system, so it needs to be figured out each time, but **figuring out whether type A `{ id -> A }` subtypes type B `{ id -> B }` seems to require knowing whether A is a subtype of B already!**

How does the compiler resolve these questions? That is, given an assignment of a value of a arbitrary structural type X to a variable of type Y, how does a practical typechecker decide whether it is allowed or not?
**Tags:** implementation types type-checker structural-types
> **Comments:**
> **username_1**: Sum types also can be subtypes of each other (interestingly, in an inverse to product types, one type is a subtype of the other iff the *other* type has all the variants of the first). This doesn't seem to occur much in practice.  
> **username_0**: Yeah, I'm trying to confine this question to the smallest range I can for the moment so that answers can be well-scoped.  
> **username_2**: I think Typescript used to give up on such cases and say they aren't assignable. But as far as I know, it's fine to assume that `A <: B` is true when you're recursively checking the properties of `A` and `B` to determine whether `A <: B`. Think of it as making an assumption that `A <: B` is true, then searching through the structures of the two types to see if that assumption leads to a contradiction. Perhaps it gets messy when you introduce generic types, where you want to know if `A <: B<T>` and that depends on whether `A <: B<B<T>>` and that depends on `A <: B<B<B<T>>>` and so on.  
> **username_2**: @apropos I don't know about you, but as a regular Typescript user, I find structural subtyping relations between sum types useful quite often. A typical example comes from compiler development itself; you might have a sum type representing various kinds of expressions, and a subtype for the kinds which are valid assignment targets (lvalues). But more generally, control-flow type narrowing of sum types (e.g. if you check for one variant in one branch, then you can eliminate that variant from the type in the other branch) depends on the narrowed version of the type being a subtype.  
> **username_3**: And it's not as straightforward as you might think for nominal subtyping either. Unrestricted nominal subtyping in a language with contravariant generic conversions (C#, Java...) is undecidable! Turns out you can encode a Turing machine into your interface definitions and make the compiler simulate the machine to compute whether one interface is convertible to another.  
> **username_3**: See https://www.cis.upenn.edu/~bcpierce/papers/variance.pdf which was written when it was still an open question as to whether it was undecidable.  
---
## 1 answers
### Answer by username_0 on 2023-08-31. Score: 5
There is a straightforward but suboptimal approach that is suitable when there are relatively few types, and is fairly easy to implement. It involves an $N \times N$ matrix of presumed subtyping relationships that are iteratively falsified. At the end, there's a lookup table of every possible pair of types and whether they're compatible or not.

---

First, collect all the types that appear in the program: this means type declarations, anonymous types, object or record construction sites, and anywhere else that creates a new type. Some of them may be duplicates, but that's ok. Give each of them a number $1..N$.

Create a two-dimensional array of booleans with $N$ rows and $N$ columns. Each cell will represent whether the type of that row is a subtype of the type of that column.

To start with, fill the entire array with trues. We're going to begin by presuming that every type is compatible with every other type, and then repeatedly check each pair of types to find reasons to falsify the assumption until we run out of mismatches.

For each cell that is currently true, call the column type X and the row type Y. Loop over every member of type X, and

* Check whether a member of the same name is in Y. If not, we know that this is not a subtype, so put a false in this cell and move on to the next cell.
* Check whether the number of parameters matches in both members (if applicable). If not, put a false in this cell, and move on to the next one.
* Call the return type (or field type) of X's member P and the return type of Y's member C. Look up the cell in the row of C and the column of P: if it's false, we know that this can't be a subtype either, so put a false in this cell and move on. If it's true, we still think that *might* be a subtype, so continue.
* Do the same thing for the parameters of the method, if applicable, swapping the row and column you look up.

If nothing has proved that Y is *not* a subtype of X, the cell will still be true. Do the same for every cell of the array, and then start again from the beginning: there will be more false cells this time and so fewer to look at, and some of the return/parameter types that were presumed compatible last time won't be any more, so there will be more subtype relationships falsified each time. As soon as you find out that a type can't be a subtype of the other, you stop looking at it further and never need to come back to it.

Repeat until you make it all the way through the entire grid without making any changes. At this point, every pair that has been proved not to be a subtype contains false, and the remaining true cells represent genuine subtyping relationships. This array can be used as a lookup table for subtyping wherever it's required in the compiler or interpreter, like in variable assignments.

---

This algorithm is guaranteed to complete and gives a sound subtyping, but it's doing a lot of work by examining every pair of types, and potentially every method of them, over and over again. For very large numbers of types and very large types this can be quite expensive, but it is cacheable and adding a new type requires only adding one row and column. There are some obvious optimisation steps (e.g. run only the cheap member/arity checks in the first pass), but beyond that more complex approaches are needed for meaningful savings. For a moderate number of types, this approach is fine for many practical use cases.

Any pair of types with no reason to believe that there *isn't* a subtype relationship will be left marked as true, correctly. In the `A { id -> A }` & `B { id -> B }` case from the question, nothing will have falsified this relationship so A and B will correctly be considered subtypes of each other (synonyms). If A had additional members, it would still be considered a subtype of B, but not the reverse because a member wouldn't have been found.
> **Comments:**
> **username_1** (2023-08-31): Curious, could you elaborate on the history (or lack thereof, if "folklore") of this algorithm?  
> **username_0** (2023-08-31): This is just the most naïve direct approach & it's somewhat *worse* than Cardelli's, let alone the more optimised approaches. I'm hoping someone with the experience will answer about the better ways.  
> **username_4** (2023-09-01): I haven't implemented it yet, but I intend to look into exposing the structural plane explicitly in a future version of Tyr. As Tyr incorporates many paradigms, going with an O(n²) mem solution will not work. I guess the solution will be to use a canonical memory layouting algorithm and do a string prefix comparison. And recursive decent into types like functions. Ask again in ten years or so ;)  
> **username_0** (2023-09-01): @feldentm Yes, type canonicalisation is a key part of the more-efficient algorithms, though they also take a pretty different approach to this overall. A good overview of the algorithmic situation a decade ago is [here](https://ecs.wgtn.ac.nz/foswiki/pub/Main/TechnicalReportSeries/ECSTR11-10.pdf) (I'm not sure whether/where it ended up in archival publication).  
---
