[Computer Science & Software Engineering]
Minutes of the FPU, Monday 5 March, 2001

A General Type Inference Framework for Hindley/Milner systems


Attendees

Bernie Pope, David Overton, Kevin Glynn, Fergus Henderson, Nick Nethercote, Martin Sulzmann, Peter Stuckey, Mark Brown

Minutes

Presenter: Martin Sulzmann

Martin presented his work on a general type inference framework for Hindley/Milner systems. This will also be presented at FLOPS 2001 (the Fifth International Symposium on Functional and Logic Programming).

In the framework he uses constraint based typing inference in place of the more traditional substitution model. Effectively the constraint system subsumes substitutions (by means of equality constraints).

The framework makes a clear distinction between the various phases of inference, these are: generation, propagation, solving, and simplification of constraints, and term reconstruction.

The framework also allows for partial solutions to typing problems which permits a more flexible constraint propagation during type inference. This is beneficial for both early and accurate detection of type errors, and type-based program analysis.

The framework also provides a means for very concise soundness and completeness results for derived type inference algorithms.

As a demonstration of his framework, Martin showed how unit types could be handled, and how Kennedy's problem can be solved in the framework, a problem for which substitution based inference fails.


References

Martin's (postscript) presentation is available here.

Previous meeting Return to the minutes index page Next meeting
Return to the FPU homepage

Bernie Pope
Last modified: Tue Mar 6 19:24:07 EST 2001