{"ID":2851175,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.20532","arxiv_id":"2510.20532","title":"Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism","abstract":"Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect systems did not yet gain widespread adoption. One reason for this is that type-and-effect systems are more complex and the existing inference algorithms make compromises between expressiveness, intuitiveness, and decidability. In this work, we present an effect inference algorithm for a type-and-effect system with subtyping, expressive higher-rank polymorphism, and intuitive set-like semantics of effects. In order to deal with scoping issues of higher-rank polymorphism, we delay solving of effect constraints by transforming them into formulae of propositional logic. We prove soundness and completeness of our algorithm with respect to a declarative type-and-effect system. All the presented results have been formalized in the Rocq proof assistant, and the algorithm has been successfully implemented in a realistic programming language.","short_abstract":"Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect systems did not yet gain widespread adoption....","url_abs":"https://arxiv.org/abs/2510.20532","url_pdf":"https://arxiv.org/pdf/2510.20532v1","authors":"[\"Patrycja Balik\",\"Szymon Jędras\",\"Piotr Polesiuk\"]","published":"2025-10-23T13:16:17Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[\"Generative Adversarial Network\"]","has_code":false}