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.