Use a value where a less specific view is sufficient
Read directional substitutability without confusing it with equality or conversion.
By the end: check immutable record width and depth compatibility under explicit rules.
A compatibility relation is directional
If Cat is a subtype of Animal, a Cat can be used where an Animal is required. The reverse does not follow: an Animal could be a Dog. Our lab stipulates Cat and Dog as disjoint refinements of Animal. It does not infer a hierarchy from class names. We write this direction as Cat <: Animal; the symbol <: means “is a subtype of.”
Unification asks whether types can be made equal. Subtyping asks whether a value described by one type satisfies a required view. Cat and Animal are not equal in this model even when Cat is acceptable for an Animal input. Do not reuse an equality solver as if it checked this relation.
Derive a required view from permitted reads
A required view tells a piece of code which operations it may perform on a value. For a record, a collection of named fields, those operations are reads by field name. Suppose a consumer may read name as Text and pet as Animal. A supplied value must support both reads with compatible results. Nothing in this requirement says that the supplied value has exactly two fields. Nor does it require the consumer to know whether the animal is specifically a Cat or Dog. Compatibility concerns the available operations, not identical descriptions.
The symbol <: gives this requirement a direction. Reading S <: T means that a value described by S can stand in a position requiring T. The supplied description is on the left; the required description is on the right. Cat <: Animal holds because the hierarchy explicitly allows each Cat as an Animal. Animal <: Cat fails because a Dog satisfies Animal without satisfying Cat. This is an argument about every value allowed by a description. Finding one Cat among possible Animals cannot justify replacing the whole Animal description with Cat.
One Dog defeats the reverse inclusion
Cora supports the Cat-to-Animal direction. Dune witnesses why Animal cannot guarantee Cat in this finite illustration.
To make that distinction concrete, imagine a paper world with exactly two animal witnesses, a cat named Cora and a dog named Dune. A witness is a particular value used to test a claim. Cat allows Cora, Dog allows Dune, and Animal allows both. Every allowed Cat belongs to Animal in this miniature world. The reverse inclusion fails at Dune. This finite illustration explains the direction; the lab does not enumerate animal objects or claim that these two objects are the entire real animal world. Its relation follows the stipulated type names directly.
Now supply the paper record {name: Text, pet: Cat, age: Int} to the consumer. Checking name succeeds because Text can supply Text. Checking pet succeeds because Cat can supply Animal. The consumer never requests age, so age adds no unsatisfied obligation. These are three separate observations, not one overall resemblance judgment. Checking each required field gives a repeatable method that also explains a rejection. A record with a suitable pet but no name fails the name read, even if every other field contains useful information for a different consumer.
This compatibility does not describe a runtime conversion. The rule need not turn Cora into a less specific animal object, delete age, or copy a record. It describes what code using the required view may assume. A particular implementation might copy or project data, but this lab only compares type descriptions and returns a compatibility result. The earlier inference engine is also unchanged. Its type equations still require equality among finite constructor trees. Cat, Dog, Animal, and record compatibility belong to this separate experiment, not to that engine's application or unification rules.
Required reads determine the comparison
Required read
Supplied guarantee
Reason
name as Text
name: Text
Text <: Text
pet as Animal
pet: Cat
Cat <: Animal
No age read
age: Int
No target obligation
Each required read passes independently. An unused age field neither creates a requirement nor repairs a failed one.
One consequence is that a failed reverse comparison needs its own explanation. From the required {name: Text, pet: Animal} view, neither age nor a specifically Cat pet is guaranteed. A consumer requiring the larger Cat record might read age or rely on the narrower pet description. Either obligation can fail. This is why a successful source-to-target comparison does not establish target-to-source compatibility. The two questions authorize different reads. Even if the particular source value happens to satisfy both descriptions, the less informative type cannot promise that fact for every value it permits.
Immutable records expose required fields
A consumer requiring name: Text and pet: Animal can read those fields from a record that also contains age: Int and whose pet is Cat. Extra fields are harmless for this read-only view. This is width subtyping; using a more specific compatible field type is depth subtyping.
Missing a required field or supplying Text where Animal is required fails. The lab compares source fields with a fixed required record. Field order does not affect compatibility. These are structural rules for immutable records, not a promise about every nominal class hierarchy or a particular compiler’s excess-property policy.
Separate extra fields from narrower field types
Width subtyping permits a record with additional fields to supply a view requiring fewer fields. Depth subtyping permits a field with a more specific compatible type to supply a less specific required field. These names distinguish two reasons the same record can fit. Width concerns which field names are present. Depth concerns the type attached to a shared field name. The supplied name/pet/age record uses width to ignore age and depth to expose a Cat pet as Animal. Neither step changes the spelling or meaning of the required fields.
A paper derivation can separate the steps. Begin with S = {name: Text, pet: Cat, age: Int}. Forgetting the age requirement gives M = {name: Text, pet: Cat}. Widening the permitted pet description gives T = {name: Text, pet: Animal}. S fits M and M fits T, so S also supports all reads allowed through T. This chaining property is called transitivity. It follows here because any read justified by T is supported by M, and every such M read is supported by S. These are paper type descriptions, not strings accepted by a parser.
A compatibility derivation separates width and depth
Step
name requirement
pet requirement
age requirement
Source S
Text
Cat
Int
S <: M by width
Text
Cat
Not required
M <: T by depth
Text
Animal
Not required
Conclusion S <: T
Text <: Text
Cat <: Animal
No read needed
The intermediate view removes the age requirement first. The second step weakens only the pet read guarantee.
Reversing either step exposes a different failure. T does not fit M because Animal does not guarantee Cat. M does not fit S because M does not guarantee an age field. Adding an arbitrary age value would not prove the missing static claim; it would construct a different value under another rule. Similarly, inspecting a runtime pet and discovering a Cat would be a runtime check, absent from this lab. The structural rule cannot assume that inspection happened. It must decide using only the source field names, their declared types, and the stipulated base-type relation.
For an exact checking procedure, inspect the required fields one at a time. First locate the same field name in the source. If it is missing, stop with a missing-field explanation. If it exists, compare the supplied base type with the required base type. Every required field must pass. This means the obligations combine with "and," not "or." A matching name cannot compensate for an incompatible pet. Extra source fields do not enter this loop. The helper bounds records to at most four fields, but a field-count limit is not part of the mathematical reason for compatibility.
Field order adds another useful contrast. The paper records {pet: Cat, name: Text} and {name: Text, pet: Cat} support the same named reads. This model therefore treats them as equivalent views despite their different written order. It does not identify {name: Text} with {label: Text}, because changing a field name changes the operation the consumer requests. Both fields might contain the same text in one value, but the rule does not search for substitute names. Structural means the declared field structure matters instead of a record's nominal identity, not that all similarly shaped descriptions are interchangeable.
Reordering preserves reads; renaming changes them
Paper source
name lookup
pet lookup
Fits?
name: Text; pet: Cat
Text
Cat <: Animal
Yes
pet: Cat; name: Text
Text
Cat <: Animal
Yes
label: Text; pet: Cat
Missing name
Cat <: Animal
No
name: Text; pet: Text
Text
Text is not Animal
No
These paper comparisons all require name: Text and pet: Animal. Field identity, not written position, determines lookup.
Required fields with unrelated base types fail even when their representations look convenient. A Text pet does not supply Animal; the lab does not interpret a string containing "Cat" as a Cat value. Int and Bool also have no nontrivial subtype relationship here. A boolean stored in a machine word is not therefore an integer under these rules. The compatibility procedure relies on the language's declared operations and relations, not guesses about storage layouts. Keeping the relation explicit makes both positive and negative answers explainable without appealing to a particular host language or compiler's special cases.
Inspect the rules and their result
Compare source fields with a required read-only view
Source record type
Field
Type
name
Text
pet
Cat
age
Int
Required record type
Field
Type
name
Text
pet
Animal
Requirement
Source
Satisfied?
name: Text
Text
Yes
pet: Animal
Cat
Yes
Source fits target: Yes. Target fits source: No.
Presets replace only the source record type. The target stays fixed. Extra fields are allowed, required fields must exist, and each supplied field type must be a subtype of its required type. This idealized immutable structural rule is not TypeScript excess-property checking.
Source record
Required view
Fits?
name: Text, pet: Cat, age: Int
name: Text, pet: Animal
Yes
name: Text
name: Text, pet: Animal
No
name: Text, pet: Text
name: Text, pet: Animal
No
The model assumes immutable records and the declared Cat <: Animal relation.
Use the presets to isolate each failed obligation
The live comparison fixes the required record at name: Text and pet: Animal. Start with Extra field and Cat. Read the requirement rows before the overall status. The name row passes by equality, and the pet row passes through Cat <: Animal. Age appears only in the source display because the target does not request it. Source fits target is Yes, while the reverse is No. For that reverse question, the target would need both a Cat guarantee and an age field, neither of which follows from its displayed type.
Select Missing pet next. This preset replaces the entire source record with name: Text. The name obligation remains satisfied while the pet obligation now lacks a source field. The failure is not about an unknown animal subtype or a conflict between Text and Animal. There is no supplied pet type to compare at all. Separating field presence from field compatibility matters when reading diagnostics. A missing field usually needs a different change from a present field with an incorrect type. Adding irrelevant fields cannot resolve either failure in the required pet position.
Four presets produce distinct evidence
Preset
name obligation
pet obligation
Source fits target
Extra field and Cat
Pass
Cat <: Animal
Yes
Missing pet
Pass
Missing field
No
Wrong pet type
Pass
Text is not Animal
No
Dog field
Pass
Dog <: Animal
Yes
The fixed target makes the missing-field and incompatible-field failures distinguishable despite their identical overall No result.
Select Wrong pet type and compare it directly with Missing pet. Now the source has a field named pet, so the lookup step succeeds. The subtype step fails because Text does not supply Animal. This preset distinguishes two stages that would both produce an overall No. It also shows why the number of source fields is insufficient evidence. Both the required record and this wrong source have two fields, yet the read contract fails. Compatibility counts neither matching labels alone nor total fields; it checks the type of each required named read.
Finally select Dog field. Dog <: Animal succeeds just as Cat <: Animal did, and the name field remains Text. Source fits target becomes Yes. Target fits source is still No, although this source has no extra age field. That isolates depth as enough to make the relation asymmetric. The target might describe a Cat pet, which would not satisfy this Dog-specific source requirement. Replacing Cat with Dog does not indicate preference between animal kinds. Both are permitted Animal refinements, and neither is a subtype of the other in the stipulated hierarchy.
These four presets vary several source details across the sequence, but the fixed requirement lets you attribute each result to a particular obligation. There is no field editor or hierarchy editor in this lab. For an additional paper comparison, require only name: Text. Every displayed source would fit that weaker view, including Wrong pet type, because that consumer never reads pet. Conversely, requiring pet: Cat would reject Dog field. A compatibility judgment belongs to a source-target pair; it is not an intrinsic "good record" label that remains unchanged when the consumer changes.
Reverse comparisons need stronger guarantees
Proposed reverse use
Value the starting view permits
Broken requirement
Animal target as Cat-and-age source
name text, Dog pet, no age
Cat pet and age missing
Animal target as Dog source
name text, Cat pet
Dog pet not guaranteed
Name-only source as Animal target
name text, no pet
pet field missing
A permitted counterexample is enough to refute a replacement claim. These witnesses are paper records, not evaluated values.
A useful way to report a result is to name the lost guarantee. For Extra field and Cat, the forward direction permits forgetting age and the Cat refinement, while the reverse cannot recover them. For Dog field, only the specific pet guarantee is lost. For Missing pet, the forward direction cannot establish field existence. For Wrong pet type, field existence is established but its read type is wrong. This vocabulary transfers to larger read-only interfaces because it identifies the exact assumption the consumer would otherwise make without evidence. It does not rely on interpreting button order as a stronger-to-weaker scale.
Mutability changes the argument
A read-only view cannot use a broader alias to overwrite a Cat field with a Dog. A writable view might permit that write. The safety argument for immutable depth subtyping therefore does not automatically carry over to mutable records. The next lesson separates read and write positions.
Subtyping alone also does not establish domain semantics. Two records with a numeric identifier may represent different concepts. Nominal names, wrappers, or brands can distinguish such uses, but external data still needs validation. Decide which distinction the program needs before choosing a representation.
Distinguish a view restriction from a write permission
The immutable qualification is essential to the depth argument. Reading a Cat as Animal never produces a value outside Animal. Writing through an Animal-typed field is different: that interface would permit a Dog as well. If the same storage were still visible through a Cat-typed view, a Dog write could invalidate the old Cat read promise. An alias is another name or reference to the same storage. The record lab has no write operations or alias controls. This is a hypothetical extension explaining why its successful read-only comparison cannot automatically authorize mutation.
Consider the extension one operation at a time. A location initially contains Cora, and the original view promises that reading pet yields Cat. Suppose an invalid broader alias permits writing any Animal into that location. Dune is allowed through the alias because Dune is a Dog and every Dog is Animal. After that write, the original read returns Dune, contradicting its Cat promise. No field vanished and no operation confused name with pet. The failure comes solely from combining a broad write permission with a narrow read guarantee over the same location.
A broader writable record alias would invalidate a read
Stage
Original record view
Hypothetical broader alias
Stored pet
Before
Reads Cat
Reads and writes Animal
Cora: Cat
Broader write
Still promises Cat
Writes Dune: Dog
Dune: Dog
Original read
Receives Dog, violating Cat
No further action
Dune: Dog
This hypothetical extension is absent from the immutable record lab. The write changes shared storage, not the original promise.
Removing write access removes that particular counterexample. A read-only Animal view cannot install Dune. The existing Cat location can therefore keep supplying Animal reads without that view changing its contents. This statement assumes the immutable setting of the lab, not arbitrary outside mutation. A language that allows external writers needs rules covering their access too. The next lesson derives the separate directions for producers, consumers, and shared read-write cells. Here the important distinction is between forgetting information in a read-only description and granting a new operation that can change information other code relies on.
Structural compatibility also leaves semantic distinctions unexpressed when they share the same structure. Imagine paper records {id: Int} for an order and {id: Int} for a customer. Their named reads coincide, so this structural rule cannot prevent swapping them. A nominal type distinguishes values by a declared identity instead of only their accessible fields. A wrapper can similarly keep an identifier in a distinct category until code explicitly extracts it. These are design options outside the record lab. They solve a category-mixing problem, not a missing-field or Cat-to-Animal compatibility problem.
Even a distinct customer identifier type does not prove that its number names a real customer or that a caller may access that customer. Those are different predicates, meaning conditions that may hold or fail for a value. A representation can establish the category without establishing database existence or permission. Conversely, a runtime existence check need not grant every operation on the found record. The useful transfer is to state the consumer's actual requirement before selecting evidence. Read availability, category identity, and authorization can concern the same value while requiring different rules to justify them.
Similar records can require different evidence
Required fact
Structural read rule enough?
Separate evidence needed
id can be read as Int
Yes, with id: Int present
Compatible field declaration
id is specifically a CustomerId
No, if both categories are Int
Distinct type construction rules
id names an existing customer
No
Existence check
Caller may update this customer
No
Authorization decision
Matching fields supports named reads. It does not establish category identity, database existence, or permission to act.
When evaluating a proposed broader interface, list its permitted operations and compare them with the original guarantees. For immutable records, checking every required read gives the width and depth rules already derived. If writes appear, repeat the argument with values the new interface permits writing; do not retain the old conclusion without checking them. If a nominal distinction appears, check the declaration rules rather than assuming matching fields suffice. This method explains why a result can be correct inside the bounded lab yet inapplicable to a different language feature. It identifies the changed assumption instead of treating all compatibility rules as one universal relation.
Exercises
Reverse a valid assignment
If a record with name and age fits a read-only name-only view, does every name-only record fit the larger view?
Hint
The larger consumer will try to read age.
Worked answer
Direction
Needed information
Result
name+age to name
name
Available
name to name+age
name and age
age may be absent
Compatibility need not be symmetric.
No. The name-only record may have no age field. Width subtyping permits forgetting access to extra fields, not manufacturing missing fields. The reverse assignment needs a stronger source guarantee.
Same shape, different meaning
OrderId and CustomerId are both represented by integers. Does structural equality alone prevent swapping them?
Hint
Representation and domain identity are different requirements.
Worked answer
Property
Established by distinct ID types alone?
Do not interchange categories
Can be enforced by the chosen type design
ID exists
No
Caller is authorized
No
A stronger static distinction still has runtime boundaries.
No. If both types are just Int, the checker sees no distinction. A language can use distinct nominal wrappers or an appropriate brand to represent it. That prevents some accidental swaps but does not prove that a numeric ID exists in a database or belongs to the current user.
Sources and further reading
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected structural compatibility and documented soundness trade-offs. Exact compiler behavior depends on flags and language version; our idealized variance lab is not a conformance test.