A Functional Programming
Language with Versions
Yudai Tanabea) Luthfan Anshar Lubisa)
Tomoyuki Aotanib) Hidehiko Masuharaa)(a) Tokyo Institute of Technology

November 24, 2022

<Programming>’22(b) Mamezou

1/29

BackgroundVersion Update May Break Software
Expects
𝑣1 of parser

appparserparse(…)

𝑣1 parse

Version Up

app
Error
parse(…)

November 24, 2022

parserparser𝑣3 parse

parse

BehaviorchangedDeleted<Programming>’22

app

𝑣2

Error?
parse(…)

2/29

Background

Implicit Assumption: One-version-at-a-timeparser 𝑣1

app
import parser (parse)
let x = parse …

parse

parser 𝑣2
parse

Only one version ofparse can be used

November 24, 2022

<Programming>’22

3/29

Background

Dependency Hell
• Difficult to resolve indirect dependency conflicts
𝑣2 parser

𝑣1 parserapp

𝑣8′

Updateapp Conflict𝑣8′ XML𝑣9′
𝑣8′ XML

So ... how do I fix it?

• Leads to version locking[Preston-Werner ’13]

Developers are reluctant to update[Bavota ‘15]
November 24, 2022

<Programming>’22

4/29

Research Proposal

Programming Language with Versions
Can use two versions
from one clientapp

Can detect inconsistentusages across versions
parser 𝑣1
parse

parse(…) 𝑣1

newXMLparse(…) 𝑣2

parser 𝑣2
parse

November 24, 2022

app

<Programming>’22

XML = newXML(…)
parse(XML)^^^

Expected: 𝑣2
Found: 𝑣1

5/29

Research Proposal

Language Overview• Idea: Multiple versions in one value
Both versions
are available

app

parser 𝑣1
parse

parse(…)

parser 𝑣2

parse(…)

parse

Semantic analysis
𝑣1 𝑣2
chooses one
November 24, 2022

<Programming>’22

6/29

Research Proposal

Language Overview• Idea: Multiple versions in one value① Bundle multiple
versions of definitions

app
parse(…)
parse(…)

parser 𝑣1

parserparse

𝑣1
𝑣2 parse

parser 𝑣2
parse

November 24, 2022

<Programming>’22

7/29

Research Proposal

Language Overview• Idea: Multiple versions in one value② Infer a safe version
by semantic analysis① Bundle multiple
versions of definitions

app
parse(…)

parse(…)

parse(…)

𝑣1 𝑣2

parser 𝑣1

parserparse

𝑣1
𝑣2 parse

parser 𝑣2
parse

November 24, 2022

<Programming>’22

8/29

Research Proposal

Language Overview• Idea: Multiple versions in one value② Infer a safe version
by semantic analysis① Bundle multiple
versions of definitions

app
parse(…) 𝑣1

parse(…)

parse(…) 𝑣2

𝑣1 𝑣2

parser 𝑣1

parserparse

𝑣1
𝑣2 parse

parser 𝑣2
parse

November 24, 2022

<Programming>’22

9/29

Research Proposal

Language Overview• Idea: Multiple versions in one value② Infer a safe version
by semantic analysis① Bundle multiple
versions of definitions

app
parse(…) 𝑣1

parse(…)

parse(…) 𝑣2

𝑣1 𝑣2

parser 𝑣1

parserparse

𝑣1
𝑣2 parse

parser 𝑣2
parse

𝜆VL [Tanabe’18, Tanabe’22]
November 24, 2022

<Programming>’22

10/29

Core Calculus

𝜆VL : Versioned Values• Versioned records:
Multiple versions in one value like a record
Version labels

𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑝𝑎𝑟𝑠𝑒 =
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

November 24, 2022𝑣1 ↦ 𝑙1𝑣2 ↦ 𝑙2𝑝𝑎𝑟𝑠𝑒𝑣1

𝑝𝑎𝑟𝑠𝑒𝑣2= \xml ->let elem = pop …
in …

= \xml ->let elem = pop …
in …

