¶Abstract

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

¶BibTeX

@InProceedings{tan_et_al:LIPIcs.ECOOP.2023.34,
  author =	{Tan, Jinhao and Oliveira, Bruno C. d. S.},
  title =	{{Dependent Merges and First-Class Environments}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{34:1--34:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18227},
  URN =		{urn:nbn:de:0030-drops-182277},
  doi =		{10.4230/LIPIcs.ECOOP.2023.34},
  annote =	{Keywords: First-class Environments, Disjointness, Intersection Types}
}