A Case for First-Class Environments

Formalizations of programming languages typically adopt the substitution model from the lambda calculus. However, substitution creates notorious complications for reasoning and implementation. Furthermore, it is disconnected from practical implementations, which normally adopt environments and closures. In this paper we advocate for formalizing programming languages using a novel style of small-step environment-based semantics , which avoids substitution and is closer to implementations. We present a call-by-value statically typed calculus, called <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> , using our small-step environment semantics. With our alternative environment semantics programming language constructs for first-class environments arise naturally, without creating significant additional complexity. Therefore, <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> also adopts first-class environments, adding expressive power that is not available in conventional lambda calculi. <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> is a conservative extension of the call-by-value Simply Typed Lambda Calculus (STLC), and employs de Bruijn indices for its formalization, which fit naturally with the environment-based semantics. Reasoning about <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> is simple, and in many cases simpler than reasoning about the traditional STLC. We show an abstract machine that implements the semantics of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> , and has an easy correctness proof. We also extend <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> with references. We show that <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msub> <mml:mtext>λ</mml:mtext> <mml:mi mathvariant="normal">E</mml:mi> </mml:msub> </mml:math> can model a simple form of first-class modules, and suggest using first-class environments as an alternative to objects for modelling capabilities. All technical results are formalized in the Coq proof assistant. In summary, our work shows that the small-step environment semantics that we adopt has three main and orthogonal benefits: 1) it simplifies the notorious binding problem in formalizations and proof assistants; 2) it is closer to implementations; and 3) additional expressive power is obtained from first-class environments almost for free.