⊤ is the most general type of the Avail type lattice. It is pronounced "top" and written as the down tack
(U+22A4) character. In Avail, every value is an instance of
⊤, and every 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, that is, function whose return type is
nil is the value produced if and only if no exposed value is produced. The virtual machine uses
nil to simplify several core algorithms, but exposure of this special value to an Avail programmer would not yield a net good.
⊤ typically appears in Avail code in only a few select contexts:
As the return type of a function definition or function type. In this context, it signifies that the function does not produce a value when applied, i.e., it produces the unexposed value
- As the return type of a continuation type. In this context, it signifies that the continuation will not produce a value when exited, i.e., it produces the unexposed value
- As the read type of a variable type. In this context, it signifies that no value may be read from the variable; the variable is write-only.
As the idempotent initial value of an accumulator variable whose intermediate and final results represent a chain of type intersections. (Remember the identity law that states that the type intersection of
⊤with some type
- As the result of a semantic restriction that serves only to reject parses based on the types of the arguments (but does not strengthen the return type).
- As the result type of a phrase type. In this context, it signifies that the phrase serves as a statement, an expression that does not produce a value.
A function whose declared return type is
⊤ is still permitted to answer an exposed — non-
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
⊤. As an example,
"If|if_then_else_" may be used either as a statement or a value-producing expression:
⊤ is expressly forbidden from occurring in most contexts, including the following:
- As a parameter type of a function definition or function type.
- As a parameter type of a continuation type.
- As the write type of a variable type. This also correctly implies that it cannot be the type of an actual variable.
- As a leading type or the default type of a tuple type.
- As the element type of a set type.
- As the key type or value type of a map type.
- As the attribute value type of an object type.
- As the type parameter of a POJO type.
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, that is, 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 an uninitialized variable whose read type is
Please do not confuse
nil with the null reference present in other imperative programming languages.
|‹ Type Lattice|||||Return to Type System|||||