PLDI 2024 Response

# Response

We thank the reviewers for their close reading and insightful comments. In what follows, we first give an overview of the response, which summarizes the reviewers' concerns and questions and briefly explains how we will address them. We then list changes we plan to make in the revision and respond to individual concerns, questions, and comments in detail.

# Overview

- Reviewer A asks whether we can ameliorate the exponential blow-up of coercions incurred by the translation to the space-efficient calculus. We expect it would be possible, but there would be a trade-off between static coercion size and runtime cost.
- Reviewer B asks what is lost in our calculus other than the full parametricity. We find no other example of the loss. The property Reviewer B mentioned as an example, which is one case of the dynamic gradual guarantee (a.k.a., graduality), does not hold even if we retain the full parametricity and instead give up space efficiency, as discussed by Toro et al. [2019].
- Reviewer B asks whether there is a hope for mechanization. Siek and Chen [JFP 2021] mechanized $\lambda$S, a simply-typed space-efficient coercion calculus. We could extend that mechanization to polymorphism, but it is challenging and beyond the scope of the present work.
- Reviewer C seems to ask what the relaxed parametricity means and why the unbounded number of casts matters in practice. The relaxed parametricity means that the parametricity holds only when polymorphic values are instantiated with non-dynamic types. The unbounded number of casts matters in programs with quasi-tail-recursive functions as the even and odd functions presented in the paper (although they don't use parametricity).
- Reviewer C asks whether there are more relaxed solutions to space efficiency. There can be (see below for details), but we believe the proposed approach strikes a good balance between simplicity and what is sacrificed for space efficiency. Note that the solution mentioned by Reviewer C does not lead to space efficiency because space efficiency is a property ensuring that the size of any coercion appearing at run time is _statically_ bounded by some static information of the program.
- Reviewer D is concerned with the practicality of the proposed approach. Although we admit the importance of evaluating the design of our space-efficient coercion calculus, in this paper, we are interested in a theoretical question of whether it is possible to gain space efficiency in the presence of polymorphism without giving up parametricity completely, which is a key question that influences the designs and implementations of polymorphic gradually typed languages. We proved it is possible by proposing a novel coercion form $\forall X. s ,\!, t$. Perhaps the design of coercions in this form seems straightforward due to its simplicity, but we believe its discovery and the proof work with it (how it ensures space efficiency and the correctness of the translation from the calculus without it to the one with it) are not straightforward. We consider the development of an efficient implementation based on the idea presented in the paper, as well as its practical evaluation, as a next step.

Reference:
- [Siek and Chen, JFP 2021] Jeremy G. Siek, Tianyu Chen. Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi. J. Funct. Program. 31: e30 (2021)

# Major Change List for Revision

We plan to revise the paper as follows.

- We will add a discussion about design decisions. Specifically, we will discuss (1) whether we can relax the exponential blow-up of coercions incurred by the translation and (2) other (more complicated) potential approaches to space efficiency.
- We will improve the discussion of why accumulating (an unbounded number of) casts can be problematic.
- We will add a discussion about the work of Kuhlenschmidt et al. [PLDI 2019].

We will also address the remaining issues (such as typos and the readability improvement) posed by the reviewers.

# Detailed Response

## Reviewer A

> p. 13
>
> Can you ameliorate the exponential blow-up by pushing the ",," to the leaves of the tree, analogous to the choice calculus of Erwig et al.?

Yes, we think so. The current translation produces a coercion whose size may grow exponentially with respect to the size of the original source coercion. By adopting the suggested change, the size of the produced coercion only grows exponentially with respect to the number of type variables appearing in the original coercion. However, we might need to pay the cost at run time. In the current definition ``,,`` only appears immediately under $\forall$ as $\forall X s ,\!, t$. A benefit of this form is that, when a type abstraction with coercion $\forall X s ,\!, t$ is applied to a type argument $A$, what the runtime system needs to do is just to choose either $s$ or $t$ according to $A$. However, when we adopt the suggested change, ``,,`` may not be placed immediately under $\forall$ as it should be in the leaf positions in a type. Then, when facing a type application, the runtime system would need to find ``,,`` in the leaf positions by traversing the type, which is more costly. Also, the definition of the meta-level coercion composition would be (much) more involved. Perhaps we could achieve an efficient implementation that resolves these issues, but whether and how it is possible is left open.

> Related Work
>
> I'd recommend adding a brief discussion of the work of Kuhlenschmidt et al. [PLDI 2019], who show how to compile space-efficient coercions.

Thanks for the suggestion. We will discuss the work of Kuhlenschmidt et al. [PLDI 2019] in the revision. Briefly speaking, their coercion calculus involves coercions for tuples, references, vectors, and recursive types, but it does not support parametric polymorphism. It is an interesting direction to extend their language implementation with polymorphism.

> p. 3
>
> "the coercion calculus λC of Henglain [1994]; Siek et al. [2015b, 2021]" -> "the coercion calculus λC of Henglain [1994] and Siek et al. [2015b, 2021]"

> p. 6
>
> "suggest that that part of code not be ready (yet)" -> "suggest that part of the code is not yet ready"

> p. 12
>
> "which case to happen at run time" -> "which case will happen at run time"

Thanks for pointing out! We will fix them.

## Reviewer B

> The loss of parametricity for *-type applications is one consequence that you discuss. Are there any others? For example, couldn't it now be that a program initially annotated with * for a type application succeeds, but when annotated with a more precise type fails at runtime?

As described in the overview section, we have not found other instances of the loss caused by our approach. For the example pointed out by the reviewer (it is covered by the dynamic gradual guarantee), our polymorphic coercion calculus is closely related to GSF, a polymorphic gradually typed language proposed by Toro et al. [2019]. GSF satisfies the parametricity but not the dynamic gradual guarantee. Especially, the property specified by the reviewer does not hold in GSF (Corollary 9.2 in [Toro et al. 2019]). Therefore, we think that even if we give up space efficiency and retain the full parametricity (such a change results in the coercion calculus proposed by Ozaki et al. [2021]), the dynamic gradual guarantee, nor the property suggested by the reviewer, would not hold.

> I was confused for a bit in Section 3.5: You say
>
>> our logical relation relates V1 and V2 at ∀X.A if either of the following holds: for any
types B1 and B2, (the one-step reduction results of) type applications V1 B1 and V2 B2 ...
>
> I was expecting B1, B2 to be qualified so that neither of them at *. And indeed it is so, from looking at your supplement, you have:
>
>> W ′
.Σ1 ▷ V1 B1 −→ W ′
.Σ1, α := B1 ▷ M1hcoerce+
α (ρ(A)[X := α])i ∧
>
>> W ′
.Σ2 ▷ V2 B2 −→ W ′
.Σ2, α := B2 ▷ M2hcoerce+
α (ρ(A)[X := α])i
>
> in a premise, forcing both of them to be non-*. It would help to say that in the main paper.

The paper uses the Blackboard bold font (typeset using \mathbb in our TeX source) to specify the types B1 and B2 (that is, they are displayed as $\mathbb{B}_1$ and $\mathbb{B}_2$ in the paper). As explained in the first paragraph of Section 3.1, they mean non-* types. Therefore, as expected by the reviewer, we intend them to be non-*. To improve the readability, the revision will rephrase that part as "for any _non-dynamic_ types $\mathbb{B}_1$ and $\mathbb{B}_2$, ...".

> That said, while I appreciate the detailed and comprehensive 202 page supplement, it's pretty much impossible to check: any hope of this being mechanized?

We hope this question is addressed in the overview section.

> - Line 805: Typo ... the -1 is not in the exponent

Thank you! We will fix it.

## Reviewer C

> - The relaxed parametricity needs more discussion.

> - This paper needs more examples or case studies demonstrating the practical usefulness of the calculus.

> This paper only briefly explains the relaxed parametricity. It is quite hard to internalize what that exactly means: how useful is the calculus in practice and conversely, does the unbounded number of casts really matters in practice? Perhaps additional examples or a suite of case studies showing what's allowed and not allowed by the calculus would make it more concrete.

It seems that there are two different concerns, which are mixed: (1) what the relaxed parametricity would mean and (2) how the unbounded number of casts matter in practice.

The relaxed parametricity means the behavior of polymorphic values is independent of how they are instantiated (i.e., the parametricity holds) as far as they are applied to non-dynamic types. One of its benefits is that we can still retain "mostly" free theorems as Theorem 3.5 in the paper. Free theorems are useful for, e.g., optimization and program reasoning. The relaxed parametricity requires type arguments appearing in the free theorems to be non-dynamic (see Theorem 3.5, for instance), but we believe there are many cases where such mostly free theorems can be applied (as in fully statically typed parts of gradually typed programs).

The importance of addressing the unbounded number of casts is that we can ensure that _quasi-tail-recursive functions_ (functions that look tail-recursive by ignoring casts) can be executed without causing a stack overflow. The even and odd functions are such an example, although they don't use polymorphism. It's also been pointed out that accumulated casts and coercions significantly lower the performance of gradually typed programs. Herman et al. (followed by Siek et al.) solved this problem for a simply typed setting, but it's been a long-standing open question if (and to what degree) the idea can be extended to (parametric) polymorphism.

> - It is unclear if the restriction is necessary and whether there are more relaxed restrictions possible.

> For space efficiency, the proposed restriction is sufficient. Is it unclear if it is necessary. Some discussions on other possible more relaxed solutions would strengthen the result. For example, a naive solution is to detect the case of the infinite casts at runtime and do something about it then. Would such a runtime solution work and be more parametric than the proposed solution?

Thanks for the suggestion. To consider another solution, let us recall the point of the impossibility of a space-efficient implementation with parametricity. As explained at the beginning of Section 3, it is that there exists a program that generates a coercion application $M \langle \alpha !\rangle \cdots \langle \alpha !\rangle$ with $n$ coercions for an arbitrary number $n$, and such a coercion application happens only when the type name $\alpha$ is associated with the dynamic type $\star$. This fact indicates that no problem happens if the body $M$ of a type abstraction $\Lambda X. M$ does not coerce a value of $X$ into $\star$ (that is, does not apply coercions of the form $\langle X! \rangle$). Therefore, we could give a space-efficient coercion calculus where a type application $(\Lambda X.M) A$ generates a type name (i.e., the parametricity is enforced) only when the type argument $A$ is non-dynamic or the body $M$ of the type abstraction does not coerce a value of $X$ into $\star$. This approach relaxes the restriction on the calculus proposed in the paper in that more programs can benefit from parametricity. However, to implement it, we would need some device to detect (either statically or dynamically) whether the bodies of type abstractions perform coercions from type variables to $\star$. We think it is quite challenging (even if possible) to design a coercion calculus equipped with such a device and as simple as the calculus proposed in the paper.

> - There is no implementation of the type system.

> Finally, it is a pity that the system is not implemented. Otherwise, one could building a large set of tests to empirically evaluate the design.

As described in the overview section, the present work focuses on the theoretical aspects of the space-efficiency problem in polymorphic gradual typing, and we consider implementation and its evaluation as a next step.

> The notion for coercions in the presence of a type substitution is a bit hard to follow, especially for people who are not experts in gradual typing. A few more concrete examples and high-level explanations would be helpful.

We are not quite sure which part the reviewer is referring to. Maybe the definition of type substitution? If the point of confusing the reviewer is made clear, we'll be happy to add a few examples to help understanding.

## Reviewer D

> That being said, the presented formalisms seem like mostly straightforward extensions of previous calculi and on their own are not too technically interesting. Further, the formal aspects of gradual typing have already been thoroughly explored from pretty much every angle, so I think any new work needs to focus more on practical issues in order to move the state of the art forward. Thus, I was disappointed that, with the emphasis on a practically important issue such as space efficiency, the submission did not have any actual evaluation of its design decisions or even any way to run such an evaluation. Without looking at a real language with a real code base, one can only speculate on whether the insights of the submission are useful or not. Thus, without at least some practical evaluation of the design choice, I cannot recommend acceptance of the submission.

As described in the overview section, the present work aims to study the theoretical aspects of the space-efficiency problem in the presence of polymorphism. In fact, our work sheds new light on the formal aspects of polymorphic gradual typing. This opinion appears to be more or less in agreement with some other reviewers because Reviewer A wrote

> Ozaki et al. [2021] showed that it is impossible to simultaneously achieve space efficiency and parametricity for the λC∀ calculus, which many of us took to be the end of the story.

and Reviewer B wrote

> It tackles a hard problem that many have looked at for the past decade or so.

Furthermore, we think introducing the new form $\forall X. s,,t$ of coercions is a non-trivial extension. We agree with Reviewer D about the importance of evaluating the design decisions from a more practical viewpoint. However, it is beyond the scope of the present work and left for future work.

> typos
>
> p1 c1 , c2 two commas?
> p6 "that that"
> p8 "defined in straightforwardly"
> p17 "sematics"

For the first one, we cannot find it in the paper. It would be appreciated if the reviewer could point out the line number.
We will fix the remaining in the revision. Thanks!

---

以下メモ

---

# Review #478A
Overall merit
5.
Strong accept

Reviewer expertise
4.
Expert

Paper summary
The paper shows how to achieve space efficiency in a gradually-typed programming language with generics while only making a minor restriction regarding parametricity. Generics behave according to relational parametricity when they are instantiated with any type other than ★ (the unknown or dynamic type). The paper presents a coercion calculus for this language that gives a straightforward definition of its operational semantics and then the paper presents a space-efficient version of the coercion calculus, following the style of Siek, Thiemann, and Wadler (2015). The paper includes proofs of parametricity, space-efficiency, and that the translation to the space-efficient calculus preserves typing and semantics.

Comments for authors
Evaluation

Ozaki et al. [2021] showed that it is impossible to simultaneously achieve space efficiency and parametricity for the λC∀ calculus, which many of us took to be the end of the story. So it was a pleasant surprise to read this paper and find out that parametricity and space-efficiency can be achieved with just one minor restriction! The language does not perform runtime sealing (needed for parametricity) when a generic is instantiated with the type ★, but does so instantiations at any other types.

The technical development is solid and clearly explained.

Comments on details

p. 3

"the coercion calculus λC of Henglain [1994]; Siek et al. [2015b, 2021]" -> "the coercion calculus λC of Henglain [1994] and Siek et al. [2015b, 2021]"

p. 6

"suggest that that part of code not be ready (yet)" -> "suggest that part of the code is not yet ready"

p. 12

"which case to happen at run time" -> "which case will happen at run time"

p. 13

Can you ameliorate the exponential blow-up by pushing the ",," to the leaves of the tree, analogous to the [choice calculus of Erwig et al.](https://eric.walkingshaw.net/projects/choice-calculus.html)?

- 多分根本的に無理で、コストを別のフェーズに押し付けるだけ。
- 理由悦明...
- See coercion comp. & coercion Trans.
- 最適化の一案：Lazyに展開できないの？
- |c|をメタオペレーションではなくcoercionのコンストラクタとして持っておく
- その場合;;は定義できるか？が問題
- 最適化の一案：|\X.c| = \X. ~ ,, ~について、cのbodyの全てをコピーする必要はないかもしれない？
- トレードオフ：
- メモリ削減：choice pointを葉に押し付ける
- 実行速度：(平均的にはおそらく)遅い、型代入の度に葉をそぎ落とすので
- 合成も... 結局全ての代入のパターンを記録していないといけない。木全体で面倒見るか否か
- 何に対して指数が変わる
- 出てくる型変数に対して...など

Related Work

I'd recommend adding a brief discussion of the work of Kuhlenschmidt et al. [PLDI 2019](https://dl.acm.org/doi/abs/10.1145/3314221.3314627), who show how to compile space-efficient coercions.

- 多相性の採用の違いあり
- 議論は追加してもいいかも

# Review #478B
Overall merit
4.
Accept

Reviewer expertise
3.
Knowledgeable

Paper summary
The author's study the problem of gradual typing in a polymorphic setting and aim to give a space-efficient implementation. Prior results note that this is a hard problem, since type abstraction enforced with dynamic seals can lead to towers of uncancellable coercions.

The solution offered here is simple, intuitive, and a compelling compromise: give up on parametricity only when type abstractions are instantiated with * but get space efficiency.

Comments for authors
This is a great paper! It tackles a hard problem that many have looked at for the past decade or so. It explains the problem clearly and then comes up with a clean and elegant solution.

It's a great observation that type applications at * are the root and only cause of trouble, rather than the fresh name creation.

The technical setup of retaining conceal/reveal for the parametricity proof and then removing them for the space efficiency part was interesting.

The loss of parametricity for *-type applications is one consequence that you discuss. Are there any others? For example, couldn't it now be that a program initially annotated with * for a type application succeeds, but when annotated with a more precise type fails at runtime?

- Another property: Gradual garanteeとかどうなる？
- Toro et al.の段階で成り立たないので多分成り立たない
- Prametricity無くなってなぜか回復してる可能性もあるが別の要因
- argument がdynかどうかでしか変わってないので、それ以外のおおまかな性質は変わってないと予想される(たしかめてないけど

I was confused for a bit in Section 3.5: You say

our logical relation relates V1 and V2 at ∀X.A if either of the following holds: for any types B1 and B2, (the one-step reduction results of) type applications V1 B1 and V2 B2 ...

- ちゃんと書いてますが、わかりやすく書き直します

I was expecting B1, B2 to be qualified so that neither of them at *. And indeed it is so, from looking at your supplement, you have:

W ′ .Σ1 ▷ V1 B1 −→ W ′ .Σ1, α := B1 ▷ M1hcoerce+ α (ρ(A)[X := α])i ∧

W ′ .Σ2 ▷ V2 B2 −→ W ′ .Σ2, α := B2 ▷ M2hcoerce+ α (ρ(A)[X := α])i

in a premise, forcing both of them to be non-*. It would help to say that in the main paper.

That said, while I appreciate the detailed and comprehensive 202 page supplement, it's pretty much impossible to check: any hope of this being mechanized?

- JeremyがAgdaか何かでやってる？
- [Github](https://github.com/jsiek/gradual-typing-in-agda?tab=readme-ov-file)
- parametricityが大変そうだよね
- 上をベースに考えることはできるかもしれないけど...大変かつこの仕事の範囲を超える

Line 805: Typo ... the -1 is not in the exponent

# Review #478C
Overall merit
3.
Weak accept

Reviewer expertise
2.
Some familiarity

Paper summary
This paper presents a gradual type system with a restricted form of polymorphism so that the space needed for casts at run time is bounded. The key observation is that the dynamic type * needs to be inspected at run time to prevent the generation of infinite number of casts. As a result, the system only satisfies a relaxed form of parametricity. This paper formally defines a coercion calculus and a corresponding space-efficient version of the calculus, proves the relation between these two calculus, and establishes relaxed parametricity theory and space efficiency.

Comments for authors
Strengths:

This paper presents a fundamental result in space efficiency of gradual polymorphic types.

The restriction of not generating type names for * is clever and well explained.

This paper proves key theorems relating the two calculus and the space bounds.

Weaknesses:

The relaxed parametricity needs more discussion.

It is unclear if the restriction is necessary and whether there are more relaxed restrictions possible.

This paper needs more examples or case studies demonstrating the practical usefulness of the calculus.

There is no implementation of the type system.

This paper is nicely written. The background and motivation sections are enjoyable to read. The main insight that generating type names for * is causing the issue for the corner case of unbounded casts makes intuitive sense. This paper builds out the formalism to show that by not doing the above, the calculus has bounded number of casts.

This paper only briefly explains the relaxed parametricity. It is quite hard to internalize what that exactly means: how useful is the calculus in practice and conversely, does the unbounded number of casts really matter in practice? Perhaps additional examples or a suite of case studies showing what's allowed and not allowed by the calculus would make it more concrete.

- どんな例を付ければ納得するのか？(... matter in practice?)
- polymorphism recursion?

The notion for coercions in the presence of a type substitution is a bit hard to follow, especially for people who are not experts in gradual typing. A few more concrete examples and high-level explanations would be helpful.

For space efficiency, the proposed restriction is sufficient. Is it unclear if it is necessary. Some discussions on other possible more relaxed solutions would strengthen the result. For example, a naive solution is to detect the case of the infinite casts at runtime and do something about it then. Would such a runtime solution work and be more parametric than the proposed solution?

- 頓珍漢な指摘。論文中のspace-efficiencyと関係ない
- *Infinite* castの検出法、とは
- 検出できたところで、動かしてみてinfinite castがあったからといってなにか出来るとも思えない
- ただ、プログラムのコードを解析するとか型システムをリッチにして型代入の有無の解析をすれば、ある意味制限を緩めることはできるかも
- そこまでのことはこの研究を超える範囲で、我々は形式化は単純な今の形式がいいと思っている

Finally, it is a pity that the system is not implemented. Otherwise, one could building a large set of tests to empirically evaluate the design.

- 理論にフォーカスしてるから実装はout-of-focus
- 実践的な実装とかその上での実験は次の研究でやります

# Review #478D
Overall merit
1.
Reject

Reviewer expertise
4.
Expert

Paper summary
The submission presents a potential solution to the space-efficient gradual-typing-with-polymorphism problem. More specifically, it proposes sacrificing full parametricity---where space efficient gradual typing has been shown to be impossible due to seals which hampers the ability to combine coercions---for "mostly parametric polymorphism", which disallows applying polymorphic values to the dyn type. With this relaxed requirement, previous techniques---a coercion calculus from Siek et al, and seals from Ahmed et al. to enforce parametricity at run time---can be mostly reused and extended with a few more rules to be made both polymorphic and space efficient. Formally, the submission models its ideas via a polymorphic calculus for the surface language with straightforward coercions, a space-efficient version, and a translation from the former to the latter. Finally, submission proves all the required properties that would be expected like soundness.

Comments for authors
I'm a big fan of gradual typing. It's already one of the biggest success stories to emerge from academic PL research in recent history, but some important practical issues are standing in the way of even more adoption. Thus I was pleased to see that someone is working on new ideas in this space, and in particular focusing on practical issues. Further, I agree with the main insight of the submission, which is that a dyn type argument probably doesnt need to be parametric to be useful, and the submission thoroughly develops the idea with formalisms that seem correct.

That being said, the presented formalisms seem like mostly straightforward extensions of previous calculi and on their own are not too technically interesting. Further, the formal aspects of gradual typing have already been thoroughly explored from pretty much every angle, so I think any new work needs to focus more on practical issues in order to move the state of the art forward. Thus, I was disappointed that, with the emphasis on a practically important issue such as space efficiency, the submission did not have any actual evaluation of its design decisions or even any way to run such an evaluation. Without looking at a real language with a real code base, one can only speculate on whether the insights of the submission are useful or not. Thus, without at least some practical evaluation of the design choice, I cannot recommend acceptance of the submission.

- choiceの部分は新規性で、しかもこの拡張によりいろんな性質がキチンと保たれるか？という問は全然straighforwardではない
- 非自明な点
- bisimulation
- coercion choiceがcompとかtransとかの既存の定義にsoundに整合するか(証明に100+pages)
- 理論にフォーカスしてる実践的な実装とかその上での実験は次の研究でやります

typos

p1 c1 ,, c2 two commas?
p6 "that that"
p8 "defined in straightforwardly"
p17 "sematics"