Isorecursion seems too weak

[RossTate]

Here are two class hierarchies that isorecursion (as just presented) seems to not support (but which nominal types support):

class A { A foo(B); }
class B extends A { override B foo(B); }

class X { X bar(); }
class Y extends X { Z z; override Y bar(); }
class Z { Y y; }

[tlively]

Once the slides from this morning's meeting are posted, it would be great if you could elaborate on how the system as presented fails in these cases. I tried to reason through it myself, but my memory/understanding of the presented subtyping details is too spotty :)

[rossberg]

As far as I can see, these examples are expressible just fine, provided we support nested recursive types as I alluded to (I didn't present the full Wasm syntax/rules for that, but you can extrapolate from the standard rules for iso-recursive types). All you have to do is wrap classes into another layer of type recursion:

;; $AB.$B <: $AB.$A
type $AB = (rec
  $A = (rec
    $inst = struct (ref $AB.$A.$vt)
    $vt = struct (ref $AB.$A.$foo)
    $foo = func (ref $AB.$A.$inst) (ref $AB.$B.$inst) -> (ref $AB.$A.$inst)
  )
  $B = (rec
    $inst = struct (ref $AB.$B.$vt)
    $vt = struct (ref $AB.$B.$foo)
    $foo = func (ref $AB.$A.$inst) (ref $AB.$B.$inst) -> (ref $AB.$B.$inst)
  )
)

;; $XYZ.$Y <: $XYZ.$X
type $XYZ = (rec
  type $X = (rec
    $inst = struct (ref $XYZ.$X.$vt)
    $vt = struct (ref $XYZ.$X.$bar)
    $bar = func (ref $XYZ.$X.$inst) -> (ref $XYZ.$X.$inst)
  )
  $Y = (rec
    $inst = struct (ref $XYZ.$Y.$vt) (ref $XYZ.$Z.$inst)
    $vt = struct (ref $XYZ.$Y.$bar)
    $bar = func (ref $XYZ.$X.$inst) -> (ref $XYZ.$Y.$inst)
  )
  $Z = (rec
    $inst = struct (ref $XYZ.$Z.$vt) (ref $XYZ.$Y.$inst)
    $vt = struct
  )
)

We can generalise this pattern to an extreme where we simply wrap the entire program's type section into one big type recursion. That would emulate the global recursive namespace that implicitly exists for nominal types -- the names correspond to the distinct paths inside the root type.

And as with nominal types, this global approach will break down at module/linking boundaries. Because in a modular system, "global" can only be "global wrt to a single module". There is no global name space beyond that. You'd need cyclic linking to allow name-based recursion to extend beyond module boundaries (which in turn requires a vastly different and more complex semantics for type recursion).

We can only have our cake and eat it too with equi-recursive types, because with those, each module in a recursive group can freely duplicate the types from other modules in its group, and linking will equate them. With iso or nominal, you'd have to break the recursion somehow, using anyref plus casts as elsewhere.

[RossTate]

I'll start with the easiest one. According to the subtyping slide of the presentation (link to slides for easy reference), (ref $t1.n1) can be a subtype of (ref $t2.n2) only if n1 equals n2. In my first example, A and B have to correspond to different indices of some rec type, and so cannot be subtypes. @rossberg's solution works with equi-recursive but not iso-recursive subtyping. (Side note: I designed my examples so that the complications of v-tables and this pointers would be unnecessary.)

For my second example, I made a mistake as I had forgotten that the subtyping rule allowed prefixing. This mistake can be rectified either by making Z extend another class that is only recursive with itself (in which case either Y or Z will have to be at index 2 and so cannot be a subtype of its superclass at index 1), or by having a self-recursive class extend another class from a pair of mutually recursive classes.

---

Besides these examples, there are some larger issues I should point out. One is that the rules provided are not reflexive. Consider the following:

(rec $X = (func (param (ref $X)))) <: (rec $Y = (func (param (ref $Y))))

According to the rules given, this subtyping holds only if (func (param (ref $X))) can be shown to be a subtype of (func (param (ref $Y))) assuming (only) $X <: $Y. But those types are contravariant with respect to $X/$Y, and as such the subtyping fails.

This can be fixed by adding a reflexivity rule, but it is also unknown if the given rules are transitive. Sure, that could be fixed by adding a transitivity rule, but at present it is unknown if this transitive closure is decidable. This paper claimed to have developed such an algorithmic formulation, but subsequent attempts to mechanize the proof of transitivity failed—this paper had to restrict isorecursive types to covariant fixpoints, thereby eliminating the example above entirely from the type system. Note that my example above would arise regularly in OO programs compiling to wasm due to the this argument for methods, so their restriction would not be well-suited to our needs.

These problems are well-known in the subtyping community. However, they are not as well known in the ML module community where the issues do not arise due to the focus on type equality rather than subtyping (as ML has no type-level subtyping).

---

These issues do not, however, arise with nominal types. The handwavy comparisons @rossberg makes seem to be due to related misunderstandings of subtyping systems. I might be wrong, but he has been asked on numerous occasions over multiple years, both in public and in private, to give concrete examples that would illustrate his concerns, and he has not. As a reminder to the group, at the in-person meeting he claimed that nominal types would require substantially more imports than structural types, but in #128 the problem was examined in more depth and the conclusion was that the two approaches would need roughly the same number of imports. Similarly, he has claimed that structural types would be necessary to support simple dynamic linking models, but in #156 a very simple approach to support such models with nominal types was offered and seemingly supported by many people. And in another presentation he claimed that C# would need host-provided type canonicalization and consequently structural types, but in #215 I (who, unlike him, have actually implemented a C# runtime, and on a typed backend no less) explained why C# would not need or even be helped by such a feature and in fact would find it a hindrance to representing its own internal data structures.

It is demeaning, demoralizing, and counterproductive to have the champion act as if such discussions never took place and continue to spread unsubstantiated claims. Since I do not know who has observed these conversations or the relevant corrections to his presentations, it puts me in a position where every time he makes such claims in new places (such as in this thread) I feel I need to inform people about the actual status quo (as I am doing now) to provide appropriate context and prevent further spread of misinformation, which distracts from the topic at hand. If the champion still believes such claims, I would ask that he would back them up in the many locations that explicitly requested such evidence and insight from him. But this thread is about the limitations of isorecursive subtyping, not (perceived) limitations of nominal subtyping, and as such I would ask @rossberg to refrain from making negative comments about nominal types so that we can stay on topic.

---

Moving on.
@tlively: Did I manage to illustrate why the examples do not work (correcting my second example as above).
@rossberg: Do you have any technical corrections to make to my comments regarding isorecursive types?
@dtig: If my comment above is inappropriate conduct, please let me know and I will correct it.

[tlively]

So working through the first example:

class A { A foo(B); }
class B extends A { override B foo(B); }

We can simplify @rossberg's lowering to ignore vtables and this pointers, i.e. just have the structs contain the methods directly:

type $AB = (rec
  $A = (rec
    $inst = struct (ref $AB.$A.$foo)
    $foo = func (ref $AB.$B.$inst) -> (ref $AB.$A.$inst)
  )
  $B = (rec
    $inst = struct (ref $AB.$B.$foo)
    $foo = func (ref $AB.$B.$inst) -> (ref $AB.$B.$inst)
  )
)

Now we can check that $AB.$B.$inst <: $AB.$A.$inst (working bottom-up):

$AB.$B <: $AB.$A  ⊢ $AB.$B <: $AB.$A ∧ 0 = 0

---

$AB.$B <: $AB.$A ⊢ (ref $AB.$B.$inst) <: (ref $AB.$A.$inst) ∧
$AB.$B <: $AB.$A ⊢ (ref $AB.$B.$inst) <: (ref $AB.$B.$inst) [reflexive]

---

$AB.$B <: $AB.$A ⊢ $AB.$B.$foo <: $AB.$A.$foo ∧
$AB.$B <: $AB.$A ⊢ $AB.$B.$inst <: $AB.$A.$inst [note: this is where we started. How to avoid diverging?]

$AB.$B <: $AB.$A ∧ 1 = 1

---

(ref $AB.$B.$foo) <: (ref $AB.$A.$foo)

---

$AB.$B.$inst <: $AB.$A.$inst

This almost seems to work given the extension to nested recursion (which we should certainly formalize somewhere to make sure we are all talking about the same thing) and the addition of a reflexivity rule. The only issue is that it looks like we have to prove $AB.$B <: $AB.$A ⊢ $AB.$B.$inst <: $AB.$A.$inst in order to prove $AB.$B.$inst <: $AB.$A.$inst, which seems circular. @rossberg, can you suggest a fix for this or see where I went wrong?

@RossTate, it does look like allowing nested recursive types resolves the problem you spotted with the indices needing to match, but may not resolve the problem above. Does that agree with your understanding?

---

I was curious about the decidability and looked at the second paper you linked to above, @RossTate. Here's the relevant section from page 26:

The soundness of the Amber rule (Sub Rec) is hard to prove syntactically [33] – in particular proving the transitivity of subtyping in the presence of the Amber rule requires a very complicated inductive argument, which only works for “executable” environments, as well as spurious restrictions on the usage of type variables in the rules (Sub Refl*), (Kind And Pub 1), (Kind And Pub 2), (Kind Or Tnt 1), (Kind Or Tnt 2), (Sub And LB 1), (Sub And LB 2), (Sub Or UB 1), (Sub Or UB 2). We use the simpler (Sub Pos Rec*) rule, which is much easier to prove sound and requires no restrictions on the other rules. It resembles (Sub Univ*), our rule for subtyping universal types, with the additional restriction that the recursive variable is not allowed to appear in a contravariant position (such as α → T).

I don't have the full context here, so I can't really judge for myself how relevant this is to our current situation. Are we affected by the mentioned "spurious restrictions on the usage of type variables" given that we don't have type variables in the language? Or is that talking about type metavariables in the rules? Would the proof that "only works for 'executable' environments" work for us?

[RossTate]

Thank you very much, @tlively, for the insightful post and for pushing the discussion forward!

---

So the issue with handwaving extensions is that 1) the ambiguity can lead to different people inferring different extensions, and 2) we have no understanding of the expressiveness and decidability properties of the extensions. In this case, you and I have inferred different extensions with different decidability properties. I'll elaborate below, using your simplified example (repeated here so that people don't have to scroll up and down):

