Compilation Semantics fora Programming Language with Versions
Yudai Tanabe1), Luthfan Anshar Lubis2),
Tomoyuki Aotani3), Hidehiko Masuhara2)
1)Kyoto University, 2)Tokyo Institute of Technology, 3)Sanyo-Onoda City University

PPL2024 @ Niigata

March 7, 2024

1

Background

Update Dilemma:
Enhancements vs. Adaptation Costs[Werner’13, Bavota’15]

Intricate update process deterring
programmers from updates
FileExpl

1.0.0

Dir

findFile:…
findFile path

Error

What’swrong?

Incompatible updates
break software

2.0.0

Dir

findFile:…

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

2BackgroundOne-version-at-a-time Limitation
FileExpl

Error
findFile p
findFile p

1.0.0

Dir

findFile

Only
one onlyversion
Assuming
onecanversion
be used!

old version
new version
2.0.0

Dir

findFile

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

3[‹Programming›’22]

Programming With Versions (PWV)
Safely handle multiple versions in one client
to split updates into smaller, consistent tasks

Dir

FileExpl

1.0.0

listDir
findfile

DirIncremental updatesof part-of-codes

2.0.0

FileExpl
hash = mkHash
findFile hash^^^^Expected: 2.0.0
Found: 1.0.0
Detecting incompatible usage

Basis of this research

FP:[‹Programming›’22],

OOP: BatakJava[SLE’22]

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

4

Contribution of This Paper

PWV w/o Version Annotations
This research[‹Programming›’22]

module FileExpl wheremodule FileExpl where

main () =main () =let [str] = [getArg [()]] inlet [digest] =[{l1=…, l2=…}[str]] in
if [{l1=…, l2=…} [digest]].l1…
[listDir [curDir]].l2

Cumbersome
syntaxRequire versions
in code locations

let str = getArg () inlet digest = mkHash str in
if exist digest …
…
listDir curDir
No version
annotations!

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

5Outline
Contribution

Programming with Versions w/o Version Annotations
This research[‹Programming›’22]

vs.

•Explicit
version annotations

Version inference
incorporating implicit versions

Semantics
and Type System• Key idea:
Utilizing module versions
for expression versions• Programming in• Compilation Overview

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

6Outline
Contribution

Programming with Versions w/o Version Annotations[‹Programming›’22]

vs.
Explicit
version annotations•Semantics
and Type System

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

7

[‹Programming›’22], Versions within Semantics

Version Labels to capture version possibilities
e.g.

Multiple terms in a versioned value\hash ->
if exist hash …
\hash ->
if exist hash …

Evaluate term in a specific version

𝒍𝟏/home/yudaitnb/vl/src/file.ext

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,𝒍𝟏Compilation Semantics for a Programming Language with Versions

8[‹Programming›’22]

Type System

Type system to enforce version consistency
Welltyped?

𝟏 𝟐
𝟏Inconsistent!

Denotes available
versions of a term

because𝟏

Soundness(preservation)(progress)
Type system is based on coeffect calculi:ℓℛPCF[Brunel’14], GrMini[Orchard’19].

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

9

Outline
Contribution

Programming with Versions w/o Version Annotations
This researchvs.
Version inference
incorporating implicit versions• Key idea:
Utilizing module versions
for expression versions•Programming

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

10

Key Idea

How to Omit Version Annotations?
Q: How/Where to get the
exp-level version info w/o labels?
Available?
Consistent?
1.0.0

Dir

listDir :: …

2.0.0

Dir

import Dir

FileExpl

main () =let str = getArg () inlet digest = mkHash str in
if exist digest …
…

listDir curDir…

findFile digest…

findFile :: …

No version labels\hash ->
if exist hash …
\hash ->
if exist hash …
PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

11

Key Idea

Compilation with Implicit Versions
A. Utilizing module vers. to denote expression vers.
Functions imported throughmulti-version interface
Dir

listDir :: □𝒓 (Hash → Unit)
findFile :: □𝒔 (Hash → Unit)

import Dir

FileExpl

main () =let str = getArg () inlet digest = mkHash str in
if exist digest …
…

