Explaining Polymorphic Types

Polymorphic types in programming languages facilitate code reuse, increase reliability and reduce semantic errors in programs. Hindley–Milner type inference forms a strong basis for checking polymorphic types but is less well suited to explaining them, as it introduces intermediate constructs that relate poorly to a programmer's understanding of the program. We report an experiment into expert human type explanation and uncover a simple set of rules for human-like explanations. We present a type explanation system based on these rules rather than Hindley–Milner inference. The system uses a new $H$ inference algorithm to annotate types with explanations and is designed to produce succinct, non-repetitive explanations with minimal reference to artefacts of mechanized type inference.