⊥ (bottom) ≝ ∅ᵀ

⊥ is the most specific type of the Avail type lattice. It is pronounced "bottom" and written as the up tack (U+22A5) character. In Avail, no value is an instance of ⊥, and every type is a supertype of ⊥.

Consider why there are no instances of ⊥. Given that values are instances of a type because of similarity, and ⊥ is a subtype of every type, the hypothetical and counterfactual instances of ⊥ would have to be compatible with every type. So an instance of ⊥ would be eligible for arithmetic, because numbers are; subscripting, because tuples are; application, because functions are; resumption, because continuations are; and so forth. Moreover, an instance of ⊥ would be valid at every argument position of every message send. This is clearly absurd. Ergo, the most specific type then is the one that cannot, for coherency, have any instances.

As a brief aside, most imperative programming languages do implicitly have an instance of a type equivalent to ⊥ in their own type systems, even though this type itself is usually not expressible. This pseudo-value is hardwired into the syntax with a name like null, nil, none, undef, or the like, and represents the absence of a value. But the mere existence of such a value is inconsistent with any coherent type theory. Though usage of such a value is often convenient in the short-term, its long-term consequences are devastating:

I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language (ALGOL W). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years.

Hoare, Tony. "Null References: The Billion Dollar Mistake." QCon. The Queen Elizabeth II Conference Centre, London, UK. 13 March 2009. Conference Presentation.

To be explicit, Avail does not have such a value. The type ⊥ truly does not have any instances. The type itself does have many other uses, however, as in the following contexts:

• As the return type of a function definition or function type. In this context, it signifies that the function does not return. Instead, it must apply another function or call a method whose return type is also ⊥. Primitive methods with a return type of ⊥ either raise an exception, switch to another continuation, terminate the current fiber, or exit the entire program. Ordinary methods combine these primitives in creative ways to cause the current fiber to loop forever, wait permanently for a synchronization event, and so on.
• As the type annotation of a label declaration.
• As the canonical default type of a tuple type whose cardinality restriction is a subtype of [0..0]. The only instance of such a type is the empty tuple (<>).
• As the canonical element type of a set type whose cardinality restriction is a subtype of [0..0]. The only instance of such a type is the empty set (∅).
• As the canonical key type and value type of a map type whose cardinality restriction is a subtype of [0..0]. The only instance of such a type is the empty map ({}).
• As the attribute value type of an uninstantiable object type.
• As a contravariant type parameter: the write type of a variable type, a parameter type of a function type or continuation type, or the return type of a continuation type. As the write type of a variable type, it signifies that no value may be written to the variable; the variable is read-only.
• As the idempotent initial value of an accumulator variable whose intermediate and final results represent a chain of type unions. (Remember the identity law that states that the type union of ⊥ with some type A is always A).
• As the type intersection of disjoint types.
• As the result of a semantic restriction. In this context, it indicates that a particular invocation of the restricted method does not return.
• As the result type of a send phrase type, to indicate that the represented message send does not return.

⊥ is expressly forbidden from occurring in the following contexts:

• As a type annotation in a variable declaration, function parameter declaration, or primitive failure variable declaration.
• As the inferred type of a constant definition, initialization expression, assignment expression, or message argument expression.
• As the inferred type of a module-level statement or a non-last statement of a function definition.

To illustrate a practical, concrete use of ⊥, here is a plausible implementation of "Repeat_", a control structure that continually repeats application of its argument, a ⊤-valued function. Following is another example of a ⊥-valued method that is slightly absurd, but demonstrative nonetheless.