Avail - Type System

`⊤ (top)`

⊤ 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 ⊤. Thus 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 nil.
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 nil.
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 A is always A.)
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:

/* Allow "If|if_then_else_" to be used either as a statement or as an expression.
 * It is ⊤-valued, so before this semantic restriction can be enforced, it can
 * only be used as a statement.
 */
Semantic restriction "If|if_then_else_" is
[
	predicate : boolean's type,
	then : []→⊤'s type,
	else : []→⊤'s type
|
	/* Capture the return types of "then" and "else". We will need them. */
	thenReturnType ::= then's return type;
	elseReturnType ::= else's return type;
	/* The return type of one (or both) of the functions will be used to
	 * determine the return type of an "If|if_then_else_" expression.
	 *
	 * If the exact type of the precidate is not known, i.e., if the type
	 * does not indicate that the predicate is necessarily true or
	 * necessarily false, then answer the type union of the return types of
	 * the two functions.
	 *
	 * If the predicate is necessarily true, then answer the first function's
	 * return type; otherwise, answer the second function's return type.
	 *
	 * Wait, this is weird, isn't it? The semantic restriction uses the very
	 * method that it's trying to restrict! This is okay, it just means that
	 * only the semantic restrictions previously defined will be applied by
	 * the compiler here. Since we are trying to define the very capability
	 * of using "If|if_then_else_" as an expression, we can't use that trick
	 * here. Instead we have to treat it as a statement.
	 */
	returnType : type;
	If predicate = boolean
	then
	[
		returnType := thenReturnType ∪ elseReturnType;
	]
	else
	[
		If predicate = true's type
		then [returnType := thenReturnType;]
		else
		[
			Assert: predicate = false's type;
			returnType := elseReturnType;
		];
	];
	returnType
];

/* Read a natural number from the console. Store the smaller of "x" and 100
 * into "maxOf100". Use "If|if_then_else" as an expression.
 */
x : natural number := next natural number from console;
maxOf100 : natural number := if x > 100 then [100] else [x];

/* Read a natural number from the console. Store the larger of "y" and 100 into
 * "minOf100". Use "If|if_then_else" as a statement.
 */
y : natural number := next natural number from console;
minOf100 : natural number;
If y > 100 then
[
	minOf100 := y;
]
else
[
	minOf100 := 100;
];

⊤ 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 | any ›