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

APLAS2023 @ Taipei

November 27, 2023

1

Background

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

Intricate updating processes are deterring
programmers from updates.
FileExpl

1.0.0

Dir

findFile:…
findFile path

Error

Incompatible updates
may break software.

2.0.0

Dir

findFile:…

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

2

Background

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

Intricate updating processes are deterring
programmers from updates.
FileExpl

1.0.0

Dir

findFile:…
findFile pathWhat’swrong?

Error

Incompatible updates
may break software.

2.0.0

Indirect dependencies
complicate tracing errors.

findFile:…

APLAS2023 @ Taipei

November 27, 2023

Dir

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

3

BackgroundOne-version-at-a-time Limitation
FileExpl

1.0.0

Error
findFile p
findFile p

DirfindFile

Only
one only
versionAssuming
one
canversion
be used!

old version
new version
2.0.0

Dir

findFile

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

4

Background[‹Programming›’22]

Programming with Versions (PwV)
Goal
FileExpl• Handling multiple versions in one client• Detecting incompatible version usage

Dir
1.0.0

listDir
findfile

Dir

FileExpl
hash = mkHash
findFile hash
^^^^

2.0.0

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

5

Background

Why Language-based Approach?
Split huge update into
Benefitsmaller and consistent tasks
FileExpl

Dir
1.0.0

listDir
findfile
Enable updates
incrementally

Dir
2.0.0

FileExpl
hash = mkHash
findFile hash^^^^[Warn] Incompatible

Expected: 2.0.0
Found: 1.0.0

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

6

Background

Existing PwV Languages• Handling multiple versions in one client• Detecting incompatible version usage

Goal

Dir

FileExpl

1.0.0

listDir
findfile

FileExpl
hash = mkHash
findFile hash
^^^^

Dir
2.0.0

Basis of this research (next slide)

FP:[‹Programming›’22],

OOP: BatakJava[SLE’22]

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

7

Contribution

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 [currentDir]].l2

Cumbersome
syntaxRequire versions
in code locations

let str = getArg () inlet digest = mkHash str in
if exist digest …
…
listDir currentDir
No version
annotations& usual syntax!

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

8Rest of the Talk
Contribution

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

IR

vs.

•

Explicit
version annotations

Version inference
incorporating implicit versions

Semantics
and Type System• Key idea:
Multi-version interface•
Programming• Compilation• Implementation & Evaluation• Future work

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

9

Outline
Contribution

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

vs.
Explicit
version annotations•

Semantics
and Type System

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

10

Background[‹Programming›’22], Versions within Semantics

Version Labels to capture multiple version possibilities
Multiple terms in a versioned value

Evaluate term in a specific version\hash ->
if exist hash …
\hash ->
if exist hash …

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

Versionnumberi.e.

APLAS2023 @ Taipei

November 27, 2023

𝒍𝟏

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

11

Background[‹Programming›’22]

Type System

Type system to enforce version consistency
𝟏
𝟏 𝟐

Welltyped?

Types are tagged withversion resourcesthat denotes available versions of a term

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

12

Background[‹Programming›’22]

Type System

Type system to enforce version consistency
Welltyped?

𝟏
𝟏 𝟐

Capture shared version resource
to enforce consistent version usage

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

13

Background[‹Programming›’22]

Type System

Type system to enforce version consistency
Welltyped?

𝟏
𝟏 𝟐

Type error

becauseAPLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

14

Background[‹Programming›’22]

Type System

Type system to enforce version consistency
Welltyped?

𝟏
𝟏 𝟐

Type error

becauseType soundness(preservation)(progress)

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

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

15

Outline
Contribution

Programming with Versions w/o Version Annotations
This researchIRvs.
Version inference
incorporating implicit versions• Key idea:
Multi-version interface•
Programming• Compilation

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

16

Contribution

Version Inference w/o Version Annotations
Q: How/Where do we get the
exp-level version information
w/o version labels?

import Dir
main () =Available?
Consistent?
1.0.0

Dir

listDir :: …

2.0.0

FileExpl

Dir

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

listDir currentDir…

findFile digest…

findFile :: …

No version labels
as of usual functional language\hash ->
if exist hash …
\hash ->
if exist hash …
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

17

Contribution

Key Ideas
A: Version tagging only at module boundaries
Multi-version interface

indicating availability for each expression

Dirimport Dir
Constraints

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

FileExpl

listDir mainfindFile
() =
let
str
= getArg () inis available let isavailable
digest = mkHash str indigest…
in Dir 1.0.0 if exist
in Dir2.0.0…

listDir currentDir
1.0.0

