Abstract

Type inference is considered of great significance for a programming language, which gives programmers convenience to write programs without type annotations. This talk covers basic background of type inference, from simply typed lambda calculus to Hindley-Milner type system. Further, as complete type inference for some type systems are undecidable, partial type inference is proposed to deal with this issue. And with local type inference, the amount of annotations needed could be greatly reduced.