Type inference for polymorphic references

The Hindley/Milner discipline for polymorphic type inference in functional programming languages is not sound if used on functions that can create and update references (pointers). We have found that the reason is a simple technical point concerning the capture of free type variables in store typings. We present a modified type inference system and prove its soundness using operational semantics. It is decidable whether, given an expression e, any type can be inferred for e. If some type can be inferred for e then a principal type can be inferred. Principal types are found using unification. The ideas extend to polymorphic exceptions and have been adopted in the definition of the programming language Standard ML.

Authors

• Mads Tofte

Keywords

No keywords are indexed for this paper.