Bidirectional Typing with Freezing, Skeletons, and Ghosts
Programming Languages
Summary
The authors introduce Fresco, a new way to guess types in programming languages that lets information flow both ways between functions and their inputs. Traditional methods usually only let information flow one way, which makes it hard to figure out certain complex types called first-class polymorphism. Fresco uses a system with 'skeletons' and 'ghosts' to handle unknown types and lets users control how information flows. They show Fresco works well by providing a clear set of rules and an algorithm that is both correct and complete, plus a prototype that can infer even more advanced type effects.
Authors
Wenhao Tang, Shengyi Jiang, Aghilas Y. Boussaa, Sam Lindley, Bruno C. d. S. Oliveira
Abstract
Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically from functions to arguments, which is insufficient to infer first-class polymorphism. Existing work on improving information flow either has limited support for mixed information flow or requires ad hoc mechanisms that harm predictability. We propose Fresco, a novel bidirectional type inference approach to first-class polymorphism. Fresco enables local type information to flow back and forth between functions and arguments via skeletons, with ghosts representing unknown type information, and allows users to customise the direction of information flow by freezing. The flexible information flow of Fresco enables expressive and predictable inference for first-class polymorphism. We provide a declarative specification for Fresco, a simple type inference algorithm that is sound and complete with respect to the declarative system, and a prototype implementation that further generalises Fresco to infer modal effect types.