/avail/Avail/Foundation/Bootstrap/Special Objects:
Source: /avail/Avail/Foundation/Bootstrap/Special Objects
Categories: Primitives, Types
See: /about-avail/documentation/type-system/types-top.html
The true abstract root of the Avail type lattice. It is pronounced top and written as the down tack (⊤) character. Every Avail value is an instance of , and every Avail type is a subtype of .

is distinct from any in that it includes exactly one additional value: the special value nil. This value does not satisfy any public protocol and is not available to an Avail programmer. It is, however, implicitly returned from every procedure, i.e., function whose return type is . Thus nil is the value produced iff no value is produced. The virtual machine uses nil to simplify several core algorithms, but exposure of nil to an Avail programmer would not yield a net good.

typically appears in Avail code in only a few select contexts:

A function whose declared return type is is still permitted to answer an actual (non-{@code nil }) value. This is consistent with the type lattice, since every value is an instance of . It is useful, moreover, because a semantic restriction may strengthen the return type of a -valued function at a particular call site to a subtype of .

is expressly forbidden from occurring in most contexts, including the following:

Note that these prohibitions, when considered in aggregate, negate any possible value that could be gleaned from exposing the special value nil to an Avail program. They conspire together to ensure that nil could never be retained by an Avail value. It may therefore only exist as a temporary within a continuation, i.e., an item on the local stack of a function call. A reflective query of a continuation's temporaries that would answer nil will instead produce a variable whose read type is .