"Bottom type" in spec?

[kripken]

The term came up in the CG meeting today. Searching the spec for it, it appears in the index, but refers to page 9 where there is no appearance of that term.

From the CG discussion, I understand it is related to the polymorphic stack concept and unreachability. Unreachability doesn't show up on page 9.

A text search for the word "bottom" turns up only the index.

[conrad-watt]

There are two places that are relevant for the current approach.

The Unknown type described here (https://webassembly.github.io/spec/core/appendix/algorithm.html) corresponds to the bottom value type. In the MVP, it's purely a detail of the (implementations') validation algorithm and doesn't appear in the formalism.

With the advent of reference types, the bottom value type needs to be added to the formalism in order to bless current implementations (as described above, these already utilized a bottom/Unknown value type). This is described here (WebAssembly/reference-types#116).

[kripken]

I see, thanks @conrad-watt !

I think I understand this now. I'm unsure if this is worth fixing in the spec text or not - maybe to most people it's just obvious what a "bottom type" is. Like in the PR you linked, it appears in the discussion, but not in the committed text. At least for me - a person without a type theory background - using a term not defined was confusing, and the spec's index just added to that confusion.

[rossberg]

Ah, thanks, another leftover of WebAssembly/reference-types#87 -- it used to be defined as part of value types. I fixed the index, once CI is done it should point to Section 3.3 (Instruction Validation).

[kripken]

Thanks @rossberg !

Sounds like this can be closed.