Presented at
PLDI’24@Copenhagen

Space-Efficient Polymorphic
Gradual Typing, Mostly Parametric
Atsushi Igarashi1, Shota Ozaki1,
Taro Sekiyama2, andYudai Tanabe3
1Kyoto University

2NII/SOKENDAI

3Tokyo Institute of Technology(Institute of Science Tokyo from October)

JSSST’41
September 11, 2024

1

Introduction

Gradual Typing (GT)[Siek&Taha’06]

Languages and tools:
TypeScript, Typed Racket, Typed Closure,
C#, Dart, Raku (Perl 6), mypy, …

Enables migration between static and dynamic typing in a language
def succ(x):return x + 1
class X:
passx = X()
succ(x)incompatible
types:
def succ(x:int): X cannot be
return x + 1
converted to intsucc(x);^class X:

ill-typed

well-typed--> TypeError:
unsupported operandtype(s) for +:'X' and 'int'

Gradualpass

x = X()
succ(x)

Gradual+ Type annotation
JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric2

Introduction

How GT[Siek&Taha’06] Works With Unknown Types
Deferred the type check for the dynamic type ⋆ to run time
At compile time

well-typed
def succ(x):return x + 1Error

class X:
pass
x = X()
succ(x)The GT checker gives ⋆ to type-unknown variables.
⋆ ⇝ intX⇝⋆

GradualThe GT checker allows implicit typeconversions between ⋆ and any type.

At runtime

All values typed ⋆ are type-checked at runtime.

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric3

Motivation

Theoretical Research on Gradual Typing
Parametric polymorphism[Ahmed et al.’11,’17; Igarashi et al.’17;
Toro et al’19, New et al.’20, Labrada et al.’22]

Intersection / union types

Objects[Siek&Taha’07]

Effects[Castagna&Lanvin’17][Schwerter et al.’14;
Sekiyama et al.’15, New et al.’23]

Dependent typing

Typestate[Lennon-Bertrand et al.’22; Eremondi et al.’22][Wolff et al.’11]

Security typing

Type inference[Fennell&Thiemann’13;
Toro et al.’18; Chen&Siek’24][Siek&Vachharajani’08;
Garcia&Cimini’15; Miyazaki et al.’19]

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametricetc.

4Motivation

Polymorphic GT (PGT)[Ahmed et al.’11,’17; others]
Supports polymorphic types ∀X.T
and enforces parametricity at run time
let id⋆let id∀: ⋆= λx:⋆. x: ∀X.X→X = id⋆

id∀ [bool] true −→ trueid∀ [int] 42−→ 42id∀ [⋆](42:⋆) −→ (42:⋆)let succ⋆ : ⋆= λx:int. x+1
let id∀: ∀X.X→X = succ⋆
id∀ [bool] true −→ errorerror
id∀ [int] 42−→ 42error
id∀ [⋆](42:⋆) −→ 42

Nonparametric?

Run-time errors happen if programs
try to break abstraction of polymorphism
JSSST’41
September 11, 2024

Yudai Tanabe,Space-Efficient Polymorphic Gradual Typing, Mostly Parametric5Motivation

Long-Term Goal: Efficient PGT Implementation
Space-efficient impl.
impl. isis possible?
possible?

What low-level instruction isnecessary to compile?
Good performance is achievable?

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric6

Motivation

Space-Efficiency vs. Full Parametricity in PGT
Impossible to implement PGT space-efficiently[Ozaki’21](at least under dynamic sealing, the standard method to enforce parametricity)

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric7

This Research

Our Contribution“Mostly” parametric PGT can be made space-efficient
Mostly parametric PGTKey Ideaid∀ [bool] true −→ error
id∀ [int] 42−→ error
id∀ [⋆](42:⋆) −→ 43:⋆

Parametricity is enforced
only if polymorphic
values are instantiatedwith non-⋆ types

Recap
let succ⋆ : ⋆let id∀= λx:int. x+1: ∀X.X→X = succ⋆

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric8

MethodCoercion Calculus: An IR for GT[Henglein’94]
Run-time type conversions are made explicit as coercions ⟨𝒄⟩
Surface Coercion calculus
Converted from int to ⋆let x:⋆ = 42
in x + 1
Converted from ⋆ to int

