Bringing back `nullref`

[tlively]

I was talking with @kripken today about some Binaryen optimizations that would be much simpler if we had nullref rather than typed nulls. I seem to remember that we had discussed the possibility of bringing nullref back, so I wanted to make sure we captured that possibility in an issue.

[Horcrux7]

I think this is valid for every compiler.

[titzer]

I support nullref--it was a major issue for Jawa.

[tlively]

I added an agenda item for us to briefly discuss this at the next subgroup meeting: WebAssembly/meetings#1012.

[tlively]

If we do bring back nullref, should we also add a new version of ref.null that does not have the useless type parameter? If so, what should it be called? I haven't thought of anything better than ref.null2, which is pretty bad.

[Horcrux7]

What is the use of the two instructions? Why wouldn't a compiler always use the shorter instruction without type if there were two?

1. do not remove the type parameter. With ref.null nullref you can define a generic null value. This should be a similar size after compression.

2. you could call it ref.nil if you need two instructions.

[tlively]

A compiler would always use the shorter instruction and the current instruction would only be kept around for backward compatibility. Not adding a second instruction is also a reasonable option, as you say.

[rossberg]

I wouldn't add a redundant instruction. Using ref.null with the bottom heap type seems fine to me.

[titzer]

If we plan to have other places in the encoding where the heap bottom type might be used, then I think it makes sense to not have a separate instruction. Otherwise, I think we shouldn't introduce a new type just for this purpose, especially if we need to add restrictions on where/how you could use it. For example, I assume it would be an error to encode (ref bottom) as a value type (i.e. a non-null reference to the bottom type--a contradiction). Holes in the encoding space like that are just warts.

[rossberg]

Well, we already can produce the bottom heap type during validation, you merely can't write it down in a program right now. Given (ref null bot), you can't disallow (ref bot) at least internally without breaking subtype substitutability, weakening, and principal types.

And of course, there are various other ways to create uninhabited types, e.g., (type $t (struct (ref $t))) has no values either. Such types are simply useless. Introducing special rules or restrictions typically creates much bigger warts than allowing useless types/expressions/programs, especially when those would introduce discontinuities.

(Uninhabited bottom types aren't even entirely useless, e.g., they can be convenient to type functions that never return regularly.)

[titzer]

There is a bottom value type in validation, but not a bottom heap type, AFAICT.

The example of the non-null circular struct is only uninhabited because there isn't a fixpoint value-construction operator. If there was, you could construct it. Or, if we had more loose initialization rules. Or, the host environment could also construct one. The type itself isn't nonsensical.

The more I think about it, the more nonsensical it seems to me.

I don't think the type of the bottom null value should be a heaptype at all, but should be its own type. It's kind of strange to me to think of (ref heapnull) (i.e. a non-null reference to the null heap type?) being a subtype of (ref $T), (i.e. a non-null reference to $T)--that only works because the type is uninhabited. And then there would also be (ref null heapnull)--which would be inhabited. And you could do (ref.as_non_null (ref.null heapnull)) which would throw, but would give you a non-null type.

Given (ref null bot), you can't disallow (ref bot) at least internally without breaking subtype substitutability, weakening, and principal types.

I am not suggesting that, but suggesting just a type nullref. Then nothing breaks.

[titzer]

Also, I think adding a null or bottom heap type complicates adding nested aggregates in the future, since one way to specify a nested aggregate would be declaring a field of with value type (inline $heaptype), which would make no sense with (inline bottom)--both on its own and in terms of subtyping.

[rossberg]

Like all similar type names, nullref would just be a shorthand, namely for (ref null bot). It is central to the type system that all reference types have the shape (ref null? heaptype), because a type algebra needs to be compositional in the right way. If nullref was different, you'd need an extra special case typing rule for every single construct involving a reference input type! (Combinatorially many for those that have more than one.)

(And some of those new rules you couldn't formulate without also introducing the equivalent of (ref bot). As a simple example, the type of ref.as_non_null is (ref null ht) -> (ref ht), for any ht. Remember that this instruction has to type-check uniformly for nullref as well, by its nature of being a subtype of every (ref null ht). Otherwise, you'd break the most basic subtyping properties! In this case, you could get around it by introducing even more mandatory type annotations, but that seems counter-productive, given that the instruction shouldn't have to care at all about what ht is.)

During validation, the bottom heap type (and in fact, (ref bot)) comes up when you pop a bottom type from the stack but expect a reference type. For example, br_on_data will then have to return (ref bot) as its principal type. See the pop_ref function in the draft algorithm sketch.

Think of the bottom heap type as the empty union. If we already had general unions, like discussed elsewhere, it would arise naturally as well.

[rossberg]

To concretise the discussion, I implemented the suggestion in terms of the bottom heap type in #295. As can be seen from the PR, it requires no functional changes to the interpreter other than recognising the new type name in de/encoder, parser, and validator.

[tlively]

Closing this in favor of continued discussion on #310