type $AB = (rec
  $A = (rec
    $inst = struct (ref $AB.$A.$foo)
    $foo = func (ref $AB.$B.$inst) -> (ref $AB.$A.$inst)
  )
  $B = (rec
    $inst = struct (ref $AB.$B.$foo)
    $foo = func (ref $AB.$B.$inst) -> (ref $AB.$B.$inst)
  )
)

---

The extension I inferred is for a subtyping like (ref $t.m1.n1) <: (ref $t.m2.n2) to hold, it must be the case that the "path" m1.n1 equals m2.n2, i.e. m1 must equal m2 and n1 must equal n2. I inferred this due to my familiarity with (Scala's) path-dependent types (though only loosely related) and due to the observation that nested recursive types like your example can be flattened to

type $AB = (rec
  $A_inst = struct (ref $AB.$A_foo)
  $A_foo = func (ref $AB.$B_inst) -> (ref $AB.$A_inst)
  $B_inst = struct (ref $AB.$B_foo)
  $B_foo = func (ref $AB.$B_inst) -> (ref $AB.$B_inst)
)

With my inferred extension, the subtyping $AB.$B.$inst <: $AB.$A.$inst fails because the two paths are distinct. This may not be the extension that was intended, but by the flattening observation above I can be reasonably assured that the computational properties of the extension haven't changed extensively.

---

Now your inferred extension is perfectly reasonable too (as there's an easy way to fix the digression problem—the presentation was a little imprecise with its formulation). However, it seems to have very different computational properties. To see why, observe that your definitions for $foo could simply be inlined into those for $inst since $foo is accessed in a very limited fashion:

type $AB = (rec
  $A = (rec
    $inst = struct (ref (func (ref $AB.$B.$inst) -> (ref $AB.$A.$inst)))
  )
  $B = (rec
    $inst = struct (ref (func (ref $AB.$B.$inst) -> (ref $AB.$B.$inst)))
  )
)

Consider then, why have the layer of indirection and what is it doing? It's definitely doing something since eliminating it results in the following, for which the subtyping breaks:

type $AB = (rec
  $A = struct (ref (func (ref $AB.$B) -> (ref $AB.$A)))
  $B = struct (ref (func (ref $AB.$B) -> (ref $AB.$B)))
)

Well, let's consider another minimized example:

type $UV = (rec
  $0 = (rec $inst = struct i32)
  $1 = (rec $inst = struct f64)
)
type $VU = (rec
  $0 = (rec $inst = struct f64)
  $1 = (rec $inst = struct i32)
)

Now, by the same reasoning you gave, you can prove that $UV.$0.$inst is a subtype of $VU.$1.$inst and vice versa, and similarly that $UV.$1.$inst is a subtype of $VU.$0.$inst. So we've (partially) solved the reordering problem: just wrap a singleton rec around each of the components of a rec. However, that comes at a price. In particular, $UV.$0.$inst is equivalent to $VU.$1.$inst without being syntactically identical (even up to alpha renaming), which means we no longer have the cheap canonicalization property that we were supposed to get from isorecursive types.

---

I don't know which of the two inferred interpretations @rossberg intended, or if there was another neither of us came up with, but it seems either the extension is insufficiently expressive or it is too expressive to preserve the cheap canonicalization property of isorecursive types. In fact, it seems like any extension that would make it possible for one index to be a subtype of another would also make it possible for the two indices to be equivalent and consequently would seem to break the cheap canocialization property that has led us to consider isorecursive types in the first place.

[rossberg]

Okay, let's flesh this out. The following rules for (higher-kinded) subtyping on type tuples and iso-recursive types are fairly standard:

    (A ⊢ t1 <: t2)*
----------------------- [tup]
A ⊢ ⟨t1*⟩ <: ⟨t2* t2'*⟩

  A ⊢ t1 <: t2
---------------- [proj]
A ⊢ t1.n <: t2.n

A, α1 <: α2 ⊢ t1 <: t2
---------------------- [rec]
 A ⊢ μα1.t1 <: μα2.t2

t1 <: t2 ∈ A
------------ [assump]
A ⊢ t1 <: t2

To deal with tuple-kinded iso-recursion, you will want one more rule, something like the following:

A, α1.n1 <: α2.n2 ⊢ t1*[n1] <: t2*[n2]
-------------------------------------- [rec-proj]
 A ⊢ (μα1.⟨t1*⟩).n1 <: (μα2.⟨t2*⟩).n2

So recursive types are not entirely rigid at tuple kind, we allow beta reduction of projections across μ. This is fairly weak but still inductive. (A is relating not just variables but paths now.)

Turning back to the example, we have to be a bit more precise about what are type definitions and what are internal variables. So let me enrich the notation and make the rec variables explicit (this wouldn't need to be explicit in the text or binary format, but the semantics needs to keep the distinction straight):

type $AB = (rec $ABself
  $A = (rec $Aself
    $inst = struct (ref $ABself.$A.$foo)
    $foo = func (ref $ABself.$B.$inst) -> (ref $ABself.$A.$inst)
  )
  $B = (rec $Bself
    $inst = struct (ref $ABself.$B.$foo)
    $foo = func (ref $ABself.$B.$inst) -> (ref $ABself.$B.$inst)
  )
)

Now we can derive $AB.$B.$inst <: $AB.$A.$inst (where $AB is not a variable but equal to the rec type above) as follows:

⊢ $AB.$B.$inst <: $AB.$A.$inst
-------------------------- [proj]
⊢ $AB.$B <: $AB.$A
-------------------------- [rec-proj] [struct] [func]
$ABself.$B <: $ABself.$A ⊢ (ref $ABself.$B.$inst) <: (ref $ABself.$A.$inst) ∧
$ABself.$B <: $ABself.$A ⊢ (ref $ABself.$B.$inst) <: (ref $ABself.$B.$inst) [refl]
-------------------------- [ref]
$ABself.$B <: $ABself.$A ⊢ $ABself.$B.$inst <: $ABself.$A.$inst
-------------------------- [proj]
$ABself.$B <: $ABself.$A ⊢ $ABself.$B <: $ABself.$A [assump]

There is no loop here, since the latter goal is on mere paths, not the original projections from rec types (also, A has been extended).

nested recursive types like your example can be flattened

definitions for $foo could simply be inlined

No. Neither of these transformations is valid with iso-recursive types. For starters, they wouldn't even preserve kinds.

However, it is true that the inner recursions aren't used, so one could simplify inner rec's to plain type tuples.

In particular, $UV.$0.$inst is equivalent to $VU.$1.$inst without being syntactically identical

They're equivalent only if you add an antisymmetry rule as an axiom.

You are right, though, that transitivity is not immediately obvious, so will need some checking. However, I don't think that the papers you pointed to are a strong signal to the contrary, since they define waaaaay richer type systems, with full-blown dependent types, unions, intersections, and refinements, which make transitivity difficult to establish for plenty of other reasons.

---

That all being said, I want to stress the other observation I made above: in general, we won't be able to compile mutually recursive classes to Wasm without breaking up the inter-class recursion (except with equi-recursive types ;) ). So these examples are kind of useless as a general compilation scheme anyway. Given that, I am not convinced it's even worth supporting nested recursion/tuples like this.

[RossTate]

To deal with tuple-kinded iso-recursion, you will want one more rule, something like the following:

A, α1.n1 <: α2.n2 ⊢ t1*[n1] <: t2*[n2]
-------------------------------------- [rec-proj]
A ⊢ (μα1.⟨t1*⟩).n1 <: (μα2.⟨t2*⟩).n2

Yeah, this is the extension that I showed @tlively's interpretation effectively enabled. But, as I pointed out, it completely changes the metatheoretic properties of the system. For example, even ignoring reflexivity/transitivity issues, this extension changes the complexity from linear time to quadratic time. But the following is probably the more important impact of this extension.

They're equivalent only if you add an antisymmetry rule as an axiom.

You seem to be suggesting that, in addition to subtype equivalence (i.e. the two types are subtypes of each other), there would be another equivalence relation. Subtype equivalence is what matters for type-checking, so what would be the purpose of this other equivalence relation? From context, it sounds like this other equivalence relation is meant to indicate when rtt.canon needs to return the same two types. But if that other equivalence relation can be weaker than subtype equivalence to serve the purposes of rtt.canon, then why can't it be arbitrarily weaker? For example, V8's prototype implementation essentially defines this weaker relation to hold only when the type index is the same, and that's currently working just fine. If you're alright with rtt.canon not using subtype equivalence, it begs the question of what the purpose of rtt.canon even is? (#215 would be the appropriate place to follow up on that question, rather than here.)

You are right, though, that transitivity is not immediately obvious, so will need some checking. However, I don't think that the papers you pointed to are a strong signal to the contrary, since they define waaaaay richer type systems, with full-blown dependent types, unions, intersections, and refinements, which make transitivity difficult to establish for plenty of other reasons.

There are other efforts that simply failed (and hence are not published). This paper illustrates that the other complexities were fairly inconsequential—just the isorecursion was problematic (hence the problem was solved by solely restricting isorecursion).

That all being said, I want to stress the other observation I made above: in general, we won't be able to compile mutually recursive classes to Wasm without breaking up the inter-class recursion (except with equi-recursive types ;) ).

You are repeating the same unsubstantiated claim you made above even after I explained why this was problematic and specifically requested you not to do so. Your winky face suggests you are aware that this is inappropriate but somehow think this is cute—you did the same thing in this inappropriate comment as well. Please stop this belittling and counterproductive behavior.

So these examples are kind of useless as a general compilation scheme anyway. Given that, I am not convinced it's even worth supporting nested recursion/tuples like this.

This seems dismissive. As I've pointed out before, String is mutually recursive with Object in Java/C#/Kotlin/Scala. It is also a class that extends Object, corresponding to my first example. And Object needs to be extended by other classes, corresponding to a correction I gave of my second example. So dismissing the importance of these examples is dismissing the needs of many of the most popular languages we would like WebAssembly to support. Maybe this was not the intent of this comment, but this is how it came across to me.

[tlively]

Thanks for fleshing those rules out, @rossberg! For the rec-proj rule, I was initially confused about why it was valid to add α1.n1 <: α2.n2 to the assumptions when we are trying to prove the conclusion A ⊢ (μα1.⟨t1*⟩).n1 <: (μα2.⟨t2*⟩).n2 because I thought that α1.n1 <: α2.n2 was just another way of writing (μα1.⟨t1*⟩).n1 <: (μα2.⟨t2*⟩).n2. But then I remembered that you were careful to make a distinction between paths and type variables, so I now understand these to not be the same. I will have to work with this more to develop an intuition for it, but it makes sense to me so far.

this extension changes the complexity from linear time to quadratic time

@RossTate, can you explain how this rule changes the complexity to quadratic? Also, to clarify, is this the complexity to check the subtype relation between two types?

You seem to be suggesting that, in addition to subtype equivalence (i.e. the two types are subtypes of each other), there would be another equivalence relation.

I'm not sure this is what @rossberg is suggesting. @RossTate, can we roll back this line of conversation a bit and can you re-explain the problem of loss of simple canonicalization in light of the newly fleshed-out subtyping rules?

I also agree that this thread is not the place to discuss rtt.canon or any of the larger questions you alluded to. Let's keep this thread focused on figuring out how to make isorecursive types work, regardless of whether we think that is a good idea in the grand scheme of things. @rossberg, let's also keep this thread focused on closed-world compilation without any module linking concerns, where @RossTate's examples are perfectly salient and important to figure out. Once we are all on the same page about how iso-recursive types will work in the simple case, we can expand the discussion to consider the implications for separate compilation and linking.

[RossTate]

Thanks, @tlively, for helping so much with the discussion!

can you explain how this rule changes the complexity to quadratic? Also, to clarify, is this the complexity to check the subtype relation between two types?

On my end, I see a mistake I made. In my head, I automatically "fixed" the ref-proj rule. As it is stated above, it does not increase the complexity, but it also is no longer analogous to the rules in the slides nor to your intepretation of nested recursive types, and as a consequence is much too weak.

To see why, consider that it's requirement is to prove A, α1.n1 <: α2.n2 ⊢ t1*[n1] <: t2*[n2]. Note that the subtyping of the type components can only assume the subtyping between the projections α1.n1 <: α2.n2. But what if the subtyping of these components would hold if were to relate other projections as well? In the rules from the slides, in order to derive (μα1.⟨t1*⟩).n <: (μα2.⟨t2*⟩).n we could assume α1.1 <: α2.1, ..., α1.k <: α2.k when proving t1*[1] <: t2*[1] ... t1*[k] <: t2*[k]. That is, we could make assumptions about multiple projections (provided we prove the corresponding type components are subtypes), not just the projection n at hand, whereas ref-proj is restricted to just the projection-pair at hand, making it much too weak.

The fix to this is to permit ref-proj to be able to make assumptions about multiple projection-pairs and prove the correspond type components are subtypes. The issue with this, though, is that unlike the rules in the slides it is no longer obvious which projection-pairs to make assumptions about (i.e. it's no longer simple "1 relates to 1 and 2 relates to 2 and ..."). The way to address this algorithmically is that you start by attempting to prove A, α1.n1 <: α2.n2 ⊢ t1*[n1] <: t2*[n2] but, if you discover you need to make an assumption about any projection-pair, you then also prove those type components are subtypes, and again keep adding obligations for every assumption you need to make. Because there are n^2 potential projection-pairs, this terminates in quadratic time. (However, the same is not true when you permit generics and non-uniform recursion because there can be infinite obligations to check.)

Recall that equirecursive subtyping is also quadratic. That's no coincidence—you can encode equirecursive subtyping in this extended version of isorecursive subtyping. Each type component essentially corresponds to a state of the automata representation of an equirecursive type, and the collection of projection-pairs that end up getting assumed forms the bisimulation relation between these states. So we're back to where we came from.

The question, then, is what is the impact of this on canonicalization?

can we roll back this line of conversation a bit and can you re-explain the problem of loss of simple canonicalization in light of the newly fleshed-out subtyping rules?

So rec types are essentially specifying DFAs where the states are explicitly numbered. With the rules in the presentation, two rec types can be equivalent, i.e. subtypes of each other, only if their DFAs were the same with the same numbering. And likewise for projections of rec types. For canonicalization, that means your hash function for a rec type can use the numbering of the states, and then your hash function for a projection can simply combine the rec type's hash with the projection index. In other words, there is a simple syntax with the property that two types are equivalent if and only if they are syntactically identical.

However, once we add rules that can make projections of different indices subtypes, then there is no such syntax because distinct projections can be equivalent. For example, rec types $A and $B can define the same DFA with different ordering and so themselves not be equivalent, but if $B reordered $A's first state to be $B's third state, then the projections $A.1 and $B.3 are equivalent. That is, $A.1 and $B.3 can be used completely interchangeably for the purposes of type-checking despite being syntactically distinct.

[tlively]

@RossTate, I don't quite understand your argument for why ref-proj is too weak. Can you show an example where it fails?

[RossTate]

Sure thing. The following is a variant on my first example (whose primary challenge is relating types within the same recursion grape):

class A { B b; A foo(); }
class B extends A { override C foo(); } // inherits field B b
class C extends A { override B foo(); } // inherits field B b

If you consider why this type-checks nominally, the fact that B can extend A depends on the fact that C (not B this time) is a subtype of A. So the projection-pair subtyping for B <: A depends on the projection-pair subtyping C <: A. But rec-proj only allows projection-pair subtypings to depend on themselves. (For fun, in this example I also made the projection-pair subtyping for C <: A depend on B <: A so that we still have a cycle of projection-pair subtyping dependencies.)

That's the intuition. I'll reformulate the example with the notation we've been using above:

type $ABC = rec $ABCself
  $A = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$A]))
  $B = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$C]))
  $C = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$B]))