CompileCoercions can be
automatically inserted[Siek’06, ’21]

A value of ⋆tagged with 𝐢𝐧𝐭

𝐥𝐞𝐭 𝑥 ∶ ⋆ = 42⟨𝐢𝐧𝐭!⟩
𝐢𝐧 𝑥⟨𝐢𝐧𝐭? ⟩ + 1→∗ 42⟨𝐢𝐧𝐭!⟩⟨𝐢𝐧𝐭?𝒑 ⟩ + 1→∗ 43
Dynamic type checking
𝐢𝐧𝐭 = 𝐢𝐧𝐭

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric9

Method

Coercion Calculus: An IR for GT[Henglein’94]
Run-time type conversions are made explicit as coercions ⟨𝒄⟩Surface Coercion calculus
Converted from bool to ⋆let x:⋆ = truein x + 1
Converted from ⋆ to int

Compile𝐥𝐞𝐭 𝑥 ∶ ⋆ = true⟨𝐛𝐨𝐨𝐥!⟩𝐢𝐧 𝑥⟨𝐢𝐧𝐭? ⟩ + 1→∗ true⟨𝐛𝐨𝐨𝐥!⟩⟨𝐢𝐧𝐭? ⟩ + 1→∗ 𝐞𝐫𝐫𝐨𝐫 ✘Dynamic type checking
𝐛𝐨𝐨𝐥 ≠ 𝐢𝐧𝐭

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric10

Method

Parametricity Enforcement

Intuition: type names 𝜶 can beconsidered as fresh base types

Key Idea: dynamic sealing
Λ𝑋. 𝑀 𝐴 → 𝑀[𝑋 ↦ 𝜶] (where 𝜶 is fresh)✘Nonparametricsemantics

Parametric semantics
w/ dynamic sealingΛ𝑋. 42⟨int!⟩⟨𝑋? ⟩Apply int

Apply bool→∗ 42⟨int!⟩⟨int? ⟩ →∗ 42⟨int!⟩⟨bool? ⟩→∗ 42→∗ error
Coercion
calculus

JSSST’41
September 11, 2024

Yudai Tanabe,

Applyint/bool

Sealing abstraction
by type names 𝛼→∗ 42⟨int!⟩⟨𝛼? ⟩→∗ error

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

11

Method

Parametricity Enforcement
Key Idea: dynamic sealing
Λ𝑋. 𝑀 𝐴 → 𝑀[𝑋 ↦ 𝜶] (where 𝜶 is fresh)
Surface Coercion calculus
let id∀ : ∀X.X → X = ΛX.λx:X.
let x’: ⋆ = x inlet y : ⋆ = x’ + 1 in(y : X)

Compile⟨𝑋!⟩ ∶ 𝑋 ⇝ ⋆New coercions:⟨𝑋? ⟩ ∶ ⋆ ⇝ X

𝐥𝐞𝐭 𝑖𝑑∀ ∶ ∀𝑋. 𝑋 → 𝑋 = 𝛬𝑋. 𝜆𝑥 ∶ 𝑋.
𝐥𝐞𝐭 𝑥 ′ = 𝑥⟨𝑋!⟩ 𝐢𝐧𝐥𝐞𝐭 𝑦 = 𝑥 ′ ⟨𝐢𝐧𝐭? ⟩ + 1 ⟨𝐢𝐧𝐭? ⟩ 𝐢𝐧𝑦⟨𝑋? ⟩⟨𝛼!⟩ ∶ 𝐴 ⇝⋆⟨𝛼? ⟩ ∶⋆⇝ A

𝐴 is the type argumentin generating 𝛼

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

12

MethodParametricity Enforcement
Key Idea: dynamic sealing
Λ𝑋. 𝑀 𝐴 → 𝑀[𝑋 ↦ 𝜶] (where 𝜶 is fresh)
Surface Coercion calculus
let id∀ : ∀X.X → X = ΛX.λx:X.
let x’: ⋆ = x inlet y : ⋆ = x’ + 1 in(y : X)

