TY - GEN
T1 - Extending hindley-milner type inference with coercive structural subtyping
AU - Traytel, Dmitriy
AU - Berghofer, Stefan
AU - Nipkow, Tobias
PY - 2011
Y1 - 2011
N2 - 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 according to the standard Hindley-Milner system (without any subtypes). The algorithm is sound and, if the subtype relation on base types is a disjoint union of lattices, also complete. The algorithm has been implemented in the proof assistant Isabelle.
AB - 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 according to the standard Hindley-Milner system (without any subtypes). The algorithm is sound and, if the subtype relation on base types is a disjoint union of lattices, also complete. The algorithm has been implemented in the proof assistant Isabelle.
UR - http://www.scopus.com/inward/record.url?scp=84055184525&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-25318-8_10
DO - 10.1007/978-3-642-25318-8_10
M3 - Conference contribution
AN - SCOPUS:84055184525
SN - 9783642253171
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 89
EP - 104
BT - Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Proceedings
T2 - 9th Asian Symposium on Programming Languages and Systems, APLAS 2011
Y2 - 5 December 2011 through 7 December 2011
ER -