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.
|Previous meeting||Return to the minutes index page||Next meeting|