This document explains the typing rules that arise from type-lifted GSLTs. We cover the notation, core rules, and how to derive and read typing judgments.
Target audience: Compiler engineers implementing type checkers
Prerequisites: Read 05-type-lifting.md for the transformation rules.
This section is critical for understanding the rest of the documentation. If you're unfamiliar with type theory notation, read this section carefully.
The most fundamental symbol:
A : B means "A has type B"
Examples:
0 : Nat - "zero has type natural number"true : Bool - "true has type boolean"P : type^Process - "P is a process type"The turnstile |- (Unicode: $\vdash$) means "derives" or "proves":
G |- A : B means "in context G, A has type B"
Read as: "From the assumptions in G, we can derive that A has type B."
Examples:
|- 0 : 00 - "with no assumptions, the nil process has type nil-type"x : N |- *x : **x - "assuming x is a name, *x has type **x"A context is a list of typing assumptions:
G = x1 : X1, x2 : X2, ..., xn : Xn
Think of it as a symbol table or environment.
| Context | Meaning |
|---|---|
empty or |- | No assumptions (empty context) |
x : N | One assumption: variable x has type N |
x : N, y : P | Two assumptions: x is a name, y is a process |
G, z : T | Context G extended with z : T |
An inference rule has this structure:
premise1 premise2 ... premiseN
---------------------------------------- (rule-name)
conclusion
The horizontal line means "therefore" or "implies":
Example:
G |- f : A -> B G |- x : A
-------------------------------- (app)
G |- f(x) : B
Read: "If f has function type A -> B, and x has type A, then f(x) has type B."
Let's walk through this RHO typing rule step by step:
G |- A : s^N G |- B : s^P G |- x : A G |- Q : B
--------------------------------------------------------- (!-intro)
G |- !(x, Q) : !!(A, B, x)
Breaking it down:
| Premise | Reading |
|---|---|
G |- A : s^N | "In context G, A is a name type at level s" |
G |- B : s^P | "In context G, B is a process type at level s" |
G |- x : A | "In context G, x has type A (which is a name type)" |
G |- Q : B | "In context G, Q has type B (which is a process type)" |
Conclusion: G |- !(x, Q) : !!(A, B, x) - "the send process !(x, Q) has type !!(A, B, x)"
Intuition: To type a send, we need the types of the channel and message.
Conventions used throughout:
| Convention | Typical Meaning |
|---|---|
| Capital letters: A, B, T, X | Types or metavariables over types |
| Lowercase letters: a, t, x | Terms or term variables |
| Greek letters: G, D | Contexts |
| s, s1, s2 | Type levels (type, kind, etc.) |
| P, Q | Processes (in RHO/Ambient) |
| N | Names (in RHO/Ambient) |
B[x/y] means "B with x substituted for y"
Example: If B = y + 1, then B[5/y] = 5 + 1
| Symbol | Name | Meaning |
|---|---|---|
: | Colon | "has type" |
\|- | Turnstile | "derives" or "proves" |
G | Context | List of assumptions |
-> | Arrow | Function type |
x | Times | Product type |
s^T | Superscript | Classifier at level s for shape T |
------ | Rule line | "therefore" |
[a/x] | Substitution | Replace x with a |
In typed lambda calculi, we have a hierarchy:
terms : types : kinds : sorts ...
Each level classifies the level below:
s^T$ NotationIn MeTTaIL, we use s^T to denote the classifier of shape T at level s:
| Notation | Meaning |
|---|---|
type^P | The type of processes (kind of process types) |
kind^P | The kind of process types |
type^N | The type of names (kind of name types) |
type^R | The type of reductions |
When we write s without a superscript, it ranges over {type, kind}.
The name comes from the multidimensional structure:
This forms a hypercube of possible type/kind combinations.
| Calculus | Shapes | Type Levels |
|---|---|---|
| lambda | P | $\text{type}^P$, $\text{kind}^P$ |
| SKI | P | $\text{type}^P$, $\text{kind}^P$ |
| RHO | P, N, R | $\text{type}^P$, $\text{type}^N$, $\text{type}^R$, $\text{kind}^P$, $\text{kind}^N$ |
| Ambient | P, N, M, R | $\text{type}^P$, $\text{type}^N$, $\text{type}^M$, $\text{type}^R$, $\text{kind}^P$, ... |
| MeTTa | Term, State, KB, List, MSet | $\text{type}^\text{Term}$, $\text{type}^\text{State}$, $\text{type}^\text{KB}$, ... |
Example in RHO:
00 : type^P - the nil process type is a process type**(@(@0)) : type^P - the type of a dereferenced quoted quoted nilThese rules form the foundation, independent of specific calculi.
Base types exist at each level:
--------------- (axiom)
|- type^T : kind^T
For each generating shape T.
Examples:
|- type^P : kind^P - process types form a kind|- type^N : kind^N - name types form a kindVariables have their declared types:
G |- A : s
----------------- (start)
G, x : A |- x : A
Reading: If A is a valid type (at level s), then in a context where x : A, we can derive x : A.
Example in lambda:
|- P : type^P
------------------ (start)
x : P |- x : P
Extra assumptions don't invalidate typing:
G |- A : B G |- C : s
-------------------------- (weak)
G, x : C |- A : B
Reading: If A : B in G, and C is a valid type, then A : B still holds in G extended with x : C.
G |- A : s G |- B : s
-------------------------- (arrow-form)
G |- (A -> B) : s
G, x : A |- t : B
------------------- (arrow-intro)
G |- \x.t : (A -> B)
G |- f : (A -> B) G |- a : A
--------------------------------- (arrow-elim)
G |- f(a) : B
These are crucial for lambda-calculus and for continuations in RHO and Ambient.
Each function symbol generates typing rules following a pattern.
For each function symbol f : A1 x ... x An -> B:
ff : T(A1) x ... x T(An) -> T(B)fffApplication:
Type formation:
G |- A : s^P G |- B : s^P
------------------------------ (AppApp-form)
G |- AppApp(A, B) : s^P
Term introduction:
G |- A : s^P G |- B : s^P G |- f : A G |- x : B
--------------------------------------------------------- (App-intro)
G |- App(f, x) : AppApp(A, B)
Abstraction:
Type formation:
G |- A : s^P G, x : A |- B : s^P
------------------------------------- (LamLam-form)
G |- LamLam(A, \x.B) : s^P
Term introduction:
G |- A : s^P G, x : A |- B : s^P G, x : A |- t : B
---------------------------------------------------------- (Lam-intro)
G |- Lam(\x.t) : LamLam(A, \x.B)
Combinators (constants):
-------------- (S-type)
|- S : SS
-------------- (K-type)
|- K : KK
-------------- (I-type)
|- I : II
Application is same as lambda-calculus.
Nil process:
-------------- (00-form)
|- 00 : s^P
-------------- (0-intro)
|- 0 : 00
Parallel composition:
Type formation:
G |- A : s^P G |- B : s^P
------------------------------ (||-form)
G |- ||(A, B) : s^P
Type-level equations:
G |- A : s^P
--------------------- (||-unit)
G |- ||(A, 00) = A
G |- A : s^P G |- B : s^P
------------------------------ (||-comm)
G |- ||(A, B) = ||(B, A)
G |- A : s^P G |- B : s^P G |- C : s^P
---------------------------------------------- (||-assoc)
G |- ||(||(A, B), C) = ||(A, ||(B, C))
Term introduction:
G |- A : s^P G |- B : s^P G |- P : A G |- Q : B
--------------------------------------------------------- (|-intro)
G |- |(P, Q) : ||(A, B)
Send:
Type formation (with channel parameter):
G |- A : s^N G |- B : s^P G |- x : A
-------------------------------------------- (!!-form)
G |- !!(A, B, x) : s^P
Term introduction:
G |- A : s^N G |- B : s^P G |- x : A G |- Q : B
--------------------------------------------------------- (!-intro)
G |- !(x, Q) : !!(A, B, x)
Receive:
Type formation:
G |- A : s1^N G |- B : s2^N G, y : B |- C : s3^P G |- x : A
---------------------------------------------------------------------- (??-form)
G |- ??(A, B, \y.C, x) : s3^P
Term introduction:
G |- A : s1^N G |- B : s2^N G, y : B |- C : s3^P
G |- x : A G, y : B |- Q : C
---------------------------------------------------- (?-intro)
G |- ?(x, \y.Q) : ??(A, B, \y.C, x)
Quote and Dereference:
G |- A : s^P
----------------- (@@-form)
G |- @@(A) : s^N
G |- A : s^P G |- P : A
--------------------------- (@-intro)
G |- @(P) : @@(A)
G |- A : s^N
----------------- (**-form)
G |- **(A) : s^P
G |- A : s^N G |- x : A
--------------------------- (*-intro)
G |- *(x) : **(A)
Quote/dereference equations at type level:
G |- A : s^P
------------------- (@@**-inverse)
G |- **@@(A) = A
G |- A : s^N
------------------- (@@**-inverse)
G |- @@**(A) = A
Based on the state machine model:
List construction:
G |- A : type^Term G |- B : type^List G |- t : A G |- l : B
---------------------------------------------------------------------- (cons-intro)
G |- cons(t, l) : conscons(A, B)
Multiset insertion:
G |- A : type^Term G |- B : type^MSet G |- t : A G |- m : B
---------------------------------------------------------------------- (insert-intro)
G |- insert(t, m) : insertinsert(A, B)
State construction:
G |- I : type^Term G |- K : type^KB G |- W : type^MSet G |- O : type^MSet
G |- i : I G |- k : K G |- w : W G |- o : O
------------------------------------------------------------------------------------ (state-intro)
G |- state(i, k, w, o) : statestate(I, K, W, O)
Reductions have types too, describing their sources and targets.
G |- A : s^R
------------------------ (srcsrc-form)
G |- srcsrc(A) : s^P
G |- A : s^R
------------------------ (tgttgt-form)
G |- tgttgt(A) : s^P
G |- A : s^R G |- r : A
--------------------------- (src-intro)
G |- src(r) : srcsrc(A)
G |- A : s^R G |- r : A
--------------------------- (tgt-intro)
G |- tgt(r) : tgttgt(A)
Lambda-calculus beta:
src(beta(K, N)) = App(Lam(K), N)
tgt(beta(K, N)) = ev(K, N)
At the type level:
srcsrc(betabeta(A, \x.B, C)) = AppApp(LamLam(A, \x.B), C)
tgttgt(betabeta(A, \x.B, C)) = B[C/x]
RHO comm:
src(comm(x, K, Q)) = |(?(x, K), !(x, Q))
tgt(comm(x, K, Q)) = ev(K, @(Q))
At the type level:
srcsrc(commcomm(A, B, \y.C, x)) = ||(??(A, B, \y.C, x), !!(A, **(B), x))
tgttgt(commcomm(A, B, \y.C, x)) = C -- (y does not appear free in C)
Parallel context (RHO, Ambient):
G |- A : s^R G |- B : s^P
----------------------------- (par1par1-form)
G |- par1par1(A, B) : s^R
G |- A : s^R G |- B : s^P
--------------------------------------------- (par1-srcsrc)
G |- srcsrc(par1par1(A, B)) = ||(srcsrc(A), B)
G |- A : s^R G |- B : s^P
--------------------------------------------- (par1-tgttgt)
G |- tgttgt(par1par1(A, B)) = ||(tgttgt(A), B)
Following Wells & Stay's "Behavior in Higher-Order Languages", the transition system for a lambda theory can be derived automatically via relative pushouts (RPOs) rather than explicitly specified.
Rather than manually specifying modal types for each context (like ctxrecv_i,
ctxcomm_d, etc.), the derived transition system computes transitions as
idempotent pushouts (IPOs):
Γ ⊢ t⃗ →[c] d⟨⟨r⃗⟩⟩
where:
t⃗ is the source term(s)c is the minimal context (label) enabling the rewrited\langle \langle r⃗\rangle\rangle$ is the target term in context d with arguments r⃗The label c represents what the environment must provide to enable the reduction.
For a rewrite rule p ⇝ q and term t:
Γ ⊢ t →[c] d⟨⟨r⃗⟩⟩
if there exists an IPO square:
p ←— Γ'
↓ ↓
t ←— c
where c is the minimal context such that c(t) contains a redex matching p.
The modal types ctxrecv_i, ctxcomm_d, etc. from 05-type-lifting.md
are derivable from the RPO computation:
| Modal Type | Derived From |
|---|---|
ctxrecv_i(...) | IPO for comm rule with receive context |
ctxsend_i(...) | IPO for comm rule with send context |
ctxcomm_i(...) | IPO for comm rule with sent-process context |
ctxposs_i(T) | General possibility via reflexive-transitive closure |
Implementation note: The current explicit modal type generation in MeTTaIL is a concrete implementation strategy for the abstract RPO derivation. Both approaches produce equivalent typing information.
IPOs (idempotent pushouts) ensure that:
This is proven in Theorem 20 and Theorem 22 of the Behavior paper.
For behavioral equivalence (bisimilarity) to be preserved under all contexts, we need conditions on the calculus structure.
Reactive context: A context containing a redex pattern. For example:
\text{out}(n, -) | \text{in}(n, \lambda x.q)$ in RHO is reactive (contains comm redex pattern)\text{App}(\text{Lam}(K), -)$ in lambda-calculus is reactive (contains beta redex pattern)Transparent context: A non-reactive context c where there exists a unique
complementary context c̄ such that for any term t:
c(t) →[c̄] d(t)
If a calculus is transparent (all non-reactive contexts are transparent), then weak bisimilarity is a congruence.
The RHO calculus and lambda-calculus are both transparent.
This means:
p \approx q$ (p and q are behaviorally equivalent)C[p] \approx C[q]$ for any context CA stronger condition: context g is IPO uniform if transitions factor
predictably through sublists of the context.
Theorem 22: If every context is either reactive or IPO uniform, weak bisimilarity is a congruence.
These conditions ensure that:
| Condition | Definition | Ensures |
|---|---|---|
| Transparency | Non-reactive contexts have unique complementary labels | Weak bisimilarity congruence |
| IPO Uniformity | Transitions factor through context sublists | Strong congruence property |
| Reactive | Context contains redex pattern | Context participates in reduction |
Goal: Derive the type of Lam(\x.x) (the identity function).
Derivation tree:
|- P : type^P
---------------- (start)
|- P : type^P x : P |- x : P
----------------------------------------------- (Lam-intro)
|- Lam(\x.x) : LamLam(P, \x.P)
Result: Lam(\x.x) : LamLam(P, \x.P)
This is the identity function with type "for any type P, takes P and returns P".
Goal: Type the process |(?(x, \y.*y), !(x, 0)) - a receive and send in parallel.
Setup:
x : N (x is a name)Derivation (sketch):
Type the send:
x : N |- !(x, 0) : !!(N, 00, x)
Type the receive:
x : N |- ?(x, \y.*y) : ??(N, @@(00), \y.**@@(00), x)
The continuation \y.*y has type \y.**y, which at type @@(00) gives **(@@(00)).
Combine with parallel:
x : N |- |(?(x, \y.*y), !(x, 0)) : ||(??(N, @@(00), \y.**(@@(00)), x), !!(N, 00, x))
The reduction comm(x, \y.*y, 0) has:
|(?(x, \y.*y), !(x, 0))*(@0) = *(@0) which reduces to 0Type of the reduction:
commcomm(N, @@(00), \y.**(@@(00)), x)
Source type (via srcsrc):
||(??(N, @@(00), \y.**(@@(00)), x), !!(N, **(@@(00)), x))
Target type (via tgttgt):
**(@@(00)) = 00 (by the @@**-inverse equation)
Here's a complete derivation for typing !(x, 0) in context x : N:
--------------- (00-form)
|- 00 : type^P
--------------- (0-intro)
--------------- (axiom) --------------- (weak) |- 0 : 00
|- N : type^N x : N |- N : type^N --------------- (weak)
--------------- (weak) --------------- (start) x : N |- 0 : 00
x : N |- N : type^N x : N |- x : N
------------------------------------------------------------ (!-intro)
x : N |- !(x, 0) : !!(N, 00, x)
The standard approach is bidirectional type checking:
enum Mode {
Check { expected: Type }, // check term against known type
Infer, // infer type from term
}
fn typecheck(ctx: &Context, term: &Term, mode: Mode) -> Result<Type, TypeError> {
match (term, mode) {
// Variable: look up in context
(Term::Var(name), Mode::Infer) => {
ctx.lookup(name).ok_or(TypeError::Unbound(name.clone()))
}
// Application: infer function type, check argument
(Term::App(f, arg), Mode::Infer) => {
let fn_type = typecheck(ctx, f, Mode::Infer)?;
match fn_type {
Type::Arrow(a, b) => {
typecheck(ctx, arg, Mode::Check { expected: *a })?;
Ok(*b)
}
_ => Err(TypeError::NotAFunction(fn_type))
}
}
// Abstraction: extend context, check body
(Term::Lam(var, body), Mode::Check { expected: Type::Arrow(a, b) }) => {
let extended = ctx.extend(var.clone(), *a.clone());
typecheck(&extended, body, Mode::Check { expected: *b })?;
Ok(Type::Arrow(a, b))
}
// Send: infer channel and message types
(Term::Send(chan, msg), Mode::Infer) => {
let chan_type = typecheck(ctx, chan, Mode::Infer)?;
let msg_type = typecheck(ctx, msg, Mode::Infer)?;
// chan_type should be a name type
Ok(Type::SendType(Box::new(chan_type), Box::new(msg_type), chan.clone()))
}
// Check mode: infer and compare
(term, Mode::Check { expected }) => {
let inferred = typecheck(ctx, term, Mode::Infer)?;
if types_equal(&inferred, &expected) {
Ok(inferred)
} else {
Err(TypeError::Mismatch { expected, actual: inferred })
}
}
}
}
#[derive(Clone)]
struct Context {
bindings: Vec<(String, Type)>,
}
impl Context {
fn empty() -> Self {
Context { bindings: vec![] }
}
fn extend(&self, name: String, ty: Type) -> Self {
let mut new = self.clone();
new.bindings.push((name, ty));
new
}
fn lookup(&self, name: &str) -> Option<Type> {
self.bindings.iter().rev()
.find(|(n, _)| n == name)
.map(|(_, ty)| ty.clone())
}
}
Handle type-level equations (like multiset commutativity):
fn types_equal(t1: &Type, t2: &Type) -> bool {
// Normalize both types first
let n1 = normalize(t1);
let n2 = normalize(t2);
syntactic_equal(&n1, &n2)
}
fn normalize(ty: &Type) -> Type {
match ty {
// ||(A, 00) = A
Type::Par(a, b) if **b == Type::Nil => normalize(a),
// ||(00, A) = A
Type::Par(a, b) if **a == Type::Nil => normalize(b),
// ||(A, B) -> canonical order (for commutativity)
Type::Par(a, b) => {
let na = normalize(a);
let nb = normalize(b);
if type_ord(&na) > type_ord(&nb) {
Type::Par(Box::new(nb), Box::new(na))
} else {
Type::Par(Box::new(na), Box::new(nb))
}
}
// @@(**(A)) = A
Type::Quote(inner) => match &**inner {
Type::Deref(a) => normalize(a),
_ => Type::Quote(Box::new(normalize(inner)))
}
// **(@@(A)) = A
Type::Deref(inner) => match &**inner {
Type::Quote(a) => normalize(a),
_ => Type::Deref(Box::new(normalize(inner)))
}
// Recursively normalize other types
_ => ty.clone()
}
}
fn generate_rules(gslt: &GSLT) -> Vec<InferenceRule> {
let mut rules = vec![];
// Core rules (axiom, start, weakening, arrow)
rules.extend(core_rules());
// Formation rules for each type constructor
for morph in &gslt.type_morphisms {
rules.push(generate_formation_rule(morph));
}
// Introduction rules for each term constructor
for morph in &gslt.term_morphisms {
rules.push(generate_intro_rule(morph, &gslt.type_morphisms));
}
// Equation rules for structural equations
for eq in &gslt.equations {
rules.push(generate_equation_rule(eq));
}
// Source/target rules for reductions
for red in &gslt.reductions {
rules.extend(generate_reduction_rules(red));
}
rules
}
fn generate_intro_rule(term_morph: &Morphism, type_morphs: &[Morphism]) -> InferenceRule {
// Find corresponding type-level morphism
let type_morph = type_morphs.iter()
.find(|m| m.name == format!("{}{}", term_morph.name, term_morph.name))
.expect("type-lifted morphism must exist");
// Generate premises: type well-formedness + term typing
let mut premises = vec![];
// Type well-formedness premises
for (i, ty) in type_morph.inputs.iter().enumerate() {
premises.push(Judgment {
context: Context::meta("G"),
term: Term::meta(format!("T{}", i)),
ty: Type::sort_at_level(ty.sort(), "s"),
});
}
// Term typing premises
for (i, (tm_input, ty_input)) in term_morph.inputs.iter().zip(type_morph.inputs.iter()).enumerate() {
premises.push(Judgment {
context: Context::meta("G"),
term: Term::meta(format!("t{}", i)),
ty: Type::meta(format!("T{}", i)),
});
}
// Conclusion
let conclusion = Judgment {
context: Context::meta("G"),
term: Term::app(term_morph.name.clone(), (0..term_morph.inputs.len()).map(|i| Term::meta(format!("t{}", i))).collect()),
ty: Type::app(type_morph.name.clone(), (0..type_morph.inputs.len()).map(|i| Type::meta(format!("T{}", i))).collect()),
};
InferenceRule {
name: format!("{}-intro", term_morph.name),
premises,
conclusion,
}
}
struct TypeChecker {
normalization_cache: HashMap<Type, Type>,
checked_terms: HashMap<(TermId, Type), bool>,
}
impl TypeChecker {
fn normalize_cached(&mut self, ty: &Type) -> Type {
if let Some(cached) = self.normalization_cache.get(ty) {
return cached.clone();
}
let result = normalize(ty);
self.normalization_cache.insert(ty.clone(), result.clone());
result
}
}
Core rules:
Pattern for term constructors:
ff for each fReduction typing:
src, tgt at term levelsrcsrc, tgttgt at type level| Symbol | Meaning |
|---|---|
\|- | "proves" or "derives" |
G | Context (list of assumptions) |
: | "has type" |
s^T | Level s classifier for shape T |
------ | "therefore" (conclusion below) |
= | Definitional equality |
[a/x] | Substitution of a for x |
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |