Type Systems: Formalizing Polymorphism
One extension to the simply typed language:
where let is recursive (scope of x includes the right hand side of definition of x)
Five extensions to our simple type system:
Type variables: ?1, ?2, ...
Type schemes: ? ::= ??1 … ?k . ? where ? is a type. Type schemes are not types!
Type environments (symbol tables) can contain type schemes; so can the table ?.
Additional inference rule:
?, x:?1 |? M:?1, ?, x:CLOSE(?1, ?) |? N:? (letpoly)
? |? (let x := M in N): ?
? |? c: OPEN(?(c), ?1, …, ?k) [c ? C and ?(c) = ??1 … ?k . ?]
?, x: ??1 … ?k . ? |? x: OPEN(??1 … ?k . ?, ?1, …, ?k)
[?1, …, ?k are type variables]