Subtyping 1 — records (4:21)
A recap of records as in the record videos, but now with types. See typed-record.rkt.
Subtyping 2 — subtypes (6:01)
Motivation for and implementation of a subtype relation on record types. See subtype (but that implementation has everything through video 6).
Subtyping 3 — record fields (2:18)
Extending the subtype relation to let field types be subtypes. (This turns out to be unsound for mutable records.)
Subtyping 4 — function results (2:13)
Extending the subtype relation to allow function types that return subtypes.
Subtyping 5 — function arguments (3:07)
Extending the subtype relation to allow function types that consume supertypes, which is an example of contravariance. See subtype for all of the pieces put together.
The end of this video has a typo: function-argument (not function-result) types are contravariant. The mistake is fixed in the slides.
Subtyping 6 — terminology (1:04)
Explains the terms covariant and contravariant.
This video starts with the same typo: function-argument (not function-result) types are contravariant.
Subtyping 7 — mutable records (4:48)
Our subtyping turns out to be unsound withmutable records, where field types must be invariant. See subtype-mut.