Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized $\lambda_{\mathrm{VL}}$, a core calculus for programming with versions, but it has not been integrated into practical programming languages. In this paper, we propose VL, a Haskell-subset surface language for $\lambda_{\mathrm{VL}}$ along with its compilation method. We formally describe the core part of the VL compiler, which translates from the surface language to the core language by leveraging Girard's translation, soundly infers the consistent version of expressions along with their types, and generates a multi-version interface by bundling specific-version interfaces. We conduct a case study to show how VL supports practical software evolution scenarios and discuss the method's scalability.

翻译：版本化编程是一种允许程序使用同一模块多个版本的范式，程序员可选择性调用单个模块旧版和新版中的函数。先前的研究形式化了λ_VL（一种用于版本化编程的核心演算），但尚未将其集成到实际编程语言中。本文提出VL——面向λ_VL的Haskell子集表层语言及其编译方法。我们形式化描述了VL编译器核心部分：通过Girard变换将表层语言翻译为核心语言，稳健推断表达式的一致版本及其类型，并通过绑定特定版本接口生成多版本接口。通过案例研究展示VL如何支持实际软件演进场景，并讨论该方法可扩展性。