Difference between rec groups of size one and types without rec groups?

[tlively]

When we first landed the isorecursive type system we decided to make types defined without rec groups identical to the corresponding types defined in singleton rec groups. At the subgroup meeting today there was a question of whether that should be revisited. @rossberg, are you aware of any reason to revisit that decision? (If so, are there existing discussions of this that I missed?)

[titzer]

What's the alternative to them being in singleton recursion groups?

[tlively]

One alternative is to disallow them from being recursive at all. In contrast, types in singleton recursion groups can reference themselves. I still don't know of any benefit to making that distinction, but perhaps I'm missing something.

[takikawa]

I see the benefit in unifying these things for a cleaner treatment in the spec and make equality more straightforward, but from an implementation perspective I think there are ways in which separating them would be easier. For example, you don't have to set anything up to parse a potential recursive reference if you don't see a rec typecode in the separate case.

At least in JSC, we are normalizing type definitions that aren't recursive to be represented without a recursion group, which is an unnecessary step if the binary format separates them to begin with.

[tlively]

we are normalizing type definitions that aren't recursive to be represented without a recursion group

Can you elaborate on that? Nothing forces the types in a rec group to actually be recursive, but the shape of the full rec group still determines their type identity.

[titzer]

In Wizard, I initially tried to keep the logic for canonicalizing non-recursive singleton function types separate from canonicalizing recursion groups and found that the code duplication wasn't worth it. The additional "recursion group" object with a vector of a single type seemed like a reasonable tradeoff to have common logic for both.

[rossberg]

The only reason for making the distinction would be planning ahead for type parameters. In the presence of those, recursive and non-recursive types have quite a different semantics, but both are useful. For example, if you define

(type $a ...)
(type $s (struct (ref $a)))
(type $t (param $x) (struct (ref $x)))
(rec (type $u (struct (ref $a)))
(rec (type $v (param $y) (struct (ref $y))))

then (ref $t (arg $a)) would be equivalent to (ref $s), but (ref $v (arg $a)) wouldn't be equivalent to (ref $u). At least that would be the natural consequence of how higher-order iso-recursion usually work (and maintain decidability). In other words, non-recursive types behave like a parameterised aliases that reduce to their substituted definitions when applied, while recursive type applications never reduce and instead behave more like nominal types.

Both semantics are useful to have for different use cases, just like various languages provide type aliases besides nominal type definitions.

But of course, this distinction could also be introduced later and by other means.

[tlively]

Thanks @rossberg. I look forward to learning more about higher-order recursive types when we get there. In the meantime, I lean toward creating that distinction later and by other means to avoid depending on post-MVP extensions in our rationale for the MVP design.

[tlively]

We decided at the meeting today to keep the current semantics.