<Programming>’22

11/29

Core Calculus

𝜆VL Program Construction• By function application of versioned values
let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in𝑓𝑥
𝜆VL

November 24, 2022≈

𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1 𝑜𝑏𝑗𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2 𝑜𝑏𝑗𝑣2

𝑝𝑎𝑟𝑠𝑒

𝑋𝑀𝐿

𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝑙1 = 𝑜𝑏𝑗𝑣1
𝑙2 = 𝑜𝑏𝑗𝑣2
𝑙3 = 𝑜𝑏𝑗𝑣3<Programming>’22

12/29

Core Calculus

𝜆VL Semantics• Extraction 𝑡. 𝑙:Specify 𝑙 to run the program in a specific version
Version-abstracted computation
𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝑙=𝑡

𝑙1 = 𝑜𝑏𝑗𝑣1
𝑙2 = 𝑜𝑏𝑗𝑣2
𝑙3 = 𝑜𝑏𝑗𝑣3

𝑡. 𝑙𝑝𝑎𝑟𝑠𝑒 𝑋𝑀𝐿 . 𝑙1
o𝑏𝑗𝑣1 , ⋯ , 𝑜𝑏𝑗𝑣3
𝑝𝑎𝑟𝑠𝑒𝑣1 , 𝑝𝑎𝑟𝑠𝑒𝑣2
Usual computation

November 24, 2022

<Programming>’22

13/29

Core Calculus

𝜆VL Semantics• Extraction 𝑡. 𝑙:Specify 𝑙 to run the program in a specific version
Version-abstracted computation
𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝑙=𝑡

𝑙1 = 𝑜𝑏𝑗𝑣1
𝑙2 = 𝑜𝑏𝑗𝑣2
𝑙3 = 𝑜𝑏𝑗𝑣3

𝑝𝑎𝑟𝑠𝑒 𝑋𝑀𝐿 . 𝑙1
o𝑏𝑗𝑣1 , ⋯ , 𝑜𝑏𝑗𝑣3
𝑝𝑎𝑟𝑠𝑒𝑣1 , 𝑝𝑎𝑟𝑠𝑒𝑣2
Usual computation

November 24, 2022

𝑡. 𝑙<Programming>’22

𝑝𝑎𝑟𝑠𝑒𝑣1 𝑜𝑏𝑗𝑣1[("English","hello"),("French","bonjour"),("Japanese","konnichiwa")]
14/29

Core Calculus

Inconsistency to Detect in 𝜆VL• No extractable version
let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in𝑓 𝑥 . 𝑙1
let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in𝑓 𝑥 . 𝑙3

November 24, 2022≈≈

𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝑙1 = 𝑜𝑏𝑗1
𝑙2 = 𝑜𝑏𝑗2
𝑙3 = 𝑜𝑏𝑗3

𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝑙1 = 𝑜𝑏𝑗1
𝑙2 = 𝑜𝑏𝑗2
𝑙3 = 𝑜𝑏𝑗3<Programming>’22

15/29

Core Calculus

𝜆VL Type System: Versions as Resources• Types are tagged with available version labels𝑝𝑎𝑟𝑠𝑒 ∶ □ 𝒍𝟏 ,𝒍𝟐 (XML → 𝐴)

𝑋𝑀𝐿 ∶ □ 𝒍𝟏 ,𝒍𝟐 ,𝒍𝟑 XML

𝒍𝟏 = 𝑝𝑎𝑟𝑠𝑒𝑣1
𝑝𝑎𝑟𝑠𝑒 =
𝒍𝟐 = 𝑝𝑎𝑟𝑠𝑒𝑣2

𝒍𝟏 = 𝑜𝑏𝑗1
𝑋𝑀𝐿 = 𝒍𝟐 = 𝑜𝑏𝑗2
𝒍𝟑 = 𝑜𝑏𝑗3

November 24, 2022

<Programming>’22

16/29

Core Calculus

𝜆VL Type System• Collect consistent versions along with usual typechecking
𝑝𝑎𝑟𝑠𝑒 ∶ □ 𝑙1 ,𝑙2 (XML → 𝐴)

