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]