Timezone: »
Optionally typed dynamic languages can permit multiple valid type assignments. When this happens, developers can prefer one valid type assignment over another because it better reflects how they think about the program and the problem it solves. Natural type inference (NTI) uses natural language text within source code, such as identifiers, to help choose valid programming language types. A growing body of techniques has been proposed for NTI. These techniques predict types; they seek to return natural type assignments (assignments that reflect developer preferences) while striving for correctness. They are empirically effective, but they are not sound by construction: they do not leverage programming language theory to formalize their algorithms and show correctness and termination. Filling this foundational gap is the purpose of this paper. We are the first to present a detailed algorithm for NTI that is validated with theorems and proofs. Valid type assignments obey logical constraints arising from type rules; natural type assignments obey natural constraints arising from the natural language text associated with a variable and its uses.The core intuition of this work is that logical and natural constraints can interact to speed finding a type valuation that 1. type checks (satisfies the logical constraints) and 2. is most natural.We formulate NTI as a joint optimization problem. To do this, we define a numerical relaxation over boolean logical constraints that give us a condition that we treat as a hard constraint, while simultaneously we minimize distance from natural constraints, which we treat as soft constraints for our optimization problem. Our main result, the first formal proof of soundness for natural type inference, is that our algorithm always terminates, either with an error or with a tuple that is guaranteed to be a type signature for its input.
Author Information
Eirini V. Pandi (University of Edinburgh)
Earl Barr (University College London)
Andrew Gordon (Microsoft Research)
Andy Gordon leads [Calc Intelligence](https://aka.ms/CalcIntel) at Microsoft Research, bringing intelligence to end-user programming, especially spreadsheets. Calc Intelligence partners closely with Microsoft Excel: features such as LAMBDA and Calc.ts, arising from their mission to enhance Excel as a programming language, ship now in production to many millions of customers.
Charles Sutton (Google)
More from the Same Authors
-
2021 : Type Inference as Optimization - Eirene V. Pandi »
AIPLANS 2021 · Eirini V. Pandi -
2021 Poster: Learning Semantic Representations to Verify Hardware Designs »
Shobha Vasudevan · Wenjie (Joe) Jiang · David Bieber · Rishabh Singh · hamid shojaei · C. Richard Ho · Charles Sutton -
2021 Poster: A Bayesian-Symbolic Approach to Reasoning and Learning in Intuitive Physics »
Kai Xu · Akash Srivastava · Dan Gutfreund · Felix Sosa · Tomer Ullman · Josh Tenenbaum · Charles Sutton -
2020 : closing talk »
Augustus Odena · Charles Sutton -
2020 : Panel »
Augustus Odena · Charles Sutton · Roopsha Samanta · Xinyun Chen · Elena Glassman -
2020 : Satish Chandra Talk »
Satish Chandra · Augustus Odena · Charles Sutton -
2020 : Spotlight Session 2 »
Augustus Odena · Kensen Shi · David Bieber · Ferran Alet · Charles Sutton · Roshni Iyer -
2020 : Spotlight Session 1 »
Augustus Odena · Maxwell Nye · Disha Shrivastava · Mayank Agarwal · Vincent J Hellendoorn · Charles Sutton -
2020 Workshop: Workshop on Computer Assisted Programming (CAP) »
Augustus Odena · Charles Sutton · Nadia Polikarpova · Josh Tenenbaum · Armando Solar-Lezama · Isil Dillig -
2020 Poster: Learning to Execute Programs with Instruction Pointer Attention Graph Neural Networks »
David Bieber · Charles Sutton · Hugo Larochelle · Danny Tarlow -
2020 Poster: Learning Discrete Energy-based Models via Auxiliary-variable Local Exploration »
Hanjun Dai · Rishabh Singh · Bo Dai · Charles Sutton · Dale Schuurmans -
2018 : Panel on research process »
Zachary Lipton · Charles Sutton · Finale Doshi-Velez · Hanna Wallach · Suchi Saria · Rich Caruana · Thomas Rainforth -
2018 : Charles Sutton »
Charles Sutton -
2018 Poster: HOUDINI: Lifelong Learning as Program Synthesis »
Lazar Valkov · Dipak Chaudhari · Akash Srivastava · Charles Sutton · Swarat Chaudhuri -
2017 Poster: VEEGAN: Reducing Mode Collapse in GANs using Implicit Variational Learning »
Akash Srivastava · Lazar Valkov · Chris Russell · Michael Gutmann · Charles Sutton -
2016 Workshop: Towards an Artificial Intelligence for Data Science »
Charles Sutton · James Geddes · Zoubin Ghahramani · Padhraic Smyth · Chris Williams -
2015 Poster: Latent Bayesian melding for integrating individual and population models »
Mingjun Zhong · Nigel Goddard · Charles Sutton -
2015 Spotlight: Latent Bayesian melding for integrating individual and population models »
Mingjun Zhong · Nigel Goddard · Charles Sutton -
2014 Poster: Semi-Separable Hamiltonian Monte Carlo for Inference in Bayesian Hierarchical Models »
Yichuan Zhang · Charles Sutton -
2014 Poster: Signal Aggregate Constraints in Additive Factorial HMMs, with Application to Energy Disaggregation »
Mingjun Zhong · Nigel Goddard · Charles Sutton -
2012 Poster: Continuous Relaxations for Discrete Hamiltonian Monte Carlo »
Zoubin Ghahramani · Yichuan Zhang · Charles Sutton · Amos Storkey -
2012 Spotlight: Continuous Relaxations for Discrete Hamiltonian Monte Carlo »
Zoubin Ghahramani · Yichuan Zhang · Charles Sutton · Amos Storkey -
2011 Poster: Quasi-Newton Methods for Markov Chain Monte Carlo »
Yichuan Zhang · Charles Sutton