Thu 24 Oct 2024 16:40 - 17:00 at IBR West - Types and Gradual Typing 1 Chair(s): Fabian Muehlboeck

Refinement types combine SMT decidable constraints with a compositional, syntax-directed type system to provide a convenient way to statically and automatically check properties of programs. However, when type checking fails, programmers must use cryptic error messages that, at best, point out the code location where a subtyping constraint failed to determine the root cause of the failure. In this paper, we introduce refinement type refutations, a new approach to explaining why refinement type checking fails, which mirrors the compositional way in which refinement type checking is carried out. First, we show how to systematically transform standard bidirectional type checking rules to obtain refutations. Second, we extend the approach to account for global constraint-based refinement inference via the notion of a must-instantiation: a set of concrete inhabitants of the types of subterms that suffice to demonstrate why typing fails. Third, we implement our method in HayStack—an extension to LiqidHaskell which automatically finds type-refutations when refinement type checking fails, and helps users understand refutations via an interactive user-interface. Finally, we present an empirical evaluation of HayStack using the regression benchmark-set of LiqidHaskell, and the benchmark set of G2, a previous method that searches for (non-compositional) counterexample traces by symbolically executing Haskell source. We show that HayStack can find refutations for 99.7% of benchmarks, including those with complex typing constructs (e.g., abstract and bounded refinements, and reflection), and does so, an order of magnitude faster than G2.

Thu 24 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
Types and Gradual Typing 1OOPSLA 2024 at IBR West
Chair(s): Fabian Muehlboeck Australian National University
16:00
20m
Talk
Intensional Functions
OOPSLA 2024
Zachary Palmer Swarthmore College, Nathaniel Wesley Filardo Microsoft, Ke Wu Johns Hopkins University
DOI
16:20
20m
Talk
Qualifying System F-sub
OOPSLA 2024
Edward Lee University of Waterloo, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, James You University of Waterloo, Kavin Satheeskumar University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen
DOI
16:40
20m
Talk
Refinement Type Refutations
OOPSLA 2024
Robin Webbers Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Ranjit Jhala UCSD
DOI
17:00
20m
Talk
Type Inference Logics
OOPSLA 2024
Denis Carnier KU Leuven, François Pottier Inria, Steven Keuchel Vrije Universiteit Brussel
DOI
17:20
20m
Talk
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs (SIGPLAN)
OOPSLA 2024
Guannan Wei Inria/ENS; Tufts University, Oliver Bračevac EPFL, LAMP, Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
Link to publication