Dir

listDir :: …

2.0.0

Dir

findFile :: …

…

findFile digest…
… and it is automaticallygeneratedfrom the interfaces of each version
with constraints.

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

18

Contribution

Key Ideas
A: Version tagging only at module boundaries
Importing external variables throughmulti-version interface …
Dir

import Dir

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

FileExpl

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

1.0.0

Dir

listDir :: …

2.0.0

Dir

findFile :: …

1.0.0

listDir currentDir

2.0.0

findFile digest…
…

… and infer a consistent version label.
Constraints

APLAS2023 @ Taipei

November 27, 2023

listDir
is available
in Dir 1.0.0

findFile
is available
in Dir 2.0.0

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

19

Programmingvs.

w/ version labels

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

Cumbersome syntax
for handling versioned values

importDir

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

importHash

module Hash where
mkHash ::{l1 :…, l2 :…}Require labelsin code locations

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

20

Programming: Surface Language for
w/o version labels

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

Determine a version
by semantic analysis

importDir

importHash

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

module Hash where
mkHash :: …

import throughmulti-version interfaces

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

21

Programming

Type Checking
Goal• Handling multiple versions in one client• Detecting incompatible version usage

module FileExpl where
main () =let str = getArg () inlet digest =mkHash str in
if exist digest
then print "Found"else error "Not found"module Dir where
exist :: … mkHash …
Use 1.0.0
for mkHash
Use 2.0.0
for 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.
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

22

Programming

Version Control Terms
Goal• Handling multiple versions in one client• Detecting incompatible version usage

module FileExpl wheremodule Dir where
exist :: … mkHash …

main () =let str = getArg () inlet digest =unversion(mkHash str) in
if exist digest
then print "Found"else error "Not found"••

Use 1.0.0
for mkHash
Use 2.0.0
for mkHash

module Hash where
mkHash :: …

Version control terms

eases ’s constraints
specifies ’s versions𝒊𝒊

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

23

Compilation Overview

In-/Out-put of Compilation

Contribution

Programming with versions
w/o version annotations
Input

OutputSingle-module multi-version
compilation for Dir
Dir

VLDir
VL
VL

Multi-version
Interface(Haskell-subset)

1.0.0 2.0.0
Versions

Constraints(external to the language)

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

24Compilation Overview

IR:

Programming with versions
via
w/o version annotations

Difference between
Input

IR:

A version-label-free variant of 𝜆andOutputDir(Terms)

VLDir
VL
VL
(patterns)

Exclude label-dependent
InterfacetermsVersion-independentfrom(Haskell-subset)(Types)(Versionresources)

1.0.0 2.0.0
Adding type variable
Versions
for version resource(external to the language)

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

Constraints

25

Compilation Overview① Inserting Annotations
Input
Haskell-subset

2.0.0
1.0.0
Dir

listDir’ VL=VLVL\s -> listDir s

Coeffect calculus

Versionwise

2.0.0
1.0.0
Dir

listDir’ = VLVLVL\[s] -> listDir [s]Treat arguments asversioned values …

… and capture theirversion resources bypromoted patterns
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

26

Compilation Overview② Version Inference
Programs

Interfaces

2.0.0
1.0.0
Dir

listDir’ = VLVLVL\[s] -> listDir [s]According to the inserted
annotations [ _ ] ...

1.0.0
𝜶𝟏

𝜷𝟏

Versionwise

2.0.0
𝜶𝟐

𝜷𝟐

Collects constraints
indicating version consistency
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

27

Compilation Overview③ Interface Bundling
OutputInterfaces

Multi-version interface

1.0.0
𝜶𝟏

𝜶

𝜷𝟏

𝜷

2.0.0
𝜶𝟐

𝜷𝟐

Incorporate dependencies
on specific versions

into constraints using out-of-language versions
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

28

Compilation Overview

In-/Out-put of Compilation①Inserting
Annotations

Input
VL
VL
VL

②Algorithmic
Type Inference

VL
VL
VL

Programs

Haskell-subset③Interface
Bundling

Interfaces

1.0.0 2.0.0

OutputMulti-version
Interface

Constraints

Next slideHowuses generated constraints

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

29

The

Core Language

Constraints“ ” representing
dependencies(Constraints)(Dependencies)

ModulenameVersionnumber

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

… then (LHS) also expects
the same version.”
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

30

Constraint Resolution

Satisfiable Constraints
Constraints

Satisfiable
Constraint
resolution

is compiledusing version
of Dir.

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

31

Constraint Resolution

Unsatisfiable Constraints
Constraints

UnsatisfiablebecauseConflicting

