Human-like Explanations of Polymorphic Types

Abstract: While Hindley-Milner polymorphic type inference algorithms are an excellent basis for mechanical type checking, they are poor at generating type explanations. They analyse programs top-down from left to right, and make use of internal artifacts, like polymorphic type variables, that do not appear in original programs. In contrast, investigation of human type explanations suggests that they prefer free scanning of programs in two dimensions, focusing on constructs of known type and avoiding the use of type variables.

We have incorporated such human techniques in a novel type explanation system for a teaching subset of Standard ML. The system is based on a Unification of Assumption Environments algorithm, and identifies all possible explanations of types and chooses the most succinct.

The genesis and design of the system are presented, and its behaviour is compared to that of human experts.

Bio:

Dr. Greg Michaelson is a senior lecturer at the Department of Computing & Electrical Engineering of Heriot-Watt University, Edinburgh. He is a member of the Dependable Systems Group and recently coordinated the 3rd Scottish Functional Programming Workshop.

Enquiries: sals@mri.mq.edu.au