Type Systems: Sample Polymorphic Type Reconstruction
Consider a functional language with polymorphic lists. The operations on polymorphic lists include the binary function cons, unary functions first and rest, and the constant null. A sample program in this language is:
(let length := (? x (if (null? x) then 0 else (+ 1 (length (rest x))))) in
(+ (length (cons 1 null)) (length (cons true null))))
Sketch: ? | length: ? list ? int
1. Use letpoly rule to infer a symbolic type for the body of length
2. Add length with polymorphic type (a type scheme) to the type environment for body of let.
3. Instantiate the type scheme for length twice: once for bool and once for int.