Constraint
resolution[Error]cannot find the consistentversion for.

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

32

Outline
Contribution

Programming with Versions w/o Version Annotations
This researchIRvs.
Version inference
incorporating implicit versions• Implementation & Evaluation• Future work
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

33

Implementation

The VL Compiler• Implemented on
GHC 9.2.4
https://github.com/yudaitnb/vl

Compiler
Pipeline

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

34

Implementation

The VL Compiler• Input and output
are Haskell ASTs

Compiler
Pipeline

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

35

Implementation

The VL Compiler• Resolve constraints
using Z3 [De Moura’08]

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

Compiler
Pipeline36Implementation

The VL Compiler• Implemented on
GHC 9.2.4
https://github.com/yudaitnb/vl• Both in-/out-put
are Haskell ASTs
(subset)• Resolve constraints
using Z3 [De Moura’08]

Compiler
Pipeline

Evaluations (next slides)

1. Case study to confirm
2. Compiler performanceachieving PwV benefits

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

37

Evaluation

1. Case Study
achieves our goals:
Handling two versions in one client
Detecting inconsistent version
Setting• Port hmatrix to Matrix• Simulating breaking updates in
Main

MatrixMatrix

List
Data.List

base (Haskell standard library)https://hackage.haskell.org/package/hmatrix-0.20.2
https://hackage.haskell.org/package/hmatrix-0.20.2/changelog

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

38

Evaluation

2. Compiler Performance
Benchmark setting
Ubuntu 22.04
Ryzen 7950X
Z3 version 4.12.2

Main

Importing#mod-times
nesteddependencies#ver
Each module
has #ver versions~500LOC/ mod verAPLAS2023 @ Taipei

November 27, 2023

#mod

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

39

Evaluation

2. Compiler Performance
Benchmark setting
Ubuntu 22.04
Ryzen 7950X
Z3 version 4.12.2

Main

Not
scalable

Importing#mod-times
nesteddependencies#ver
Each module
has #ver versions~500LOC/ mod ver… but existing techniques can
optimize the constraint resolution(out-of-scope, short discussion in the paper)

APLAS2023 @ Taipei

November 27, 2023

#mod

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

40

Future Work

Further Compatibility Support
Supported changes

Unsupported changes• Add/delete definitions• Semantically incompatible changes• Type changes(w/o interface-level changes)• Add/Delete imports(w/o cyclic dependencies)

BatakJava[SLE’22]••

Add/delete methods
Class inheritance changes•

Semantically compatible changes(Currently unsupported features)• Data types• Type classes• License• Visibility

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

41

Future Work

Further Compatibility Support
Supported changes

Unsupported changes• Add/delete definitions• Semantically incompatible changes• Type changes(w/o interface-level changes)• Add/Delete imports[SLE’22]••

Semantically compatible changes(Currently unsupported features)• Data types• Type classes• License• Visibility(w/o cyclic dependencies)

BatakJava•

Add/delete methods
Class inheritance changes

Idea: Integrating PwV into record calculus[Ohori’95]?

APLAS2023 @ Taipei

November 27, 2023,⋅

Allow different types
across versions unlike
🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

42

Summary

Contribution

Programming with versions
w/o version annotations
This research[‹Programming›’22]

IRvs.
Explicit
version annotations

Version inference using
Multi-version interface

incorporating implicit versions

Implementationon

GHC with Z3

https://github.com/yudaitnb/vl

Preprint
Formalization
Proof of soundness

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

43

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

44

Background

Dependency Hell

• Indirect dependencies complicate updates
Dir
App
Conflict

Only help externally

Dir
Hash

Stack

• Increasing update costs• Lead to version locking[Preston-Werner’13]• Discourage users from updates[Bavota’15]
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

45

Background

Type System

Version Resource Semiring
Coeffect calculus:

PCF[Brunel’14],

versioned values con-/de-structors[Orchard’19](version labels)… and some corresponding typing rules(security level[Orchard’19])e.g.

(exact usage[Petricek’14])
e.g.

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

46

Background

Type System

Version Awareness
Additive part: resource splitting
Splitting resources for sub judgments

app

(
⊕

Multiplication part: resource demandingpr

Requiring resources from a context⊗“ available in requires
all assumptions to be available in .”APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

47

Background

Type System

Intuition to 0 and 1 in Semiring
Both 0 and 1 indicate unavailable resources.
Treated differently only in multiplication

.

weak

der

sub
In other coeffect calculi, the semantic difference between 0 and 1 may be meaningful.
[Patriceik’14,Orchard’19]i.e.) Exact usage
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

48

