Extending Hindley-Milner Type Inference with Coercive Structural Subtyping

Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow

We investigate how to add coercive structural subtyping to a type system for simply-typed lambda calculus with Hindley-Milner polymorphism. Coercions allow to convert between different types, and their automatic insertion can greatly increase readability of terms. We present a type inference algorithm that, given a term without type information, computes a type assignment and determines at which positions in the term coercions have to be inserted to make it type-correct. The algorithm is sound and, if the subtype relation on base types is a disjoint union of lattices, also complete. Also, a sound but incomplete extension of the algorithm to type classes is given. The algorithm has been implemented in the proof assistant Isabelle.

conference version long version

BibTeX:

@inproceedings{TraytelBN-APLAS11,
author={Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow},
title={Extending Hindley-Milner Type Inference with Coercive Structural Subtyping},
booktitle={Programming Languages and Systems (APLAS 2011)},
editor={H. Yang},
publisher=Springer,series=LNCS,volume={7078},pages={89-104},year=2011}