Polymorphism, subtyping, and type inference in MLsub
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Dolan, S
Mycroft, Alan https://orcid.org/0000-0001-7013-8572
Abstract
We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system support type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict superset of core ML programs. This is made possible by keeping a strict separation between the types used to describe inputs and those used to describe outputs, and extending the classical unification algorithm to handle subtyping constraints between these input and output types. Principal types are kept compact by type simplification, which exploits deep connections between subtyping and the algebra of regular languages. An implementation is available online.
Description
Keywords
Subtyping, Polymorphism, Type Inference, Algebra
Journal Title
ACM SIGPLAN Notices
Conference Name
POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages
Journal ISSN
1523-2867
1558-1160
1558-1160
Volume Title
Publisher
ACM