Type Inference

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.
  /* These initializations are legal because the compiler infers the instance types * of literal values. */ i : 5’s type := 5; d : 10.1’s type := 10.1; s : "daffodil"’s type := "daffodil";
• 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 ⊤.
  /* This illustrates that the compiler can produce the precise double-precision * floating point approximation of "π". The assignment to "pi", a variable that * can only store the value 3.141592653589793, is legal only because "π" is known * to have a compatible type. */ π ::= 3.141592653589793; pi : 3.141592653589793’s type := π;
• 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 ⊤.
  aFunction ::= [ /* The compiler infers that "k" has type "integer", because this is * the static type inferred for this particular send of "_+_". */ x : integer := 5; k ::= x + 10; k ];
• 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 ⊤.
  /* This function converts a number into a numeral (in a silly way). */ stringifier ::= [ aNumber : number | /* This label is inappropriate, but together with the assertion * illustrates that the compiler infers that "body" is a continuation * accepting a number (when restarted) and yielding a string (when * exited). */ $body : string; Assert: body ∈ $[number]→string; Exit body with “aNumber” ] : string;
• 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.
  /* The initialization of "x" is permissible because "one" has a declared type of * "integer". */ one : integer := 1; x : integer := one;
• 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.
  /* Assuming that this is the module scope, then "referenceToX" is declared with * the instance type of the variable "x". */ x : integer := 20; referenceToX : (↑x)’s type := ↑x; Assert: ↓referenceToX = 20; aFunction ::= [ /* The instance type of "y" is not available to the compiler, because * a new variable is created each time this function is applied. */ y : integer := 50; referenceToIntegerVariable : ↑integer := ↑y; Assert: ↓referenceToIntegerVariable = 50; ];
• 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.
  multiplier : [integer, integer]→integer := [ /* These type annotations are mandatory. */ multiplicand : integer, multiplier : integer | /* The send of "_×_" is the last (and only) expression. Its type is * inferred to be "integer", thus the function's return type is also * inferred to be "integer". */ multiplicand × multiplier ];
• 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.
  /* Assume that "_+_" has a declared return type of "integer", and that there * exists a semantic restriction capable of producing an integral instance type * when presented with two instance types. Under these assumptions, the following * initializing declaration is legitimate. */ sum : 7's type := 5 + 2;