Inference

Lexica is a staticly typed language and relies on type inference to determine the types of unannotated expressions. Type inference is performed using unification constraint solving and immediately solved at the site of the constraint.

Structures

Structure	Description
Inference Type	Represents a type variable or solved type
Engine	Stores and unifies type variables based on constraints
Environment	Maps expressions and variables to type variables and inference types
Type Resolution	Represents a resolved type
Type Context	Maps expressions and variables to resolved types

Queries

Function

Return

A type context for the function that was requested. May raise inference errors.

Dependencies

Requires the function node of the requested function.

Templates

Templates in a function are represented with a template inference type.

fn identity(value: $Value) -> $Value: value

Templates cannot unify with an instance. Templates can only be unified with themselves or inference variables. This prevents erroneous unification of templates with other templates.

// This should NOT type check.
fn identity(value: $Other) -> $Value: value

When a template function is used, templates are replaced with fresh inference variables and are unified as normal.

fn double(value: i64) -> i64:
    identity(value) * 2

Projections

The type of a field or method call cannot be determined until the expression type itself is known.

expression.field = other

Hence, unification of fields and method calls are deferred until all other expressions have been unified. If the type of the expression is still not resolved an inference error is raised.