𝐥𝐞𝐭 𝑖𝑑∀ ∶ ∀𝑋. 𝑋 → 𝑋 = 𝛬𝑋. 𝜆𝑥 ∶ 𝑋.
𝐥𝐞𝐭 𝑥 ′ = 𝑥⟨𝑋!⟩ 𝐢𝐧𝐥𝐞𝐭 𝑦 = 𝑥 ′ ⟨𝐢𝐧𝐭? ⟩ + 1 ⟨𝐢𝐧𝐭? ⟩ 𝐢𝐧𝑦⟨𝑋? ⟩𝑖𝑑∀ int 42→∗ 𝐥𝐞𝐭 𝑥 ′ = 42⟨𝛼!⟩ 𝐢𝐧 …
→∗ 𝐥𝐞𝐭 𝑦 = (42⟨𝜶!⟩⟨𝐢𝐧𝐭? ⟩ + 1)⟨𝐢𝐧𝐭? ⟩ 𝐢𝐧 …
→∗ error

JSSST’41
September 11, 2024

CompileYudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

13

Method

Space-Efficiency[Herman et al.’07,’10]
The space consumed by coercions is statically predictable∀𝑀. ∃𝑛 ∈ ℕ. 𝑀 →∗ 𝑀′ ⟨𝑐𝑖 ⟩⇒ ∃𝑐. 𝑐 =ctx ⟨𝑐𝑖 ⟩ ∧ size 𝑐 ≤ 𝑛• Any ⟨𝑐1 ⟩ ⋯ ⟨𝑐𝑛 ⟩ appearing at run time can be compressed into ⟨𝑐⟩whose size is bounded statically• They introduce eager composition semantics to coercion calculus𝑀⟨int!⟩⟨int? ⟩ → 𝑀⟨idint ⟩JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric14

[Ozaki et al.’21]

Key Idea

Impossibility of Space-Efficient, Fully Parametric PGTShown by the following facts:
Coercion
calculus①There is a well-typed program thatgenerates ⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩ for arbitrary 𝑛let 𝐹 = 𝐟𝐢𝐱 𝑓 = Λ𝑋. 𝜆𝑥 ∶ 𝑋. 𝑓 ⋆ 𝑥⟨𝑋!⟩
𝐢𝐧 𝐹 ⋆ 0⟨Int!⟩→∗ 𝐹 ⋆ 0⟨Int!⟩⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩size ⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩ > 𝑛∄c s.t. ⟨𝑐⟩ =ctx ⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩③The size of ⟨𝜶𝟏 !⟩ ⋯ 𝜶𝒏 !
is not less than 𝑛②⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩ cannot be compressed intoa smaller coercion with the same semantics

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

15

Key Idea

Key Observations from The Impossibility
The impossibility arises from the type name generation at 𝑴 ⋆Erroneous but well-typed coercion sequence⟨𝜶𝟏 !⟩ ⋯ 𝜶𝒏 ! ∶ 𝐴 ⇝ ⋆⟨𝜶𝟏 !⟩ ⋯ ⟨𝜶𝒏 !⟩ is well typed
only when⇒ ⟨𝛼𝑖 !⟩ ∶⋆ ⇝ ⋆Recap⟨𝛼!⟩ ∶ 𝐴 ⇝ ⋆𝐴 is the type argumentin generating 𝛼(2 ≤ 𝑖 ≤ 𝑛)
… and such 𝛼𝑖 is generated bytype application 𝑴 ⋆JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

16Key Idea“Mostly” Parametric Semantics, InformallySpace-efficiency is possible if 𝑴 ⋆ generates no type nameDynamic type analysis for type arguments

𝑀 𝑋 ↦⋆
Λ𝑋. 𝑀 𝐴 → ቊ𝑀 𝑋↦𝛼if 𝐴 = ⋆if 𝐴 ≠ ⋆Dynamic type checking does not perform for ⋆⟨𝑋!⟩ 𝑋 ↦ ⋆ = ⟨id⋆ ⟩⟨𝑋? ⟩ 𝑋 ↦ ⋆ = ⟨id⋆ ⟩JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

17

(Informally)

