[ICFP24] Contextual Typing

Contextual Typing (Video, ICFP 2024) Xu Xue and Bruno C. d. S. Oliveira (University of Hong Kong, China; University of Hong Kong, China) Abstract: Bidirectional typing is a simple, lightweight approach to type inference that propagates known type information during typing, and can scale up to many different type systems and features. It typically only requires a reasonable amount of annotations and eliminates the need for many obvious annotations. Nonetheless the power of inference is still limited, and complications arise in the presence of more complex features. In this paper we present a generalization of bidirectional typing called contextual typing. In contextual typing not only known type information is propagated during typing, but also other known information about the surrounding context of a term. This information can be of various forms, such as other terms or record labels. Due to this richer notion of contextual information, less annotations are needed, while the approach remains lightweight and scalable. For type systems with subtyping, contextual typing subsumption is also more expressive than subsumption with bidirectional typing, since partially known contextual information can be exploited. To aid specifying type systems with contextual typing, we introduce Quantitative Type Assignment Systems (QTASs). A QTAS quantifies the amount of type information that a term needs in order to type check using counters. Thus, a counter in a QTAS generalizes modes in traditional bidirectional typing, which can only model an all (checking mode) or nothing (inference mode) approach. QTASs enable precise guidelines for annotatability of contextual type systems formalized as a theorem. We illustrate contextual typing first on a simply typed lambda calculus, and then on a richer calculus with subtyping, intersection types, records and overloading. All the metatheory is formalized in the Agda theorem prover. Article: https://doi.org/10.1145/3674655 Supplementary archive: https://doi.org/10.5281/zenodo.11429428 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0009-0008-2165-3330, https://orcid.org/0000-0002-1846-7210 Video Tags: Bidirectional Typing, Type Inference, icfp24main-p93-p, doi:10.1145/3674655, doi:10.5281/zenodo.11429428, orcid:0009-0008-2165-3330, orcid:0000-0002-1846-7210, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2024 conference, September 2–7, 2024, https://icfp24.sigplan.org/ Sponsored by ACM SIGPLAN,