Background

var

int

Type System

Typing Rules

abs
app

let

weak

der

sub
veri
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

pr

extr
ver
49

Background

Type System

Properties

Well-typed versioned substitutions(Well-typed linear
substitutions hold as well)Type-safe extractions

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

50

①TranslatetoA generalization of the originalfor linear -calculus[Girard’87][Orchard’19]
toGirard’s Translation

Inserting syntactic annotation wherea value should be treated as a versioned value
Treat arguments asversioned values …

xt s\x −> ttst

… and capture theirversion resources bypromoted patterns

Terms
Types

VLDir
VL
VL
(STLC)

VLDir
VL
VL

A
A −> AAPLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

51

②Version Inference

Constraint Generation𝒇𝒙②Algorithmic Type Inference

Variable dependencies
generated by inserted promotion

1.0.0
2.0.0

𝜶𝟏

𝜷𝟏

𝜶𝟐

𝜷𝟐

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

52

②Version Inference & ③Interface Bundling

Constraint Generation𝒇Please see the paper
for more details!

𝒙②Algorithmic Type Inference

Variable dependencies
generated by inserted promotion

𝜶

1.0.0
2.0.0

𝟏

𝜶𝟏

𝜷𝟏

𝜶𝟐

𝜷𝟐

𝜷

𝟐

③Interface Bundling

Label dependencies

generated by availability checking
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions53

② Version Inference

Algorithmic Type Inference
Allocate resource variables and collect constraints

Input

Output: Term: Typing context: Type variable kinds: Type: Constraints: Type variable kinds: Substitution

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions54

② Version Inference

Pattern Type Synthesis
Resource contexts

Input

OutputAggregate
resources by
Convert the resource
into assumption

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions55

② Version Inference

Data Structure Support• Inserting distributive combinators[Huges’21]
LC

Granule[Orchard’19,
Huges’21]• Motivation:

push : (a, b)[r] -> (a[r], b[r])push [(x, y)] = ([x], [y])pull : (a[n], b[m]) -> (a, b)[n ⊓ m]pull ([x], [y]) = [(x, y)]

How to propagate resources in-/out-side a data structure?
A versioned value of a tuple

is
ill-typed𝒓

A tuple of versioned values𝒓𝒔

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions56

③ Interface Bundling

Generate Multi-version Interface
Dir

DirInterface

Interface

1.0.0
𝜶𝟏

𝜷𝟏

𝜷
𝟏

2.0.0
𝜶𝟐

𝜶

Generated
constraints

𝟐

𝟏

𝜷𝟐

𝟏

Restriction

𝟐

All versions musthave a same typefor

𝟐

APLAS2023 @ Taipei

November 27, 2023

for

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

57

[SBV] : http://leventerkok.github.io/sbv/

Implementation

How to use SMT solver

Vectorizing Constraints
Translate constraints to symbolic lists[SBV]Label / Constraints

Symbolic lists

A

B

A

B

1.0.0
2.0.0

the

A labelindicates that-th element of a symbolic list is

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions.

58

Implementation

Version Polymorphism

Ad-hoc Polymorphism via Duplication• Rename all occurrences of external symbols• Replicate those in constraints and contexts as wellType inference

Code generation

main = g_0 x_0+ unversion
Lang.Absyn (h_0 x_1)-- ID 1.0.0x = 1
g x = x + 1-- ID 2.0.0x = 2
h x = x + 2

main= (\x.x+1) 1
GHC.HsSyn + (\x.x+2) 2
Allows allocating
different type variables

x_0
x_1

1
2

※ Full-resource polymorphism[Orchard’19] requires a revised
compilation scheme and an extension to core calculus.
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

59

Compiler Performance

How to Estimate Complexity
Exponential for number of variables, how to estimate?
Vectorize
Constraints

Vectors

Compile via sbv

Constraint
solving

SMT-LIB scripts[Barrett’16]
LabelsVectors
Reverse-vectorize

APLAS2023 @ Taipei

November 27, 2023

Constraint
resolution via Z3(declare-const a Bool)(declare-const b Bool)(define-fun demorgan () Bool(= (and a b) (not (or (not a) (not b)))))(assert (not demorgan))(check-sat)🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

60

Compiler Performance

