Sciweavers

ICFP
2004
ACM

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

15 years 12 days ago
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...
Harry G. Mairson, Peter Møller Neergaard
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2004
Where ICFP
Authors Harry G. Mairson, Peter Møller Neergaard
Comments (0)