Bidirectional type checking versus Hindley-Milner type checking, with some worked examples of subtyping:
miniblog.
Related Posts
I've really come to appreciate OCaml's notion of generics. It doesn't have subtyping, so e.g. you have an `int list` or an arbitrary `'a list`, but nothing inbetween.
As soon as you add constraints like Java's `List<? as Foo>` it become incredibly hard to produce good errors.
OCaml has several unusual design features that I've come to appreciate.
(1) Separating integer and float addition is really clear.
(2) No subtyping (everything is 'a or concrete) simplifies lots too.
I've realised the big advantage of teaching OO with physical analogies. It's well accepted that OO isn't just about modelling the eworld.
Physical items are great for explaining subtyping.
You can view types as subsets, and Ferrari <: Car <: Vehicle is intuitive.