Type Inference

6 Type Inference

Cyclone allows many explicit types to be elided. In short, you write _ (underscore) where a type should be and the compiler tries to figure out the type for you. Type inference can make C-like Cyclone code easier to write and more readable. For example,

  _ x = malloc(sizeof(sometype_t));

is a fine substitute for

  sometype_t * x = malloc(sizeof(sometype_t));

Of course, explicit types can make code more readable, so it is often better style not to use inference.

Inference is even more useful because of Cyclone's advanced typing constructs. For example, it is much easier to write down _ than a type for a function pointer.

We now give a rough idea of when you can elide types and how types get inferred. In practice, you tend to develop a sense of which idioms succeed, and, if there's a strange compiler-error message about a variable's type, you give more explicit information about the variable's type.

Syntax

As far as the parser is concerned, _ is a legal type specifier. However, the type-checker will immediately reject _ in these places (or at least it should):

As part of a top-level variable or function's type.
As part of a struct, union, datatype, or typedef declaration.

Note that _ can be used for part of a type. A silly example is $(_,int) = $(3,4); a more useful example is an explicit cast to a non-nullable pointer (to avoid a compiler warning). For example:

  void f(some_big_type * x, some_big_type @ y) {
  if(x != NULL) {
    y = (_ *@notnull) x;
  }

Semantics

Except for the subtleties discussed below, using _ should not change the meaning of programs. However, it may cause a program not to type-check because the compiler no longer has the type information it needs at some point in the program. For example, the compiler rejects x->f if it does not know the type of x because the different struct types can have members named f.

The compiler infers the types of expressions based on uses. For example, consider:

  _ x = NULL;
  x = g();
  x->f;

This code will type-check provided the return type of g is a pointer to a struct with a field named f. If the two statements were in the other order, the code would not type-check. Also, if g returned an int, the code would not type-check, even without the x->f expression, because the _ x = NULL constrains x to have a pointer type.

However, the above discussion assumes that sequences of statements are type-checked in order. This is true, but in general the type-checker's order is unspecified.

Subtleties

In general, inference has subtle interactions with implicit coercions (such as from t*@notnull to t*@nullable) and constants that have multiple types (such as numeric constants).

The following is a desirable property: If a program is modified by replacing some explicit types with _ and the program still type-checks, then its meaning is the same. This property does not hold! Here are two examples:

Numeric Types

This program prints -24 1000:

  int f() {
  char c = 1000;
  return c;
  }
  int g() {
  _ c = 1000; // compiler infers int
  return c;
  }
  int main() {
  printf("%d %d", f(), g());
  return 0;
  }

Order Matters

Here is an example where the function's meaning depends on the order the type-checker examines the function:

  void h1(int *@notnull c, int maybe) {
    _ a;
    if(maybe)
      a = c;
    else
      a = NULL;
  }

At first, the type of a is completely unconstrained. If we next consider a = c, we will give a the type of c, namely int *@notnull, an int pointer that cannot be NULL. Clearly that makes the assignment a = NULL problematic, but Cyclone allows assignment from nullable pointers to non-nullable pointers; it gives a compile-time warning and inserts a run-time check that the value is not NULL. Here the check will fail and an exception will be raised. That is, h1(p,0) is guaranteed to raise an exception.

But what if the type-checker examines a = NULL first? Then the type-checker will constrain a's type to be a nullable pointer to an unconstrained type. Then the assignment a = c will constrain that type to be int, so the type of a is int *. An assignment from int *@notnull to int * is safe, so there is no warning. Moreover, the assignment a = NULL is not a run-time error.

The order of type-checking is left unspecified. In the future, we intend to move to a system that is order-independent.