Type Systems: Formalizing Polymorphism continued
The notation OPEN(??1
?k . ?, ?1,
, ?k) means convert the type scheme ??1
?k . ? to the type ? where ? is ? with type variables ?1
?k replaced by fresh type variables ?1,
, ?k.
The notation CLOSE(?1, ?) means convert the type ?1 to the type scheme ??1
?k . ?1 where ?1,
, ?k are the type variables that appear in ?1 but not ?.
Polymorphism abbreviates brute force replication of the definition introduced in a let. The new type variables that appear in the type of M (rhs of the let binding) are arbitrary. The instantiation and polylet rules lets us adapt a symbolic type for M to each of the specific uses of x (the lhs of the let binding) in N (the body of the let).
The rhs side of the let binding cannot use x polymorphically because such usage is inconsistent with the fact that polymorphic let is an abbreviation mechanism!