Method“Mostly” Parametric PGT becomes Space-Efficientlet 𝐹 = 𝐟𝐢𝐱 𝑓 = Λ𝑋. 𝜆𝑥 ∶ 𝑋. 𝑓 ⋆ 𝑥⟨𝑋!⟩
𝐢𝐧 𝐹 ⋆ 0⟨Int!⟩→∗ 𝐟𝐢𝐱 𝑓 = Λ𝑋. 𝜆𝑥 ∶ 𝑋. 𝑓 ⋆ 𝑥⟨𝑋!⟩⋆ 0⟨Int!⟩→∗ 𝜆𝑥 ∶ ⋆. 𝐹 ⋆ 𝑥⟨id⋆ ⟩→∗ 𝐹 ⋆ 0⟨Int!⟩⟨id⋆ ⟩→∗ 𝐹 ⋆ 0⟨Int!⟩

Refinedtype substitution

0⟨Int!⟩⟨𝑋!⟩ 𝑋 ≔ ⋆ = ⟨id⋆ ⟩JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric18

Results

New polymorphic coercions for
type analysis on whether
type arguments are ⋆What We Achieve∀𝜆C𝑚𝑝preservingtypes and semantics• Mostly parametric semantics• Eager coercion composition• Mostly parametric semantics• Not space-efficient

Bisimulation

Type safety

Parametricity
except for ⋆Refined from[Ahmed’17]

Type safety

Is

Space-efficient(By handwritten proof, 200+ pages)

JSSST’41
September 11, 2024∀
𝜆S𝑚𝑝

Translation

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly ParametricFrom[Siek’15]
From[Herman’10]

19SummaryConclusion“Mostly” parametric PGT can be made space-efficient∀𝜆C𝑚𝑝Parametricity
except for ⋆Translation∀𝜆S𝑚𝑝Bisimulation

Space-efficiency

Future work:• Practical evaluation in terms of both time and space• Explore optimization opportunities for "mostly"-parametricity
JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric20

(Spares) Motivation

Why Parametricity?[Reynold’86, Wadler’89]
Security• Non-interference[Sumii&Pierce’00,’03, Chen&Siek’22,’24]

Data abstraction• State encapsulation[Launchbury’94]𝑝Program optimization• Deforestation (a.k.a. fusion)[Wadler’90, Gill’93,’96, Marlow’96]

map f (map g xs)= map (f . g) xss.t. ∀𝑒𝑖 , 𝑒𝑗 . 𝑝 𝑒𝑖 =ctx 𝑝 𝑒𝑗
JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

21

(Spares) Ongoing & Future Work

[Siek’12,Herman et al.’07,’10]

Difficulties in Space-Efficient GT Implementation
Need to capture the context-sensitivity
to trigger eager-composition

Case. 𝐸 = □ 𝑀 𝑉 □ □ 𝐴

Case. 𝐸 = □ ⟨𝑐⟩
Subcase. 𝑀 is a coercion application′𝑀⟨𝑐1 ⟩⟨𝑐2 ⟩ → 𝑀 ⟨𝑐1 ྦ 𝑐2 ⟩𝑀 → 𝑀′′
𝐸[𝑀] → 𝐸[𝑀 ]Note: No compilers fully solve(d) the growing-coercion problem.
[Feltey’18, Kuhlenschmidt’19]

JSSST’41
September 11, 2024

Yudai Tanabe,

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

22

(Spares) Ongoing & Future Work

2
Defunctionalized 𝐂 PS Interpreter
type val =IntV of int| Fun of (val -> cont -> val)
| TFun of (ty -> cont -> val)
| CAppV of coercion * val
and cont =CFId| CFAppFun of term * env * cont
| CFAppArg of val * cont
| CFTApp of ty * cont
| CFCApp of coercion * contDefunctionalizecontinuation closures[Reynolds’98, Danvy’01]

JSSST’41
September 11, 2024

Yudai Tanabe,

Originally stated in [Herman’10],
Formalized in [Tsuda’20]“Coercion”-passing style interpreter(& continuation)

k captures nearest
let rec apply_k k v env =match k withevaluation context
CFId -> v& coercion| CFAppFun(exp,env,k’) ->eval exp env (CFAppArg(v,k’))| CFCApp(c1,k’) -> …
and eval exp env k =match exp with
Var(r,id) ->apply_k k (lookup id env) env| …
Implemented in ~5000LOC,
though still WIPSpace-Efficient Polymorphic Gradual Typing, Mostly Parametric23