listDir
is available
in Dir 1.0.0

1.0.0

findFile
is available
in Dir 2.0.0

DirlistDir :: …

2.0.0

1.0.0

listDir curDir

2.0.0

findFile digest

…
…

Dir

findFile :: …

… and compiled with aninferred version

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

12

Programming invs.

: w/ Version Labels

module FileExpl wheremain () =let [str] = [getArg [()]] inlet [digest] =[mkHash [str]] inif [exist [digest]].l1 …
…
[listDir [currentDir]].l2

Cumbersome syntax

importDir

module Dir where
exist ::
{l1 :…, l2 :…}listDir ::{l1 :…, l2 :…}import Hash

importHash

module Hash where
mkHash ::{l1 :…, l2 :…}Require version
annotations

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions13

Programming invs.

: w/o Version Labels
No version annotations!

module FileExpl wheremain () =let str = getArg () inlet digest = mkHash str in
if exist digest …
…
listDir currentDir
2.0.0

Determine a version 1.0.0
by semantic analysis

importDir

importHash

module Dir where
exist :: …
listDir :: …
importHash

module Hash where
mkHash :: …

Enable refer all versions
through multi-version interfaces

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,Compilation Semantics for a Programming Language with Versions

14

Programming in

Handling Multiple Versions in One Client
module FileExpl where
main () =let str = getArg () inlet digest =ver [Hash = 2.0.0] ofmkHash str in
if exist digest
then print "Found"else error "Not found"

Expression-levelversion control
module Dir where
exist :: … mkHash …

module Hash where
mkHash :: …

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

15

Programming in

Detecting Incompatible Version Usage
module FileExpl where
main () =let str = getArg () inlet digest =ver [Hash = 2.0.0] of
mkHash str in
if exist digest
then print "Found"else error "Not found"If exist depends
1.0.0 for mkHash …
module Dir where
exist :: … mkHash …

module Hash where
mkHash :: …
Type checking failed

exist expects an argument from Hash 1.0.0,
but digest is a value from Hash 2.0.0.

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

16

Programming in

Collaboration with Compatible Version
module FileExpl where

If programmers know 1.0.0 and
2.0.0 of Hash are compatible …

main () =let str = getArg () inlet digest =ver [Dir = 2.0.0] ofmkHash str in
let exist’ = unver exist
if exist’ digest
then print "Found"else error "Not found"module Dir whereexist :: … mkHash …

module Hash wheremkHash :: …

Incorporate compatibility
into type checking

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

17

Outline
Contribution

Programming with Versions w/o Version Annotations
This researchvs.
Version inference
incorporating implicit versions• Compilation Overview
PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

18

Compilation Overview

I/O of Compilation①Inserting
Annotations

Input
VL
VLVL

②Algorithmic
Type Inference

VL
VLVL

Programs

Haskell-subset③Interface
Bundling

Interfaces

1.0.0 2.0.0

OutputMulti-version
Interface

onstraints

Next slide

How thecompiler
uses generated constraints
PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

19

Compilation Overview

Constraints“ ” represents
dependencies(Constraints)(Dependencies)

ModulenameVersion
number

“If a version label for RHS
expects a specific version, …

… then (LHS) also expects
the same version.”
PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

20

Compilation Overview

Satisfiable Constraints
onstraints

Satisfiable
Constraint
resolution

is compiledusing versionof Dir.

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

21

Compilation Overview

Unsatisfiable Constraints
onstraints

UnsatisfiablebecauseConflicting

Constraint
resolution[Error]cannot find the consistentversion for.

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions22

In the Paper
Formalization:2310.00298

Implementation
https://github.com/yudaitnb/vl

Evaluation
with case studies• Algorithmic
type & version
inference• Proof ofsoundness wrt
semantics

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

23Summary
Contribution

Programming With Versions w/o version annotations
This research[‹Programming›’22]

vs.
Explicit
version annotations

Version inference

incorporating implicit versions

PPL2024 @ Niigata

March 7, 2024

Yudai Tanabe,

Compilation Semantics for a Programming Language with Versions

24