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}