Polymorphism, subtyping, and type inference in MLsub

Abstract

We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports 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.

References

1. R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS), 15 (4), 1993.
2. H. Bekiˇc. Definable operations in general algebras, and the theory of automata and flowcharts. In C. Jones, editor, Programming Languages and Their Definition, volume 177 of Lecture Notes in Computer Science, pages 30–55. Springer Berlin Heidelberg, 1984.
3. F. Bourdoncle and S. Merz. Type checking higher-order polymorphic multi-methods. In POPL ’97: 24th ACM Symposium on Principles of Programming Languages, pages 302–315, Paris, Jan. 1997. ACM.
4. G. Castagna and Z. Xu. Set-theoretic foundation of parametric polymorphism and subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP ’11, pages 94–106. ACM, 2011.
5. B. A. Davey and H. A. Priestley. Introduction to lattices and order. Cambridge University Press, 2002.
6. S. Dolan. Algebraic Subtyping. PhD thesis, University of Cambridge, 2016. To appear.
7. J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. Electronic Notes in Theoretical Computer Science, 1:132–153, 1995. MFPS XI, Mathematical Foundations of Programming Semantics, 11th Annual Conference.
8. J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. In Proceedings of the Tenth Annual Conference on Object-oriented Programming Systems, Languages, and Applications, OOPSLA ’95, pages 169–184. ACM, 1995.
9. F. Henglein and J. Rehof. The complexity of subtype entailment for simple types. In Logic in Computer Science, 1997. LICS’97. Proceedings., 12th Annual IEEE Symposium on, pages 352–361. IEEE, 1997.
10. F. Henglein and J. Rehof. Constraint automata and the complexity of recursive subtype entailment. In 25th International Colloquium on Automata, Languages and Programming, ICALP ’98, pages 616–627. Springer Berlin Heidelberg, 1998.
11. M. Hoang and J. C. Mitchell. Lower bounds on type inference with subtypes. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’95, pages 176–185. ACM, 1995.
12. L. Ilie, G. Navarro, and S. Yu. On NFA reductions. In J. Karhumäki, H. Maurer, G. Păun, and G. Rozenberg, editors, Theory Is Forever, volume 3113 of Lecture Notes in Computer Science, pages 112–124. Springer Berlin Heidelberg, 2004.
13. S. Kaes. Type inference in the presence of overloading, subtyping and recursive types. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP ’92, pages 193–204. ACM, 1992.
14. D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’93, pages 419–428. ACM, 1993.
15. A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4 (2):258–282, 1982.
16. J. Niehren and T. Priesnitz. Entailment of non-structural subtype constraints. In P. Thiagarajan and R. Yap, editors, Advances in Computing Science — ASIAN’99, volume 1742 of Lecture Notes in Computer Science, pages 251–265. Springer Berlin Heidelberg, 1999.
17. J. Niehren and T. Priesnitz. Non-structural subtype entailment in automata theory. In N. Kobayashi and B. C. Pierce, editors, Theoretical Aspects of Computer Software, volume 2215 of Lecture Notes in Computer Science, pages 360–384. Springer Berlin Heidelberg, 2001.
18. F. Pottier. Type inference in the presence of subtyping: from theory to practice. PhD thesis, Université Paris 7, 1998.
19. T. Priesnitz. Subtype Satisfiability and Entailment. PhD thesis, Saarland University, 2004.
20. G. S. Smith. Principal type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23 (2):197–226, 1994.
21. Z. Su, A. Aiken, J. Niehren, T. Priesnitz, and R. Treinen. The firstorder theory of subtyping constraints. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’02, pages 203–216. ACM, 2002.
22. V. Trifonov and S. Smith. Subtyping constrained types. In R. Cousot and D. A. Schmidt, editors, Static Analysis, volume 1145 of Lecture Notes in Computer Science, pages 349–365. Springer Berlin Heidelberg, 1996.
23. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and computation, 115(1):38–94, 1994.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

      • Language types

        • Functional languages

• Theory of computation

  • Semantics and reasoning

    • Program constructs