This is just a brief little walkthrough of how to interpret the simplest typing rules, by presenting them as Rust types to appeal to what you already know. There's plenty uncovered, but this should get you off to a great start!
(I originally wrote this in response to a particular question, so it's a little targeted. Anyone is very welcome to suggest edits, I might come by and fix it up later)
We want typing contexts because some expressions have free variables. To know the type of (x, y), we need to know the types of the x and y variables, so we need a way to store them.
Let's do that in the bluntest way possible:
type Context = HashMap<Identifier, Type>;now with that context type, we can describe the typing judgement we're looking for:
fn type_of(expression: Expr, in_context: Context) -> Type;This shouldn't seem too surprising! We want to define a function that finds the type of any particular expression by some sensible collection of rules. however, functions are a bit too restrictive, part of our job here it proving this is a function (has 1 output for any given input), so we use a looser definition of "relations" in general:
pub struct TypeOf {
expression: Expr,
in_context: Context,
ty: Type,
}and we say that whenever you have a value of TypeOf, you know that that typing relation is true.
so, the simplest axiom we could possibly add from the variables in context would be:
note that "axioms" here are basically just the public functions, which define all the ways we can make new
TypeOfobjects once we leave this module since we can't just write to the fields anymore
pub fn loading_a_variable_uses_its_type(variable: Identifier, ty: Type) -> TypeOf {
TypeOf {
expression: Expr::Var(variable),
in_context: HashMap::from([(variable, ty)]),
ty,
}
}so lets reiterate what this means:
when we're in a context where context[variable] = ty,
a variable load expresssion of variable
has the type ty
this is the core purpose of the typing context, we want to define the relationship between identifiers and "scopes" of let bindings.
Next up, we'll move onto our challenge of typing (x, y), we have
fn type_of_x_y_tuple(xt: Type, yt: Type) -> TypeOf {
let x_typeof = loading_a_variable_uses_its_type("x", xt);
let y_typeof = loading_a_variable_uses_its_type("y", yt);
// so we know that TypeOf(["x", xt], Var("x"), xt) and vice versa,
// but we need a new axiom to tell us about the type of pairs.
tuple_constructor_is_pair(x_typeof, y_typeof)
}When making a pair, we want to take information about the fst and snd member
and merge it together to find out (x : A, y : B) : Pair A B
pub fn tuple_constructor_is_pair(a: TypeOf, b: TypeOf) -> TypeOf {
TypeOf {
// once we've written the expression that this axiom is for,
expression: Expr::tuple([a.expression, b.expression]),
// the type we want becomes pretty clear:
ty: Type::Pair(a.ty, b.ty),
// and lastly, what context is this true in?
// we can't just pick anything here. as an example,
// the empty context would mean that `(x, y) : Pair A B`
// even when there're no variables in scope.
//
// instead, we need all the variables from a *and* b's judgements:
// a pair is only valid when we can build both elements.
in_context: {
let mut all_variables = a.in_context.clone();
for (name, t) in &b.in_context {
let Some(existing_type) = all_variables.get(name) else {
// we can just add variables that are missing
all_variables.insert(name.clone(), t.clone());
continue;
};
// but if both contexts have a name, then
// there's a small snag, we can't put (x : a.cx[x], x : b.cx[x])
// into the same context.
// So instead, we *require* that they agree.
// if both contexts have the same type then it's fine to use the original from a's context.
assert_eq!(existing_type, t);
}
all_variables
}
}
}here's an executable version of the rules so far
While this really is faithful to the semantics of inference rules, there is 1 major difference in normal type systems: we generally dont have all this context "merging" logic inside every rule, and instead separate it out into another rule that can be composed with the normal axioms. That way, tuple_constructor_is_pair can simply assert that the two contexts are equal:
pub fn tuple_constructor_is_pair(a: TypeOf, b: TypeOf) -> TypeOf {
assert_eq!(a.in_context, b.in_context);
TypeOf {
expression: Expr::tuple([a.expression, b.expression]),
ty: Type::Pair(a.ty, b.ty),
in_context: a.in_context,
}
}and this is instead handled by a rule that says that
whenever TypeOf(expr: E, ty: T, in_cx: Vars),
it's also true that TypeOf(expr: E, ty: T, in_cx: Vars | {other_variable : AnyType})
that is, adding more variables to the scope doesnt change the type
of an expression.
pub fn with_bigger_scope(mut a: TypeOf, v: Identifier, t: Type) -> TypeOf {
assert_eq!(a.in_context.insert(v, t), None);
TypeOf {
expression: a.expression,
ty: a.ty,
in_context: a.in_context,
}
}and you can play with that working altogether with this playground
to keep on learning, with_bigger_scope is generally referred to as the "weakening" rule and tweaking it is how you get linearity :) we tend to generally also use "exchange" - the order that variables are declared in doesnt matter, and "contraction" - treating the context like a set where each element is unique.
Together exchange + contraction are effectively "implementing a Set" on the native arrays that inference rules are made of
For comparison, here's a presentation of all the above axioms - with the exact same meaning - in conventional inference rule notation. Γ can be used to refer to contexts, here I have named them "cx".
TypeOf(expr, cx, ty) itself is written cx |- expr : ty, and contexts are written as
a list of v : T. cx specifically means a context of any length. This in fact relates to BNF,
where "unknowns" in inference rules are often referred to by their nonterminals:
cx ::=
cx ::= x : T, cx
-------------- loading_a_variable_uses_its_type
x : T |- x : T
--------------------------------- type_of_x_y_tuple
x : X, y : Y |- (x, y) : Pair X Y
cx_1 |- a : A cx_2 |- b : B
distict_union cx_1 cx_2 merged_cx
--------------------------------- tuple_constructor_is_pair
merged_cx |- (a, b) : Pair A B
cx |- a : A cx |- b : B
--------------------------- tuple_constructor_is_pair'
cx |- (a, b) : Pair A B
cx |- a : A does_not_contain cx x
----------------------------------- weakening
cx, x : T |- a : AYou'll notice that they've included some predicates, distinct_union and does_not_contain
to describe the more involved logic.
These should be read as relations, just like TypeOf. does_not_contain cx x is
struct DNC(Context, Identifier); and can be built only when it's true.
Now let's bring this full circle and actually see how type contexts get closed.
You could try to take what you've learned so far and have a try at implementing the
typing judgement for a new Expr::let(Identifier, Expr , Expr) node.
While writing this I actually needed to write out the inference rule first to see the structure I wanted, so lets start there:
cx |- e : A cx, x : A |- e2 : B
------------------------------------ let-binds
cx |- let x = e in e2 : T"A let expression is well typed in a context when we can evaluate the bound value and then the body evaluates in the context extended with the binder"
fn let_binds(binder: Identifier, expr: TypeOf, body: TypeOf) -> TypeOf {
assert!(body.in_context.all(|(name, ty)| expr.in_context.get(name) == Some(ty) || binder == name));
TypeOf {
expression: Expr::Let(binder, expr.expression, body.expression),
ty: body.ty,
in_context: expr.context
}
}