Avail is a statically typed language. As such, every phrase comprising a source program is either 1) annotated with a particular type by the programmer or 2) inferred to yield a particular type by the compiler. Which of these mechanisms is employed depends only upon the kind of the phrase in question. Most phrase kinds acquire their types through compiler inference. Only a few phrase kinds mandate type annotation by the programmer:
- A variable declaration phrase introduces a named mutable storage location into the current scope and specifies a type to which stored values must conform. A variable declaration that also stores an initial value is an initializing variable declaration.
- A function parameter declaration phrase introduces a named function parameter and specifies a type to which its values must conform during function application.
- Some functions rely on virtual machine primitives for their implementations. For example, adding two numbers together is so basic that it would be inappropriate, if not impossible, to provide an implementation in Avail source code; therefore the virtual machine must implement this capability directly and expose it for use in Avail source code. Such a function is a primitive function. A primitive function begins its body with a primitive linkage statement that specifies, by ordinal, which virtual machine primitive should be invoked when the function is applied. A primitive linkage statement includes a primitive failure variable declaration that is mandatory whenever the target primitive is permitted to fail in some circumstance and forbidden otherwise. When a fallible primitive actually fails, a value is stored into the primitive failure variable; this value indicates what went wrong, and is usually a numeric error code. Only in the event of failure is the sequence of statements following the primitive linkage statement actually executed. It has the responsibility of handling the failure somehow, and the failure variable should help it fulfill this role. The return type declaration specifies the type of values producible by the function. This declaration is optional for ordinary Avail functions, but mandatory for primitive functions.
Only two phrase kinds permit type annotation but do not necessarily require it:
- Any function definition may include a trailing return type declaration. As mentioned above, this declaration is optional for ordinary Avail functions. Though the return type of any non-primitive function can be inferred directly from its implementation, the programmer may explicitly annotate a function with its return type in order to 1) sincerely document, as a courtesy to humans, the type of values producible or 2) weaken the type beyond what would be inferred by the compiler.
Any non-primitive function definition may begin with a label declaration. A label is a special constant that is bound to a continuation when the enclosing function is applied. This continuation, when restarted, causes the body of the function to execute. The same continuation, when exited, causes control to return to the function’s caller. A label declaration permits an optional return type declaration. If specified, then this declaration must be compatible with the return type declaration, annotated or inferred, of the enclosing function. If not specified, then this declaration is inferred to be
A type annotation may be any expression that yields a type when evaluated, so long as that expression does not incorporate variables and constants introduced in intermediate scopes. The compiler always evaluates type annotations in the module scope rather than the nearest enclosing scope. This is essential for a statically typed language. It guarantees that the type represented by an annotation cannot depend upon values not known until execution time.
All of this also implies, correctly, that the compiler must run user code in order to ascertain the type intended by an annotation. Avail differs from other programming languages in that the compiler itself can and does invoke user code, yet a firm distinction is maintained between the compilation time and execution time of a program. In order to build a program, the compiler must execute all module-level statements. Type annotations may always rely on the side-effects of previously executed module-level statements.
|‹ Type Names|||||Return to Type System|||||Type Inference ›|