A Modular Type Reconstruction Algorithm

• Published in: ACM transactions on computational logic 2018-12, Vol.19 (4), p.1-43
• Main Author: Rabe, Florian
• Format: Article
• Language: English
• ISSN: 1529-3785; 1557-945X
• DOI: 10.1145/3234693

M mt is a framework for designing and implementing formal systems in a way that systematically abstracts from theoretical and practical aspects of their type of theoretical and logical foundations. Thus, definitions, theorems, and algorithms can be stated independently of the foundation, and language designers can focus on the essentials of a particular foundation and inherit a large-scale implementation from M mt at low cost. Going beyond the similarly motivated approach of meta-logical frameworks, M mt does not even commit to a particular meta-logic—that makes M mt level results harder to obtain but also more general. We present one such result: a type reconstruction algorithm that realizes the foundation-independent aspects generically relative to a set of rules that supply the foundation-specific knowledge. Maybe surprisingly, we see that the former covers most of the algorithm, including the most difficult details. Thus, we can easily instantiate our algorithm with rule sets for several important language features including, e.g., dependent function types. Moreover, our design is modular such that we obtain a type reconstruction algorithm for any combination of these features.