Dependent Merges and First-Class Environments

In most programming languages a (runtime) environment stores all the definitions that are available to programmers. Typically, environments are a meta-level notion, used only conceptually or internally in the implementation of programming languages. Only a few programming languages allow environments to be first-class values, which can be manipulated directly in programs. Although there is some research on calculi with first-class environments for statically typed programming languages, these calculi typically have significant restrictions. In this paper we propose a statically typed calculus, called ?_i, with first-class environments. The main novelty of the ?_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them. Such operators include: reification of the current environment, environment concatenation, environment restriction, and reflection mechanisms for running computations under a given environment. In ?_i any type can act as a context (i.e. an environment type) and contexts are simply types. Furthermore, because ?_i supports subtyping, there is a natural notion of context subtyping. There are two important ideas in ?_i that generalize and are inspired by existing notions in the literature. The ?_i calculus borrows disjoint intersection types and a merge operator, used in ?_i to model contexts and environments, from the ?_i calculus. However, unlike the merges in ?_i, the merges in ?_i can depend on previous components of a merge. From implicit calculi, the ?_i calculus borrows the notion of a query, which allows type-based lookups on environments. In particular, queries are key to the ability of ?_i to reify the current environment, or some parts of it. We prove the determinism and type soundness of ?_i, and show that ?_i can encode all well-typed ?_i programs