Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

Useful type inference must be faster than normalization. Otherwise, you could check safety conditions by running the program. We analyze the relationship between bounds on normalization and type inference. We show how the success of type inference is fundamentally related to the amnesia of the type system: the nonlinearity by which all instances of a variable are constrained to have the same type. Recent work on intersection types has advocated their usefulness for static analysis and modular compilation. We analyze System-I (and some instances of its descendant, System E), an intersection type system with a type inference algorithm. Because System-I lacks idempotency, each occurrence of a variable requires a distinct type. Consequently, type inference is equivalent to normalization in every single case, and time bounds on type inference and normalization are identical. Similar relationships hold for other intersection type systems without idempotency. The analysis is founded on an in...

• Type: Conference
• Year: 2004
• Where: ICFP
• Authors: Harry G. Mairson, Peter Møller Neergaard
• Keywords: ICFP 2004, Programming Languages, Type Inference, Type Inference Algorithm, Useful Type Inference