title = {The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)},
year = {2020},
issue_date = {August 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {ICFP},
url = {https://doi.org/10.1145/3409006},
doi = {10.1145/3409006},
abstract = {MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.},
journal = {Proc. ACM Program. Lang.},
month = {aug},
articleno = {124},
numpages = {28},
keywords = {subtyping, type inference, principal types}
}
@inproceedings{PT98,
author = {Pierce, Benjamin C. and Turner, David N.},
title = {Local type inference},
booktitle = {Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
series = {POPL '98},
year = {1998},
location = {San Diego, California, United States},
pages = {252--265}
}
@article{OZZ01,
author = "Martin Odersky and Matthias Zenger and Christoph Zenger",
title = "Colored local type inference",
journal = "Proc. 28th ACM Symposium on Principles of Programming Languages",
abstract="Wildcards are a complex and subtle part of the Java type system, present since version5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.",
isbn="978-3-540-70592-5"
}
@article{WildcardsNeedWitnessProtection,
author = {Bierhoff, Kevin},
title = {Wildcards Need Witness Protection},
year = {2022},
issue_date = {October 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3563301},
doi = {10.1145/3563301},
abstract = {In this paper, we show that the unsoundness discovered by Amin and Tate (2016) in Java’s wildcards is avoidable, even in the absence of a nullness-aware type system. The key insight of this paper is that soundness in type systems that implicitly introduce existential types through subtyping hinges on still making sure there are suitable witness types when introducing existentially quantified type variables. To show that this approach is viable, this paper formalizes a core calculus and proves it sound. We used a static analysis based on our approach to look for potential issues in a vast corpus of Java code and found none (with 1 false positive). This confirms both that Java's unsoundness has minimal practical consequence, and that our approach can avoid it entirely with minimal false positives.},
