T-AppDiamond

[Tantalus13A98B5F]

Notes following today's discussion.

Consider applying a function of type $(T^{\blacklozenge r} \to Q)^q$ to an argument of type $T^p$. By converting this function type to a type suitable for T-App $\blacklozenge$, we require $\blacklozenge(p\cap q) <: \blacklozenge r$. Alternatively said, we project $p$ over the domain of $q$ as $\blacklozenge(p\cap q)$, and then require the overlap to be a subtype of $\blacklozenge r$ as we do in an everyday application.

However, considering a concrete example, and we will find that subtyping is not sufficient here. We take the hypothetic context $\Gamma = [\ldots b, c, d, e$ are fresh $\ldots, a: T^{d,e}, x: T^{a,b,c}, f: (T^{\blacklozenge a,b}\to Q)^x]$, where function $f$ should permit arguments of $a, b$, or fresh, but not $c$. In checking $f(c)$, we check $c \cap x = c <: a, b$, which fails as expected. However, in checking $f(a)$, we check $a \cap x = a <: a, b$, which should but is not working, due to the fact that saturated overlapping upcasted $a$, making it no longer bounded by $a$ itself.

https://github.com/Kraks/diamond-lang/blob/04ac2114201a2d4014ef38b9a0559d4c956c57f2/src/main/scala/qualfsub/TypeCheck.scala#L391-L399

Our current implementation takes the approach replacing $r$ on the right side with $r$ (see .sat on L396). By doing so we are able to type check $f(a)$ since now we are checking $a \cap x = a <: (a, b) $, which is working. However, this is not the subtyping relation we have in the base system, by which we are allowing castings unseen in the paper. This also brings up inconsistent behaviour. Suppose we have another function $g: (T^{a,b}\to Q)^x$, then we are able to check $g(a)$, $g(b)$, but not $g(d)$ since $d <: a, b$ is required in the non-fresh application but it fails. If this is a desired behavior, we are losing it since we can type check $f(d)$ where $d\cap x = d <: (a, b)* $.

We are looking into several ways to resolve this issue,

• Justify the saturation $r*$ in the current system.
• Leave the saturation or not choice to end users, i.e. permit users to write saturation markers in qualifiers.
• Seek non-saturated overlapping.

[Kraks]

