| Playlist | schedule page slides as PDF |
Subtyping 1 — records (4:03)
A recap of records as in the record videos, but now with types. See typed-record.rhm.
Subtyping 2 — subtypes (5:19)
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 (1:44)
Extending the subtype relation to let field types be subtypes witin record subtype. (This turns out to be unsound for mutable records, but it’s fine for functional update.)
Subtyping 4 — function results (1:40)
Extending the subtype relation to allow function types that return subtypes.
Subtyping 5 — function arguments (2:44)
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.
Subtyping 6 — terminology (0:56)
Explains the terms covariant and contravariant.
Subtyping 7 — mutable records (3:35)
Our subtyping turns out to be unsound with mutable records, where field types must be invariant. See subtype_mut.