Type Inference with Run-time Logs

Ravi Chugh, Sorin Lerner, and Ranjit Jhala
STOP 2011 [ paper | slides ]

Gradual type systems offer the possibility of migrating programs in dynamically-typed languages to more statically-typed ones. There is little evidence yet that large, real-world dynamically-typed programs can be migrated with a large degree of automation. Unfortunately, since these systems typically lack principal types, fully automatic type inference is beyond reach. To combat this challenge, we propose using logs from run-time executions to assist inference. As a first step, in this paper we study how to use run-time logs to improve the efficiency of a type inference algorithm for a small language with first-order functions, records, parametric polymorphism, subtyping, and bounded quantification. Handling more expressive features in order to scale up to gradual type systems for dynamic languages is left to future work.