A Fix for Dynamic Scope
Ravi Chugh
ML 2013
[ paper
]
When the semantics for pure lambda-terms is defined with dynamic scope, instead of the more conventional lexical scope, recursive computations can be expressed directly without the need for a fix operator, either as a native function or as a lambda-term. In this report, we sketch the design of a type system for a dynamically scoped lambda-calculus based on a simple idea called open types. An open function type declares assumptions about the types of free variables in the function body, and these assumptions must be satisfied in every context where the function is used. We then discuss how the same mechanism can describe well-typed recursive computations in the lexically scoped lambda-calculus extended with references. In this setting, recursion can be achieved without a fix operator using a well-known encoding called "backpatching." But whereas the typical encoding requires that the reference to a recursive function be initialized to a dummy function of the desired type, open function types allow type checking the backpatching pattern without such initialization, an idiom that appears in scripting languages like JavaScript.
Type Inference with Run-time Logs
Ravi Chugh, Ranjit Jhala, and Sorin Lerner
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.