Yudai Tanabe

Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficiency problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop \lambdaC^∀_mp, which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present \lambdaS^∀_mp, a space-efficient version of \lambdaC^∀_mp, and prove that \lambdaS^∀_mp programs can be executed in a space-efficient manner and that translation from \lambdaC^∀_mp to \lambdaS^∀_mp is type- and semantics-preserving.

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 _{}textrm{VL}}\\λ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 _{}textrm{VL}}\\λVLalong 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.

While modern software development heavily uses versioned packages, programming languages rarely support the concept of versions in their semantics, which makes software updates more bulky and unsafe. This paper proposes a programming language that intrinsically supports versions. The main goals are to design core language features to support multiple versions in one program and establish a proper notion of type safety with those features. The proposed core calculus, called Lambda VL, has versioned values, each containing different values under different versions. We show the construction of the type system as an extension of coeffect calculus by mapping versions to computational resources. The type system guarantees the existence of a valid combination of versions for a program. The calculus enables programming languages to use multiple versions of a package within a program. It will serve as a basis for designing advanced language features like module systems and semantic versioning.