Now for the subtyping:

⊢ $ABC.$B <: $ABC.$A
-------------------------- [rec-proj] [struct] ([refl] | [func])
$ABCself.$B <: $ABCself.$A ⊢ (ref $ABCself.$C) <: (ref $ABCself.$A)
-------------------------- [ref]
$ABCself.$B <: $ABCself.$A ⊢ $ABCself.$C <: $ABCself.$A
><
failure - mismatch between assumed subtyping and goal subtyping

Does that clarify, @tlively?

[fgmccabe]

Fun fact: I tested the scenario in Java. It compiles and works as expected! Francis

…

On Mon, May 24, 2021 at 11:20 AM Ross Tate ***@***.***> wrote: Sure thing. The following is a variant on my first example (whose primary challenge is relating types within the same recursion grape): class A { B b; A foo(); } class B extends A { override C foo(); } // inherits field B b class C extends A { override B foo(); } // inherits field B b If you consider why this type-checks nominally, the fact that B can extend A depends on the fact that C (not B this time) is a subtype of A. So the projection-pair subtyping for B <: A depends on the projection-pair subtyping C <: A. But rec-proj only allows projection-pair subtypings to depend on themselves. (For fun, in this example I also made the projection-pair subtyping for C <: A depend on B <: A so that we still have a cycle of projection-pair subtyping dependencies.) That's the intuition. I'll reformulate the example with the notation we've been using above: type $ABC = rec $ABCself $A = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$A])) $B = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$C])) $C = struct (mut (ref $ABCself.$B)) (ref (func [] -> [ref $ABCself.$B])) Now for the subtyping: ⊢ $ABC.$B <: $ABC.$A -------------------------- [rec-proj] [struct] ([refl] | [func]) $ABCself.$B <: $ABCself.$A ⊢ (ref $ABCself.$C) <: (ref $ABCself.$A) -------------------------- [ref] $ABCself.$B <: $ABCself.$A ⊢ $ABCself.$C <: $ABCself.$A >< failure - mismatch between assumed subtyping and goal subtyping Does that clarify, @tlively <https://github.com/tlively>? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#217 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAQAXUAPSPXVWCOIHE6MNCLTPKKFNANCNFSM45DALP4A> .

