Repository logo
 

Polymorphism, subtyping, and type inference in MLsub

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Dolan, S 

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

Volume Title

Publisher

ACM