𝑋𝑀𝐿 ∶ □ 𝑙1,𝑙2 ,𝑙3 XML=

let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in : □ 𝒍𝟏 ,𝒍𝟐 𝐴
𝑓𝑥
𝑙1 , 𝑙2 , 𝑙3 ∩ 𝑙1 , 𝑙2

November 24, 2022

<Programming>’22

17/29

Core Calculus

𝜆VL Type System• Inspect the consistency of specified version by an
extraction𝑝𝑎𝑟𝑠𝑒 ∶ □ 𝑙1 ,𝑙2 (XML → 𝐴)

𝑋𝑀𝐿 ∶ □ 𝑙1,𝑙2 ,𝑙3 XML

let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in : 𝐴
𝑓 𝑥 . 𝑙1
because 𝑙1 ∈ 𝑙1 , 𝑙2 , 𝑙3 ∩ 𝑙1 , 𝑙2

November 24, 2022

<Programming>’22

□𝑟 𝐴
𝑙=𝑡

𝑡. 𝑙

𝐴

18/29

Core Calculus

𝜆VL Type System• Inspect the consistency of specified version by an
extraction𝑝𝑎𝑟𝑠𝑒 ∶ □ 𝑙1 ,𝑙2 (XML → 𝐴)

𝑋𝑀𝐿 ∶ □ 𝑙1,𝑙2 ,𝑙3 XML

let 𝑓 = 𝑝𝑎𝑟𝑠𝑒 inlet 𝑥 = 𝑋𝑀𝐿 in :𝑓 𝑥 . 𝑙3

[ERROR]
Expected 𝑙3 ,but got 𝑙1 , 𝑙2

because 𝑙3 ∉ 𝑙1 , 𝑙2 , 𝑙3 ∩ 𝑙1 , 𝑙2

November 24, 2022

<Programming>’22

19/29

The Design of 𝜆VL Type System

Formalization with Coeffect Calculus
𝑝𝑎𝑟𝑠𝑒: XML → . . {𝒍𝟏 ,𝑙2}⊢ 𝑝𝑎𝑟𝑠𝑒 𝑋𝑀𝐿 : □ 𝒍 ,𝑙 𝐴
𝟏 2

𝑋𝑀𝐿: XML 𝒍𝟏 ,𝑙2 ,𝑙3
All subterms hold theversion label as a resource

The program is⟺ available
in the version

Coeffect calculus:ℓRPCF[Brunel’14], GrMini[Orchard’19]
November 24, 2022

<Programming>’22

20/29

The Design of 𝜆VL Type System

Coeffect Calculus
Coeffect calculus: ℓRPCF[Brunel’14], GrMini[Orchard’19]𝑡 ∷= 𝑛

𝑥

𝑡1 𝑡2

𝜆𝑥. 𝑡

𝑡 | let 𝑥 = 𝑡1 in 𝑡2 |Terms from coeffect calculus

𝐴 ∷= Int

𝐴→𝐴

□𝑟 𝐴

Γ ∷= ∅

Γ, 𝑥 ∶ 𝐴

Γ, 𝑥 ∶ 𝐴 𝑟𝑟 ∈ (ℛ, +, 0,×, 1)ℛ-parameterized type systemsℛ = {Irrelevant, Private, Public}(security level[Orchard’19])

November 24, 2022

<Programming>’22ℛ = ℕ (exact usage[Petricek’14])
e.g. □0 𝐴, □2 𝐴

21/29

The Design of 𝜆VL Type System

𝜆VL Type System• ℓRPCF-extension by versions as resources
Coeffect calculus: ℓRPCF[Brunel’14], GrMini[Orchard’19]𝑡 ∷= 𝑛

𝑥

𝑡1 𝑡2

𝜆𝑥. 𝑡

𝑡 | let 𝑥 = 𝑡1 in 𝑡2 |Terms from coeffect calculus

𝜆VL

November 24, 2022

