A simple function

We’re going to walk through how the type checker handles a very simple program, step by step. Here is the complete program:

crate::assert_ok!(
    {
        class Point {
            x: Int;
            y: Int;
        }

        class Main {
            fn test(given self) -> Int {
                let p = new Point(22, 44);
                0;
            }
        }
    }
);

Nothing very exciting happens here – we create a Point and then return 0. But working through this example introduces the basic machinery that everything else builds on: the environment, places, types, and – most importantly – how the type checker is structured as a set of judgment functions with inference rules.

Grammar declarations

The formal model represents programs using Rust structs annotated with #[term], a macro from formality-core. Each #[term] struct defines both the abstract syntax and a textual grammar (the $-prefixed patterns).

A class declaration contains a name, an optional class predicate, and a binder wrapping the fields and methods:

#[term($?class_predicate class $name $binder)]
pub struct ClassDecl {
    pub name: ValueId,
    pub class_predicate: ClassPredicate,
    pub binder: Binder<ClassDeclBoundData>,
}

#[term($:where $,predicates { $*fields $*methods })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
}

A field declaration is a name and a type:

#[term($?atomic $name : $ty ;)]
pub struct FieldDecl {
    pub atomic: Atomic,
    pub name: FieldId,
    pub ty: Ty,
}

A method declaration contains a name and a binder wrapping the receiver (this), parameters, return type, predicates, and body:

#[term(fn $name $binder)]
pub struct MethodDecl {
    pub name: MethodId,
    pub binder: Binder<MethodDeclBoundData>,
}

// FIXME: need to guard `$inputs` by a comma and output by `->`, using customized parse
#[term(($this $,inputs) -> $output $:where $,predicates $body)]
#[customize(parse)]
pub struct MethodDeclBoundData {
    pub this: ThisDecl,
    pub inputs: Vec<LocalVariableDecl>,
    pub output: Ty,
    pub predicates: Vec<Predicate>,
    pub body: MethodBody,
}

The environment

The type checker’s job is to walk through each statement in a method body and track what it knows about each variable. This information is stored in the environment (Env), which maps variables to their types:

#[derive(Clone, Ord, Eq, PartialEq, PartialOrd, Hash)]
pub struct Env {
    program: Arc<Program>,
    universe: Universe,
    in_scope_vars: Vec<Variable>,
    local_variables: Map<Var, Ty>,
    assumptions: Set<Predicate>,
    fresh: usize,
}

The key field for now is local_variables, which maps each variable to its type. (We’ll explain the other fields as they become relevant.)

Judgments and inference rules

The type system is defined as a collection of judgment functions. Each judgment function is defined with the judgment_fn! macro and contains one or more inference rules. An inference rule has premises above a horizontal line and a conclusion below it. The conclusion holds when all the premises are satisfied.

For example, an inference rule with the conclusion check_program(program) => () means “the program type-checks successfully.” The premises above the line specify what must be true for that conclusion to hold.

How type checking begins

Type checking begins with the check_program judgment, which checks that every declaration in the program is well-formed:

(for_all(decl in program.decls.clone())
    (check_decl(program, decl) => ()))
----------------------- ("check_program")
(check_program(program) => ())

The sole premise uses for_all to require that check_decl succeeds for each declaration. In our example, the program has two declarations (Point and Main), so the premise is satisfied when both classes check successfully.

For each class, check_class checks the fields and then each method. Let’s look at the rule for check_method:

(let MethodDecl { name: _, binder } = decl)
(let (env, vars, MethodDeclBoundData { this, inputs, output, predicates, body }) =
    env.open_universally(binder))

(let env = env.add_assumptions(
    vars.iter()
        .flat_map(|v| vec![VarianceKind::Relative.apply(v), VarianceKind::Atomic.apply(v)])
        .collect::<Vec<_>>(),
))

(check_predicates(env, predicates) => ())
(let env = env.add_assumptions(predicates))

(let ThisDecl { perm: this_perm } = &this)
(let this_ty = Ty::apply_perm(this_perm, class_ty))
(let env = env.push_local_variable(This, this_ty)?)

(let env = env.push_local_variable_decls(inputs)?)

(for_all(input in inputs)
    (let LocalVariableDecl { name: _, ty } = input)
    (check_type(env, ty) => ()))

(check_type(env, output) => ())

(check_body(env, output, body) => ())
----------------------------------- ("check_method")
(check_method(class_ty, env, decl) => ())

For our example, the method declaration for test specifies given self, so the premises compute the type given Main and push it into the environment as self. If there were other parameters, they’d be pushed too. Once the environment is ready, the final premise invokes the check_body judgment:

(let live_after = LivePlaces::default())
(can_type_expr_as(env, live_after, block, output) => ())
----------------------------------- ("block")
(check_body(env, output, MethodBody::Block(block)) => ())