-- Francis McCabe SWE

[tlively]

Got it, thanks, @RossTate! I am convinced that the subtyping rules with rec-proj are too weak to show that B <: A in the example above. @rossberg, do you concur or is there something we've missed?

[rossberg]

@tlively, yes, the rules are too weak for that example.

So, let me try to summarise what I believe we now all agree on:

1. The semantics as sketched, including the rec-proj rule, is inductive and does allow canonicalization as expected.

2. It can directly express the examples in the OP.

3. There are examples of nested mutual recursion that it cannot express without falling back to casts, like the one Ross gave later.

4. It cannot handle any mutual recursion across module boundaries without casts.

5. Only equi-recursive types can do the latter (in Wasm's given framework of AOT compilation and linking).

So the concern boils down to how relevant we consider limitations (3) and (4). Personally, I don't think they would be deal breakers. Again, insert my standard reminder that there will always be things that our type systems won't be able to express and where we will have to fall back to casts. And regarding this particular case, cycles of this sort are not super common, and even less so the forward edges in them, so casts to deal with forward references would not seem very likely to have relevant performance impact on real code. (To Take Ross' example of Object.toString, the overhead of executing that method will surely dominate any down cast to String in the end. If not, we'd have much more serious problems elsewhere.) Though of course this should be confirmed through some experimentation.

What I suspect matters more in practical terms is whether extra handling of forward references complicate producers significantly. The answer to that is less obvious. One experiment I plan to do is to prototype iso-recursive types in the reference interpreter and in the Wob compiler, to get a better insight into the impact they'd have.