2026-07-22T01:57:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18227 2024-03-06T11:01:26Z ddc:004 open_access

Dependent Merges and First-Class Environments Tan, Jinhao Oliveira, Bruno C. d. S. First-class Environments Disjointness Intersection Types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jinhao Tan and Bruno C. d. S. Oliveira 2023 Is Part Of LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2023.34 urn:nbn:de:0030-drops-182277 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.34 eng https://creativecommons.org/licenses/by/4.0/legalcode