Constraint-Based Type Inference for FreezeML

作     者：Emrich, Frank Stolarek, Jan Cheney, James Lindley, Sam 

作者机构：Lodz Univ Technol Lodz Poland Alan Turing Inst London England Univ Edinburgh Edinburgh Midlothian Scotland 

出 版 物：《PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL》 (Proc. ACM Program. Lang.)

年 卷 期：2022年第6卷第ICFP期

页      面：570–595页

核心收录：

基　　金：ERC Consolidator Grant Skye ISCF Metrology Fellowship - UK government's Department for Business, Energy and Industrial Strategy (BEIS) UKRI Future Leaders Fellowship lEffect Handler Oriented Programmingz [MR/T043830/1] European Research Council (ERC) Funding Source: European Research Council (ERC) 

主　　题：first-class polymorphism type inference impredicative types constraints 

摘      要：FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to AlgorithmW. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Remy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.