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 E_i, with first-class environments. The main novelty of the E_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 E_i any type can act as a context (i.e. an environment type) and contexts are simply types. Furthermore, because E_i supports subtyping, there is a natural notion of context subtyping. There are two important ideas in E_i that generalize and are inspired by existing notions in the literature. The E_i calculus borrows disjoint intersection types and a merge operator, used in E_i to model contexts and environments, from the λ_i calculus. However, unlike the merges in λ_i, the merges in E_i can depend on previous components of a merge. From implicit calculi, the E_i calculus borrows the notion of a query, which allows type-based lookups on environments. In particular, queries are key to the ability of E_i to reify the current environment, or some parts of it. We prove the determinism and type soundness of E_i, and show that E_i can encode all well-typed λ_i programs.