It explained HM type inference in a slightly different way, strongly
emphasizing type inference as a non-standard interpretation. The
second main idea was relating polymorphism and `inlining' (copying).
Type schemas were then introduced as an optimization, to inlining. It
becomes clear why it is unsound to infer a polymorphic type for ref
: expressions of polymorphic types are always inlined (conceptually,
at least), which goes against the dynamic semantics of reference
The lectures also show how to infer not only the type but also the
type environment. This inference helps to make the point that `tests'
cannot replace typing. We can type check open expressions (and infer
the minimal environment they make sense to use in). We cannot run
(that is, dynamically check) open expressions.