𝐴 ∷= Int

𝐴→𝐴

□𝑟 𝐴

Γ ∷= ∅

Γ, 𝑥 ∶ 𝐴

Γ, 𝑥 ∶ 𝐴 𝑟𝑟 ∈ (ℛ, +, 0,×, 1)

𝑡 ∷= … | 𝑙 = 𝑡 | 𝑡. 𝑙v.v. con-/de-structorsℛ = 𝕃 (version labels)
e.g. □∅ 𝐴, □ 𝑙1,𝑙2 𝐴… and some corresponding typing rules<Programming>’22

22/29

Future Work

Implementation② Inference & Extraction① Bundling➢ Formalize an inference algorithm
and select one specific version➢ Conversion from
Haskell subset to 𝜆VL

parser 𝑣1

app
parse(…) 𝑣1

parse(…)

parse(…) 𝑣2

𝑣1 𝑣2

parser

parse

𝑣1
parse
𝑣2

parser 𝑣2
parse

𝜆VL [Tanabe’18, Tanabe’22]
November 24, 2022

<Programming>’22

23/29

Future Work

Implementation① Bundling

𝜆VL

Bundle all top-level values
as versioned values

parserHaskellsubsetparser 𝑣1

parser{𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1 }parse{𝑙1 = 𝑝𝑎𝑟𝑠𝑒𝑣1 ,𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2 }parserparser 𝑣2{𝑙2 = 𝑝𝑎𝑟𝑠𝑒𝑣2 }parse

Any term and type derivation in STLC can betranslated into GrMini (𝜆VL -base)[Orchard’19]
November 24, 2022

<Programming>’22

24/29

Future Work

Implementation② Inference & Extraction
Haskellsubset𝜆VL

appparse(…) 𝑣1
parse(…) 𝑣2

𝑣1
𝑣2

parse(…)

parse(…)

𝑣1 xml𝑣1
𝑣2 parse

Require to reduce the search
space by preprocessing?
November 24, 2022

<Programming>’22

25/29

Future Work

Adapting Old Version into New Version• Incorporate compatible updates… but actually 𝑝𝑎𝑟𝑠𝑒𝑣1 and𝑝𝑎𝑟𝑠𝑒𝑣2 are compatible

𝑣2
parse(…)
Updated𝑣1

November 24, 2022

parse(…)

Update<Programming>’22

𝑣1

26/29

Future Work

Adapting Old Version into New Version• Incorporate compatible updates… but actually 𝑝𝑎𝑟𝑠𝑒𝑣1 and𝑝𝑎𝑟𝑠𝑒𝑣2 are compatible

𝑣2
parse(…)
Updatedparse(…)

𝑣1

Update𝑣1① Inserting an adapter

𝑣1 𝑣2

Updated𝑣2

𝑣1

Adapterparse(…)

November 24, 2022

<Programming>’22

27/29

Future Work

Adapting Old Version into New Version• Incorporate compatible updates… but actually 𝑝𝑎𝑟𝑠𝑒𝑣1 and𝑝𝑎𝑟𝑠𝑒𝑣2 are compatible

𝑣2
parse(…)
Updatedparse(…)

𝑣1① Inserting an adapter

𝑣1 𝑣2

Update𝑣1② Handling compatibility
in the type system
𝑣2 𝑣1

≈

Updatedparse(…)

November 24, 2022

Compatible<Programming>’22

Updated𝑣1 ≈ 𝑣2

parse(…)
28/29

Summary
Proposal

ProblemA language enablesMultiple versions in one value

Implicit assumption:
One-version-at-a-time② Inferenceappparse(…) 𝑣1

parse(…)

parse(…) 𝑣2

𝑣1 𝑣2① Bundlingparser 𝑣1

parserparse

𝑣1
𝑣2 parse

parser 𝑣2
parse

Core: 𝜆VL

Future work

Coeffect calculus+ Versions as resources❑ Implementation❑ Adaptation
For Java: BatakJava[TBD]

November 24, 2022

<Programming>’22

29/29