10.2. Type inference🔗

We will allow inferring types for local variables, but possibly also procedure signatures. Possibly based on configuration, we will enable inferring the dynamic type for variables, which may cause fewer type errors to be emitted. We might also infer composite type definitions based on usage.

Laurel can statically infer the types of variables, which, when the inferred types were otherwise not available in the source program, can enable emitting code that can be verified more efficiently.

Here's an example related to nullable reference types:

Input program:

var foo := new Foo;
foo#x := 1;

var bar := foo;
bar := null;
bar#x := 2

Without type inference, we cannot judge whether the variable foo should have type Foo or Nullable<Foo>, so we have to pick defensively:

datatype Nullable<T> = from_NotNull(as_notNull: T) | from_Null

var foo: Nullable<Foo> := from_NotNull(new Foo);
as_notNull(foo)#x := 1;

var bar: Nullable<Foo> := foo;
bar := null;
as_notNull(bar)#x := 2

With type inference, we can infer that foo is never nullable:

var foo: Foo := new Foo;
foo#x := 1;

var bar: Nullable<Foo> := from_NotNull(foo);
bar := null;
as_notNull(bar)#x := 2

Note the coercion from_NotNull that was inserted in the assignment to bar. Laurel can be given a list of coercions that can be inserted automatically. Laurel can also be given a list of type coercions, which it can use to change the type annotations of variables, from for example T to Nullable<T>.