Most phrase kinds neither require nor permit type annotation. The compiler infers the types of such phrases by examining their composition. The exact process of type inference depends upon the phrase kind.
- The most basic type inference occurs for literal value phrases. A literal value is one primitively known to the compiler. Literal values are supported through special syntax. The compiler only understands three kinds of values primitively: integers, double-precision floating point numbers, and strings. The type of a literal value phrase is the instance type of the value itself.
A module constant definition phrase permanently binds a name to a value. The new constant has the type that is most specific to the bound value; that is, the type whose only instance is the value itself. The module constant definition itself is a statement, and therefore its inferred type is
A local constant definition phrase binds a name to a value within the remainder of the nearest enclosing scope. A local constant definition may be bound to any expression whatsoever, including one that refers to variables and arguments. Its type is the same as the inferred type of the expression. The local constant definition itself is a statement, and therefore its inferred type is
Whether or not its return type is annotated, some type inference is required for a label declaration. If the return type is specified, then it is used during type inference; otherwise, the compiler behaves as though there were an annotation of
⊥. The actual type inferred for a label is a continuation type whose parameter types match the enclosing function’s parameter types and whose return type is the one declared or determined. The label declaration is a statement, and therefore its inferred type is
- A variable use phrase indicates that the value of a variable, constant, or label should be read at execution time. The inferred type of such a phrase is obvious: it is the same as the type declared or inferred for the entity.
- A variable reference phrase denotes a usage of the variable itself, not the value that it stores. In Avail, a variable is a value, and thus an instance of some number of types. If the variable was declared in the module scope, then the type inferred for a variable reference phrase is the instance type of the variable itself; otherwise the variable is a local variable, and the type inferred is the type of variables able to yield and store values of the variable’s annotated type.
- A function definition must always explicitly type its parameters via parameter declarations. The return type annotation of an ordinary function definition is optional, however, so type inference may be necessary to ascertain it. If the return type annotation is present, then it is used to type the function. Otherwise, the return type of a function is inferred to match that of the last expression of the implementation. The type inferred for the function itself is a function type with appropriate parameter types and return type.
- Message sends constitute the bulk of an Avail program. The type inferred for a message send is the type intersection of the method's declared or inferred return type and all semantic restrictions applicable at the call site.
|‹ Type Annotations|||||Return to Type System|||||Semantic Restrictions ›|