`

Timezone: »

 
Type Inference as Optimization
Eirini V. Pandi · Earl Barr · Andrew Gordon · Charles Sutton

@ None
in Advances in Programming Languages and Neurosymbolic Systems (AIPLANS) »
Event URL: https://openreview.net/forum?id=yHYZaQ0Zvml »

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