Andrew K. Wright. Simple imperative polymorphism.
Lisp and Symbolic Computation, 8(4):343-356, December 1995.
H-M is unsound in the presence of imperative language features like references and exceptions.
This paper shows why, and describes a solution. Importantly, this solution has the property that equivalent abstractions have equivalent types - regardless of whether they are implemented functionally or imperatively. This is a desirable property if we want to separate interfaces from implementations - a very important SE goal.
Posted to theory by Ehud Lamm on 11/12/01; 11:52:24 AM