This program is tentative and subject to change.
\emph{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 eliminates the need for many obvious annotations, while typically requiring only a reasonable amount of 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 \emph{contextual typing}. In contextual typing not only known type information is propagated during typing, but also other known information about the \emph{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.
This program is tentative and subject to change.
Thu 5 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Refinement Types, Type InferenceICFP Papers and Events / JFP First Papers | ||
10:30 18mTalk | The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures ICFP Papers and Events | ||
10:48 18mTalk | Contextual Typing ICFP Papers and Events | ||
11:06 18mTalk | Synchronous Programming with Refinement Types ICFP Papers and Events Jiawei Chen University of Michigan - Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Shayan Jalili University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Nicholas Wohlfeil University of Michigan - Ann Arbor, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor | ||
11:24 18mTalk | Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP Papers and Events | ||
11:42 18mTalk | Trace contractsJFP First Paper JFP First Papers DOI |