The issue can also be exemplified by a simpler example (https://github.com/Kraks/diamond-lang/blob/04ac2114201a2d4014ef38b9a0559d4c956c57f2/src/test/scala/diamond/Diamond.scala#L206C35-L206C35)

val x = Ref 42;                                                                                 
val y = x;
// f: (Ref^{<>, y} => Int)^x
def f(z: Ref[Int]^{<>, y}): Int = (! x) + (! z);

Then consider application f(x) (or f(y)), both the argument qualifier and function qualifier share x. We want to check if this overlap x is permitted by the user-annotated function parameter qualifier {<>, y}. The user annotation communicates the intention that any value aliased with y should be allowed. However, simply check {x} <: {<>, y} would not work. So, the current implementation chooses to check inclusion after computing saturation on the user-annotated function parameter qualifier {x} <: {<>, y}*, which is to check {x} <: {<>, x, y}.

The issues are

• Can this implementation choice be justified by the declarative system?
• If not, how do we allow such cases?

[Kraks]

but on non-fresh application this is not possible since d <: a, b fails; should this be expected?

Non-fresh application would not work here since it requires non-fresh for parameter/argument qualifiers.

[Tantalus13A98B5F]

Revised the text. For the non-fresh application we consider another function with the appropriate paramter type.

[Kraks]

a* ∩ x* <: {a, b}*, which is working, However, this is not the subtyping relation we have in the base system

The way I see it is that the issue is not about subtyping, since the implementation does not invent a new subtyping rule. But it has a way of using subtyping rules as a premise in its "algorithmic" T-App<>. The issue is if this "algorithmic" T-App<> can be justified by the declarative T-App<>.

To make it clear, the implemented "algorithmic" T-App<> can be expressed in this way:

Γ^ϕ ⊢ t1 : (f(x: T^r1 -> U^r2))^q
Γ^ϕ ⊢ t2 : S^r3
<> ∈ r1
q* ∩ r3* <: r1*
S <: T
<> ∈ r3 ⇒ x ∉ FV(U)
<> ∈ q  ⇒ f ∉ FV(U)
r2 ⊆ ϕ ∪ {<>, x, f}
-------------------------------
 <as in the decl rule>

Note that in the declarative T-App<>, we just "guess" a p and q simultaneously and we use <>(p* ∩ q*) as the function parameter qualifier to type the function. And crucially, <>(p* ∩ q*) is already saturated since the intersection of two saturated sets is also saturated. However the user may not need to annotate the function parameter with saturated sets. In my intuition, this somehow justifies the saturation over r1 in the implementation.

This also brings up inconsistent behaviour. Suppose we have another function $g: (T^{a,b}\to Q)^x$, then we are able to check $g(a)$, $g(b)$, but not $g(d)$ since $d <: a, b$ is required in the non-fresh application but it fails. If this is a desired behavior, we are losing it since we can type check $f(d)$ where $d\cap x = d <: (a, b) $.

Not sure I follow this part. For non-fresh applications, g(d) indeed should not be allowed, right? Why we are "losing it"?

[Tantalus13A98B5F]

And crucially, <>(p* ∩ q*) is already saturated since the intersection of two saturated sets is also saturated.

My reading this is that this explains why we need r1*, but not why we can have r1*. The way to testify is that we have a full declarative derivation tree to type any of our examples.

Note that in the declarative T-App<>, we just "guess" a p and q simultaneously and we use <>(p* ∩ q*) as the function parameter qualifier to type the function.

When we are guessing, f is still a function within the context, and our guessing can only be up to T-Sub. I don't think we are able to avoid declarative subqualifier here.

For non-fresh applications, g(d) indeed should not be allowed, right? Why we are "losing it"?

As expected g(d) is not allowed, but r1* is allowing f(d), which may cause a slight inconsistency.

[Kraks]

My reading this is that this explains why we need r1, but not why we can have r1. The way to testify is that we have a full declarative derivation tree to type any of our examples.

Some proof or derivation would be good. My thinking is that we can have r1* because this is how the declarative T-App<> assigns qualifiers for the parameter of function types.

When we are guessing, f is still a function within the context, and our guessing can only be up to T-Sub. I don't think we are able to avoid declarative subqualifier here.

This is only true when f is in the top-level context. Otherwise, we can "backtrack" and "guess" a better typing assignment for f in the context.

As expected g(d) is not allowed, but r1* is allowing f(d), which may cause a slight inconsistency.

But this is still consistent with the declarative system, right?

[bracevac]

However, simply check {x} <: {<>, y} would not work. So, the current implementation chooses to check inclusion after computing saturation on the user-annotated function parameter qualifier {x} <: {<>, y}*, which is to check {x} <: {<>, x, y}.

The issues are

* Can this implementation choice be justified by the declarative system?

* If not, how do we allow such cases?

This sounds wrong, because it amounts to "for the algorithmic application, I am going to pretend I first made an upcast of the function so that I check the argument by subtyping against {<>, y}*". Which is to say we implicitly assumed the subtyping step

f(Ref^{<>, y} => Int)^x <: f(Ref^{<>, y}* => Int)^x

By contravariance, this amounts to

{<>, y}* = {<>, x,y} <: {<>, y}

which does not seem generally true.

I would have expected that an algorithmic rule would check that the overlap is a subqualifier the exact domain qualifier, and not its saturated version. That is at least if you are after the algorithmic version of the POPL paper's calculus.

So, the declarative system will reject f(x) but accept f(y), because that's what the user annotated and how reachability currently works. One stance is that reachability simply isn't aliasing, but a stronger notion, period.

But could we have it behave more like aliasing here? I think there is a bit of a tension between how we expect subtyping and overlap checking to behave, e.g., should the type (Ref^{<>, y} => Int)^x be semantically the same as (Ref^{<>, x,y} => Int)^x? One could certainly try a soundness proof with a version of function application that treats them the same.

[TiarkRompf]

Accepting f(x) would be blatantly unsound -- consider a slight variation of the example:

val x = Ref 42
def g(y: (A=>A)^x) = { // y looks like it reaches x
  def f(z: Ref[Int]^{<>, y}): Int = (! x) + (! z);
  ...
g(a=>a) // oops, y does not actually reach x

[Tantalus13A98B5F]

val x = Ref 42;                                                                                 
val y = x;

Assume the above definitions, we can have diversed application behavior below (saturation of argument qualifier is made explicit by y*; otherwise argument qualifers are not saturated)

applies to	x	y
def f(z: Ref[Int]^{<>, y}) = (! x) + (! z)	no	no	$y^ \cap x^ = x \nsubseteq y$
def f(z: Ref[Int]^{<>, y}) = (! y) + (! z)	no	no	$y^ \cap y^ = xy \nsubseteq y$
def f(z: Ref[Int]^{y}) = (! x) + (! z)	no	yes
def f(z: Ref[Int]^{y}) = (! y) + (! z)	no	yes
def f(z: Ref[Int]^{<>, y*}) = (! x) + (! z)	yes	yes	$x^ \cap x^ = x \subseteq y^* = xy$
def f(z: Ref[Int]^{<>, y*}) = (! y) + (! z)	yes	yes	$y^ \cap y^ = xy \subseteq y^* = xy$
def f(z: Ref[Int]^{y*}) = (! x) + (! z)	yes	yes
def f(z: Ref[Int]^{y*}) = (! y) + (! z)	yes	yes

[TiarkRompf]

Edit: I believe the first two could/should also support calling f(y) via the non-fresh rule.

Makes sense -- though the last four entries use y* as part of the qualifier syntax, which is not something the current formalization models.

I believe it could be added (as part of a 'syntactic qualifier' system -- i.e. give qualifier expressions syntactic structure) but we'd need to pin down the semantics precisely. The baseline could be a form of 'macro expansion', i.e., treating y* as syntactic sugar for y,x. Connected to this, one could look at adding complement, intersection and other ops in a user-facing way.

However, this seems to be a project on its own.

[Kraks]

Thanks, @bracevac and @TiarkRompf -- I can see the issue of allowing f(x) in that variant example.

But I do think we want to allow f(y) in the example (as well as in the first two lines of Sonlin's table), which seems to be not allowed by the T-App-Fresh rule. The non-fresh T-App rule could do that by upcasting the function type (narrowing the contravariant qualifier). This also leads to the issue of how the type checker decides which T-App rule to use, and it seems some heuristics/backtracking is needed.

[Tantalus13A98B5F]

Regarding the combination of T-App-NonFresh, we are able to construct a slightly more complex example,

val c = Ref 42
val b = c
val a = Ref 42
val p = if (...) a else b
def f(x: Ref[Int]^{◆, b}) = (! x) + (! b)
f(p)  // will not type check

Intuitively f(p) should work, as b is permitted by argument type and a is separated from f.

On the non-fresh path, $p <: a, b <: b$ does not go through

On the fresh path, $p^ \cap b^ = b^* = b, c <: b$ does not go through either.

[TiarkRompf]

How about the following:

1. if $q_x <: q_1$ and $q_x$ is non-fresh do a non-fresh app (as before)
2. if $q_x^{* \setminus q_1} \cap q_f^{*} <: q_1$ do a fresh app -- here $*\setminus q_1$ means that we compute the $*$ on $q_x$ in an environment $\Gamma \setminus q_1$, i.e., stop the transitive computation whenever an $x \in q_1$ is reached.

Note:

1. if the $x \in q_1$ aren't included in the transitive expansion of $q_x$, then it seems the formula simplifies to $q_x^{* \setminus q_1} \cap q_f^{*} <: \emptyset$
2. it's an interesting question if $q_f^{*}$ should also be adapted in this way -- I think this would be wrong, but we should look at some examples to be sure

[Tantalus13A98B5F]

I think this is reasonable, and will make applications very natural. Would be best if we can have some soundness evidence.

2. Counterexample: $x^{*\backslash \blacklozenge y} \blacklozenge\cap y^{*\backslash \blacklozenge y} = x \cap y = \emptyset <: \blacklozenge y$

val x = ref 42
val y = x
def f(z: Ref[Int]^⧫y)^y = ...
f(x)  // should not but works

[TiarkRompf]

Would be best if we can have some soundness evidence.

Yes, it should be straightforward to try on this file: https://github.com/YuyanBao/DependencyTracking/blob/main/coq/dev/LR/stlc_reach_ref_overlap_self_fresh_mut.v

Edit: biggest immediate question is if the internal environment invariant, which is currently symmetric (https://github.com/YuyanBao/DependencyTracking/blob/main/coq/dev/LR/stlc_reach_ref_overlap_self_fresh_mut.v#L507), is still sufficient for the proof.

[Tantalus13A98B5F]

Concerning that $*\setminus q_1$ might be too heavyweight for the declarative system, we can use an alternative criterion,

$q_x <: q_x' \qquad (q_x'\setminus q_1)^*\cap q_f^* \subseteq \varnothing$

I'm not sure if we can hide $q_x <: q_x'$ as in the non-fresh TApp rule, but this makes dependent application explicit.