Type Annotations

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.
  /* After this declaration and until the end of the enclosing scope, code may refer * to "n". The variable begins life unassigned; an attempt to read from it will * raise an exception. */ n : integer; /* This next declaration introduces "greeting", a variable initialized with a * famous string and capable of storing any other string (irrespective of its * fame). */ greeting : string := "Hello, world!\n";
• A function parameter declaration phrase introduces a named function parameter and specifies a type to which its values must conform during function application.
  /* "plusOne" is a function applicable to a single argument, an integer, that * produces a value exactly one greater than this argument. */ plusOne ::= [x : integer | x + 1]; Assert: plusOne(20) = 21;
• 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.
  /* This primitive function accepts two numeric arguments and answers their sum. */ adder ::= [ augend : number, addend : number | /* Addition fails when the arguments are unlike infinities, so the * primitive failure variable type annotation is mandatory. * "failureCode" will contain a specific numeric error code if the * primitive fails. The method "cannot-add-unlike-infinities code" * answers this particular error code. */ Primitive 1 (failureCode : natural number); Assert: failureCode = cannot-add-unlike-infinities code; Raise a cannot-add-unlike-infinities exception ] : number; Assert: adder(10, 25) = 35;

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.
  /* "explicitPlusOne" is the same function as "plusOne" above, but annotated with * an explicit return type. */ explicitPlusOne ::= [x : integer | x + 1] : integer; Assert: explicitPlusOne(20) = 21;
• 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 ⊥.
  /* This is an implementation of the classical while loop. */ Method "While_do_" is [ predicate : []→boolean, body : [⊥]→⊤ | /* "loop" is a label. Whenever "predicate" yields true, then "body" is * applied and the continuation bound to "loop" is restarted, i.e., control * suddenly resumes at the the beginning of the function. */ $loop; If predicate() then [ body(); Restart loop ]; ] : ⊤; /* This answers the first element of a tuple that satisfies the given predicate, * or 0 if no such element exists. */ Method "first index of_where_" is [ elements : tuple, predicate : [any]→boolean | /* If "elements" contains an element that satisfies "predicate", then we * want to exit the implementation early; there’s no point in testing the * remaining elements. So we need to annotate "foundIt" with the return type * "natural number" (a subtype of "whole number") so that we can safely exit * the continuation. */ $foundIt : natural number; For each of elements do [ element : any, index : natural number | If predicate(element) then [ Exit foundIt with index ]; ]; 0 ] : whole number;

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.