The “block” rule applies to our example (the “trusted” rule handles built-in methods with no body). Its premises initialize live_after to the empty set – nothing is live after the method body returns – and then require that can_type_expr_as succeeds, checking that the body can be typed as the declared return type (Int).

Typing a block

The body of a method is a block expression, so type_expr dispatches to type_block:

(type_statements(env, live_after, statements) => (env, ty))
----------------------------------- ("place")
(type_block(env, live_after, Block { statements }) => (env, ty))

A block is a sequence of statements, so this delegates to type_statements, which walks through statements one at a time:

(let live = live_after.before(statements))
(type_statement(env, live, statement) => (env, ty))
(type_statements_with_final_ty(env, live_after, statements, ty) => (env, ty))
----------------------------------- ("cons")
(type_statements_with_final_ty(env, live_after, Cons(statement, statements), _ty) => (env, ty))

The type of the last statement becomes the type of the block.

Notice the first premise: live_after.before(&statements). Every judgment in the type system carries a live_after parameter – the set of variables that are live (i.e., used later in the program). In this chapter, nothing interesting happens with liveness because we never use our variables again. We’ll explain liveness in detail in the Giving chapter, where it determines whether a value is moved or copied.

Typing let p = new Point(22, 44)

The let statement is handled by this rule:

(type_expr(env, live_after.clone().overwritten(id), &**expr) => (env, ty)) // [1]
(let env = env.push_local_variable(id, ty)?)
(let env = env.with_in_flight_stored_to(id))
----------------------------------- ("let")
(type_statement(env, live_after, Statement::Let(id, Ascription::NoTy, expr)) => (env, Ty::unit()))

The rule has three premises:

• type_expr(env, live_after.overwritten(&id), ...) => (env, ty) – Type the right-hand side expression (new Point(22, 44)) and produce its type ty. The live_after.overwritten(&id) removes p from the live set, since p doesn’t exist yet while the RHS is being evaluated.

• env.push_local_variable(&id, ty) – Add p to the environment with the type produced by the first premise.

• env.with_in_flight_stored_to(&id) – Record that the result of the expression is now stored in p. (We’ll explain “in-flight” values in a later chapter – for now, just think of it as “the result of the expression flows into the variable”.)

Typing new Point(22, 44)

The new expression is typed by the following rule:

(let class_decl = env.program().class_named(class_name)?)

(let ClassDeclBoundData { predicates, fields, methods: _ } = class_decl.binder.instantiate_with(parameters)?)

(if fields.len() == exprs.len())

(let this_ty = NamedTy::new(class_name, parameters))
(prove_predicates(env, predicates) => ())

(let (env, temp_var) = env.push_fresh_variable(this_ty))

(type_field_exprs_as(env, live_after, temp_var, exprs, fields) => env)

(let env = env.with_place_in_flight(temp_var))
(let env = env.pop_fresh_variable(temp_var))
----------------------------------- ("new")
(type_expr(env, live_after, Expr::New(class_name, parameters, exprs)) => (env, this_ty))

The premises require:

1. Looking up the class Point to find its fields: x: Int, y: Int.
2. Checking that the argument count matches the field count (2 = 2).
3. Creating a temporary variable to represent the object under construction.
4. Invoking type_field_exprs_as to type each argument against the corresponding field type – 22 against Int, 44 against Int. Both succeed via the integer typing rule:

----------------------------------- ("constant")
(type_expr(env, _live_after, Expr::Integer(_)) => (env, Ty::int()))

The “constant” rule has no premises – the conclusion type_expr(env, _, Expr::Integer(_)) => (env, Ty::int()) holds unconditionally. Any integer literal has type Int.

The conclusion of the “new” rule gives us the type Point.

After the let

After typing let p = new Point(22, 44), the environment becomes:

Typing the return expression 0

The final statement in the block is 0 – an expression statement. It is typed by this rule:

(type_expr(env, live_after, expr) => (env, ty))
(let (env, temp) = env.push_fresh_variable_with_in_flight(ty))
(env_permits_access(env, live_after, Access::Drop, temp) => env)
(parameter_permits_access(env, ty, Access::Drop, temp) => env)
(let env = env.pop_fresh_variable(temp))
----------------------------------- ("expr")
(type_statement(env, live_after, Statement::Expr(expr)) => (env, ty))

The first premise types the expression 0, yielding type Int (by the “constant” rule shown above). The remaining premises check that both the environment and the type permit dropping the temporary value. For Int, dropping is trivially permitted.

The type of the last statement (Int) becomes the type of the block. Back in check_body, the can_type_expr_as premise checks this against the declared return type Int – subtyping succeeds, and the method type-checks successfully.

What about p?

You may have noticed that we never use p. We create a Point, bind it to p, and then ignore it. The type checker is fine with this – p is never referenced after the let, so it’s not in the live set and the type checker simply ignores it.

In the next chapter, we’ll see what happens when variables are live – and how liveness determines whether a value is moved or copied.