SMT-Lib Scripts(declare-fun s0 () (_ BitVec 8))(declare-fun s1 () (_ BitVec 8))
Declare symbolic variables…
(define-fun s1552 () (_ BitVec 8) #x00)-- Special int value indicating undefined version…
(define-fun s1553 () Bool (distinct s1 s1552))
Constraints(define-fun s1554 () Bool (= s0 s1))
(define-fun s1555 () Bool (and s1553 s1554))
New symbolic variables(define-fun s1556 () Bool (= s1 s1552))
per variable/label(define-fun s1557 () Bool (xor s1555 s1556))
dependency…
(assert s3842)-- Represents all constraints
Assertion(minimize s4362) -- Maximize the number of-- undefined version elements(check-sat)(get-objectives)
Inspecting solution models…
APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

61

Compiler Performance

Size of Constraints
Vector size

Size of variable dep. :Size of label dep.
:

Correspond variable dependencies
Correspond label dependencies

Number ofdefinitions

Number of AST edges
𝑨𝑺𝑻

number of definitions in a module

depth of AST

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

62

hmatrix

Case Study

Module Structure
Reproducing incompatibility with Matrix and List

•
•
•
•
•

vjoin
sortVectortranspose
determinant…

Main

MatrixMatrix

List

•
•
•
•

join
transpose
determinant…
Data.List

from base (Haskell standard library)versionjoin

sortVector

0.15.0available

unavailable

0.16.0

Deleted (replaced vjoin)

available

hmatrix

Vector a
Matrix a=>=>

List Int
MatrixList (List Int)APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

63

Case Study

hmatrix

Handling Multiple Versions in a CodeCompilemodule Main where

Dispatching to a consistentVL
version of programs,
import Matrix
with unversion
as boundaries
importList
main =
let vec = [2, 1]
sorted = unversion(sortVector vec)
m22 = join -- [[1,2],[2,1]](singleton sorted)(singleton vec)in determinant m22

module Main where Haskell AST(prettyprint)
main = ...
-- join(let join = \xs -> \ys ->case xs of[] -> ysx : xs -> (:) x (join xs ys)
in join)...
-- sortVector(let sortVector = \xs ->case xs of[] -> [][x] -> [x]xs -> (\r -> (let vjoin = ... in vjoin)(sortVector((let init = ... in init) r))[(let last = ... in last) r])((let bubble = ... in bubble) xs)
in sortVector)...

Consistent in 0.15

Consistent in 0.16

> ghc –o main Main.hs> ./main-3
Note: inserting IO function “print” manually

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

64

Case Study

hmatrix

Main Module (before update)module Main where

Haskell

import Matrix
import List

• join• determinant
• …

Main

main =
let vec = [2, 1]
vec’ = [1, 2]
m22 = join -- [[1,2],[2,1]](singleton vec’)(singleton vec)in determinant m22

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

Matrix
List

65

Case Study

hmatrix

Main Module (after update)module Main where• join• determinant• …

Haskell

import Matrix
import List
main =
let vec = [2, 1]
sorted = sortVector vec
m22 = join -- [[1,2],[2,1]](singleton sorted)(singleton vec)in determinant m22

Main

Matrix
Conflict

Matrixmain.hs:1:38: error:
Variable not in scope: sortVector

•
•
•
•

vjoin
sortVector
determinant…

APLAS2023 @ Taipei

November 27, 2023

List

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

66

Case Study

hmatrix

Detecting Inconsistent Version

module Main where

VL

import Matrix
import List Version conflicts resolved,

but no consistent versions

main =
let vec = [2, 1]
sorted = sortVector vec
m22 = join -- [[1,2],[2,1]](singleton sorted)
Inconsistent(singleton vec)in determinant m22• join• determinant
• …

Main

Matrix
Conflict

Matrix
•
•
•
•

vjoin
sortVector
determinant…

APLAS2023 @ Taipei

November 27, 2023

List

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

67

Case Study

hmatrix

Handling Two Versions in One Client

module Main whereimport Matrix
import List

VL
No longer
depends on
0.16

main =
let vec = [2, 1]
sorted = unversion(sortVector) vec
m22 = join -- [[1,2],[2,1]](singleton sorted)(singleton vec)in determinant m22• join• determinant
• …

Main

MatrixMatrix

List

•
•
•
•

vjoin
sortVector
determinant…

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

68

Future Work

Automatic Adaptations

Detecting incompatibilities and inserting adapters automaticallyUpdateparse(…)

Adaptation
UpdatedUpdatedparse(…)

parse(…)

Concept:• Code repository, a persistent definition/package store• Working environment(s) that are views into the code repository
Nix [Dolstra’04]: Hash-tagged packages + Nix package manager
Unison: Hash-tagged definitions + Unison code base manager

Consistency
checking
within expressions

APLAS2023 @ Taipei

November 27, 2023

🎤Yudai Tanabe, 📑Compilation Semantics for a Programming Language with Versions

69