Aarhus University Seal

Polymorphic types and effects with Boolean unification

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

We present a simple, practical, and expressive type and effect system based on Boolean constraints. The effect system extends the Hindley-Milner type system, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support type inference by extending Algorithm W with Boolean unification based on the successive variable elimination algorithm. We implement the type and effect system in the Flix programming language. We perform an in-depth evaluation on the impact of Boolean unification on type inference time and end-to-end compilation time. While the computational complexity of Boolean unification is NP-hard, the experimental results demonstrate that it works well in practice. We find that the impact on type inference time is on average a 1.4x slowdown and the overall impact on end-to-end compilation time is a 1.1x slowdown.

Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
Number of pages29
Volume4
PublisherAssociation for Computing Machinery
Publication year13 Nov 2020
EditionOOPSLA
DOIs
Publication statusPublished - 13 Nov 2020
SeriesACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications

Bibliographical note

Publisher Copyright:
© 2020 Owner/Author.

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

    Research areas

  • Boolean unification, polymorphic types and effects, type inference

See relations at Aarhus University Citationformats

ID: 215997179