Bidirectional Type Checking
The type inference engine represents the most component of our System F-ω implementation. Built around the DK (Dunfield-Krishnaswami) worklist algorithm, it handles the complex interactions between higher-rank polymorphism, existential type variables, and bidirectional type checking that make System F-ω both powerful and challenging to implement efficiently.
The algorithm operates on a worklist of judgments and constraints, systematically reducing complex type checking problems into simpler ones until all constraints are resolved. This approach provides decidable type inference for System F-ω while maintaining principal types and supporting polymorphic programming patterns.
Notably this approach is different than our direct tree-walking approach before. Now we walk the syntax tree and emit constraints, which are then solved by the worklist algorithm, and then back-propagate the results to the original syntax tree to give the final types. This system allows more copmlex rules to be introduced, but it also makes the entire process “non-local” in the sense that we are looking at a constraint generated by many different expressions, and thus do error reporting becomes a bit more challenging because tracing back a constraint problem to its original syntax requires quite a bit of bookkeeping
Typing Rules
Now we’re going to bodly go into the next generation of type checking. We have some new symbols in our type system, but they’re mostly the same as before except for the addition of new kind-level operations.
-
\( \Gamma \) (Gamma) - The typing context that stores information about variables and their types.
-
\( \vdash \) (Turnstile) - The “proves” relation, meaning “given this context, we can conclude this judgment.”
-
\( \Rightarrow \) (Double Right Arrow) - Synthesis mode, where the type checker figures out what type an expression has.
-
\( \Leftarrow \) (Double Left Arrow) - Checking mode, where we verify that an expression has the expected type.
-
\( \forall\alpha \) (Forall Alpha) - Universal quantification, meaning “for any type α.”
-
\( :: \) (Double Colon) - The “has kind” relation, telling us what category a type constructor belongs to.
-
\( \star \) (Star) - The kind of concrete types like
Int,Bool, andString. -
\( \square \) (Box) - The kind of kinds, the kind that kinds themselves have.
-
\( \to \) (Arrow) - Function types at the term level, or kind arrows at the type level.
-
\( [B/\alpha]A \) - Type substitution that replaces all occurrences of type variable α with type B in type A.
-
\( \Lambda\alpha \) (Big Lambda) - Type abstraction that creates polymorphic functions at the type level.
-
\( \kappa \) (Kappa) - Kind variables representing unknown categories in our type system.
-
\( \overline{x} \) - Overline notation indicating a sequence or list of elements, such as multiple variables or arguments.
Before examining the DK worklist algorithm implementation, let’s establish the formal typing rules that govern System F-ω. These rules extend System F with higher-kinded types and more polymorphism.
Basic Expression Rules
Variable lookup finds types in the context:
\[ \frac{x : A \in \Gamma}{\Gamma \vdash x \Rightarrow A} \text{(T-Var)} \]
Function application with bidirectional checking:
\[ \frac{\Gamma \vdash e_1 \Rightarrow A \to B \quad \Gamma \vdash e_2 \Leftarrow A}{\Gamma \vdash e_1 ; e_2 \Rightarrow B} \text{(T-App)} \]
Lambda abstraction in checking mode:
\[ \frac{\Gamma, x : A \vdash e \Leftarrow B}{\Gamma \vdash \lambda x. e \Leftarrow A \to B} \text{(T-Lam)} \]
Type Application and Abstraction
Type application instantiates polymorphic expressions:
\[ \frac{\Gamma \vdash e \Rightarrow \forall \alpha :: \kappa. A \quad \Gamma \vdash B :: \kappa}{\Gamma \vdash e ; [B] \Rightarrow [B/\alpha]A} \text{(T-TApp)} \]
Type abstraction introduces universal quantification:
\[ \frac{\Gamma, \alpha :: \kappa \vdash e \Leftarrow A}{\Gamma \vdash \Lambda \alpha :: \kappa. e \Leftarrow \forall \alpha :: \kappa. A} \text{(T-TAbs)} \]
Higher-Kinded Type Rules
Kind checking ensures type constructors are well-formed:
\[ \frac{}{\Gamma \vdash \star :: \square} \text{(K-Type)} \]
\[ \frac{\Gamma \vdash \kappa_1 :: \square \quad \Gamma \vdash \kappa_2 :: \square}{\Gamma \vdash \kappa_1 \to \kappa_2 :: \square} \text{(K-Arrow)} \]
Type constructor application:
\[ \frac{\Gamma \vdash F :: \kappa_1 \to \kappa_2 \quad \Gamma \vdash A :: \kappa_1}{\Gamma \vdash F ; A :: \kappa_2} \text{(K-App)} \]
Pattern Matching Rules
Constructor patterns check against data types:
\[ \frac{\Gamma \vdash e \Rightarrow T \quad \overline{\Gamma \vdash p_i \Leftarrow T \leadsto \Delta_i \quad \Gamma, \Delta_i \vdash e_i \Leftarrow A}}{\Gamma \vdash \text{match } e \text{ with } \overline{p_i \to e_i} \Rightarrow A} \text{(T-Match)} \]
Bidirectional Control
Mode switching from inference to checking:
\[ \frac{\Gamma \vdash e \Rightarrow A}{\Gamma \vdash e \Leftarrow A} \text{(T-Sub)} \]
Existential variable instantiation:
\[ \frac{\Gamma, \hat{\alpha} :: \kappa \vdash e \Rightarrow A}{\Gamma \vdash e \Rightarrow [\hat{\alpha}/\alpha]A} \text{(T-InstL)} \]
In these rules, \( \Rightarrow \) denotes inference mode (synthesizing types), \( \Leftarrow \) denotes checking mode (verifying against expected types), \( :: \) relates types to their kinds, and \( \hat{\alpha} \) represents existential type variables solved during inference.
The DK Worklist Algorithm
The DK algorithm represents type inference as a constraint solving problem. Instead of recursively traversing expressions and immediately making type checking decisions, it accumulates constraints in a worklist and processes them systematically.
Worklist Structure
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::core::{CoreBinOp, CorePattern, CoreTerm, CoreType}; use crate::errors::{TypeError, TypeResult}; /// DK Worklist Algorithm for System-F-ω /// Based on "A Mechanical Formalization of Higher-Ranked Polymorphic Type /// Inference" pub type TyVar = String; pub type TmVar = String; #[derive(Debug, Clone, PartialEq)] pub enum TyVarKind { /// Universal type variable: α Universal, /// Existential type variable: ^α Existential, /// Solved existential: ^α = τ Solved(CoreType), /// Marker: ►α (for scoping) Marker, } #[derive(Debug, Clone, PartialEq)] pub enum Judgment { /// Subtyping: A <: B Sub { left: CoreType, right: CoreType }, /// Type inference: e ⊢ A Inf { term: CoreTerm, ty: CoreType }, /// Type checking: e ⇐ A Chk { term: CoreTerm, ty: CoreType }, /// Application inference helper: A • e ⊢ C InfApp { func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, }, } #[derive(Debug, Clone)] pub struct Worklist { entries: Vec<WorklistEntry>, next_var: usize, } impl Default for Worklist { fn default() -> Self { Self::new() } } impl Worklist { pub fn new() -> Self { Worklist { entries: Vec::new(), next_var: 0, } } pub fn fresh_var(&mut self) -> TyVar { let var = format!("α{}", self.next_var); self.next_var += 1; var } pub fn fresh_evar(&mut self) -> TyVar { let var = format!("^α{}", self.next_var); self.next_var += 1; var } pub fn push(&mut self, entry: WorklistEntry) { self.entries.push(entry); } pub fn pop(&mut self) -> Option<WorklistEntry> { self.entries.pop() } pub fn find_var(&self, name: &str) -> Option<&CoreType> { for entry in self.entries.iter().rev() { if let WorklistEntry::Var(var_name, ty) = entry { if var_name == name { return Some(ty); } } } None } pub fn solve_evar(&mut self, name: &str, ty: CoreType) -> TypeResult<()> { for entry in self.entries.iter_mut() { if let WorklistEntry::TVar(var_name, kind) = entry { if var_name == name { match kind { TyVarKind::Existential => { *kind = TyVarKind::Solved(ty); return Ok(()); } TyVarKind::Solved(_) => { // Variable already solved, that's OK return Ok(()); } _ => { // Skip universal variables, markers, etc. continue; } } } } } Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } pub fn before(&self, a: &str, b: &str) -> bool { let mut pos_a = None; let mut pos_b = None; for (i, entry) in self.entries.iter().enumerate() { if let WorklistEntry::TVar(name, _) = entry { if name == a { pos_a = Some(i); } if name == b { pos_b = Some(i); } } } match (pos_a, pos_b) { (Some(pa), Some(pb)) => pa < pb, _ => false, } } } pub struct DKInference { worklist: Worklist, trace: Vec<String>, data_constructors: HashMap<String, CoreType>, /// Variable typing context for pattern-bound variables var_context: HashMap<String, CoreType>, } impl DKInference { pub fn with_context( data_constructors: HashMap<String, CoreType>, var_context: HashMap<String, CoreType>, ) -> Self { DKInference { worklist: Worklist::new(), trace: Vec::new(), data_constructors, var_context, } } pub fn check_type(&mut self, term: &CoreTerm, expected_ty: &CoreType) -> TypeResult<()> { self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: term.clone(), ty: expected_ty.clone(), })); self.solve() } fn solve(&mut self) -> TypeResult<()> { while let Some(entry) = self.worklist.pop() { match entry { WorklistEntry::TVar(_, _) => { // Skip variable bindings during processing continue; } WorklistEntry::Var(_, _) => { // Skip term variable bindings during processing continue; } WorklistEntry::Judgment(judgment) => { self.solve_judgment(judgment)?; } } } Ok(()) } fn solve_judgment(&mut self, judgment: Judgment) -> TypeResult<()> { match judgment { Judgment::Sub { left, right } => self.solve_subtype(left, right), Judgment::Inf { term, ty } => self.solve_inference(term, ty), Judgment::Chk { term, ty } => self.solve_checking(term, ty), Judgment::InfApp { func_ty, arg, result_ty, } => self.solve_inf_app(func_ty, arg, result_ty), } } fn solve_subtype(&mut self, left: CoreType, right: CoreType) -> TypeResult<()> { self.trace.push(format!("Sub {} <: {}", left, right)); if left == right { return Ok(()); } match (&left, &right) { // Reflexivity (CoreType::Con(a), CoreType::Con(b)) if a == b => Ok(()), (CoreType::Var(a), CoreType::Var(b)) if a == b => Ok(()), (CoreType::ETVar(a), CoreType::ETVar(b)) if a == b => Ok(()), // Function subtyping (contravariant in argument, covariant in result) (CoreType::Arrow(a1, a2), CoreType::Arrow(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *b1.clone(), right: *a1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Application subtyping (covariant in both components) (CoreType::App(a1, a2), CoreType::App(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a1.clone(), right: *b1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Forall right (_, CoreType::Forall(var, ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left, right: substituted_ty, })); Ok(()) } // Forall left (CoreType::Forall(var, ty), _) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted_ty = self.substitute_type(var, &CoreType::ETVar(fresh_evar), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: substituted_ty, right, })); Ok(()) } // Existential variable instantiation (CoreType::ETVar(a), _) if !self.occurs_check(a, &right) => { self.instantiate_left(a, &right) } (_, CoreType::ETVar(a)) if !self.occurs_check(a, &left) => { self.instantiate_right(&left, a) } _ => Err(TypeError::SubtypingError { left, right, span: None, }), } } fn solve_inference(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Inf {} ⊢ {}", self.term_to_string(&term), ty)); match term { CoreTerm::Var(name) => { // Check pattern variable context first if let Some(var_ty) = self.var_context.get(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.worklist.find_var(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.data_constructors.get(&name).cloned() { // Check data constructors for constructor variables self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } } CoreTerm::LitInt(_) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::Con("Int".to_string()), right: ty, })); Ok(()) } CoreTerm::Lambda { param, param_ty, body, } => { let result_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &result_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(result_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: arrow_ty, right: ty, })); self.worklist.push(WorklistEntry::Var(param, param_ty)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: result_ty, })); Ok(()) } CoreTerm::App { func, arg } => { let func_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &func_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: func_ty.clone(), arg: *arg, result_ty: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *func, ty: func_ty, })); Ok(()) } CoreTerm::TypeLambda { param, body } => { let body_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &body_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let forall_ty = CoreType::Forall(param.clone(), Box::new(body_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: forall_ty, right: ty, })); self.worklist .push(WorklistEntry::TVar(param, TyVarKind::Universal)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: body_ty, })); Ok(()) } CoreTerm::Constructor { name, args: _ } => { if let Some(constructor_ty) = self.data_constructors.get(&name) { // Instantiate the constructor type with fresh existential variables let instantiated_ty = self.instantiate_constructor_type(constructor_ty.clone()); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: instantiated_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } CoreTerm::BinOp { op, left, right } => { let (left_ty, right_ty, result_ty) = self.infer_binop_types(&op); // Add any existential variables to the worklist self.add_etvars_to_worklist(&left_ty); self.add_etvars_to_worklist(&right_ty); self.add_etvars_to_worklist(&result_ty); // Check that the operands have the expected types self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *left, ty: left_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *right, ty: right_ty, })); // Check that the result type matches the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_ty, right: ty, })); Ok(()) } CoreTerm::If { cond, then_branch, else_branch, } => { // The condition must be Bool self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *cond, ty: CoreType::Con("Bool".to_string()), })); // Both branches must have the same type as the expected result self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *then_branch, ty: ty.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *else_branch, ty, })); Ok(()) } CoreTerm::Case { scrutinee, arms } => { // Create a fresh type variable for the scrutinee let scrutinee_ty = CoreType::ETVar(self.worklist.fresh_evar()); self.add_etvars_to_worklist(&scrutinee_ty); // Check that the scrutinee has the inferred type self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *scrutinee, ty: scrutinee_ty.clone(), })); // Process each pattern arm for arm in arms { // Check pattern constraints and get pattern variable bindings let pattern_bindings = self.check_pattern(&arm.pattern, &scrutinee_ty)?; // Add pattern variable bindings to worklist as regular variables for (var_name, var_type) in pattern_bindings { self.worklist.push(WorklistEntry::Var(var_name, var_type)); } // Check the body with pattern variables in the worklist self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arm.body.clone(), ty: ty.clone(), })); } Ok(()) } } } fn solve_checking(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Chk {} ⇐ {}", self.term_to_string(&term), ty)); match (&term, &ty) { ( CoreTerm::Lambda { param, param_ty, body, }, CoreType::Arrow(expected_param, result_ty), ) => { // Check that parameter types match self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: param_ty.clone(), right: *expected_param.clone(), })); self.worklist .push(WorklistEntry::Var(param.clone(), param_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *body.clone(), ty: *result_ty.clone(), })); Ok(()) } (_, CoreType::Forall(var, body_ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), body_ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term, ty: substituted_ty, })); Ok(()) } _ => { // Fallback: infer type and check subtyping let inferred_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &inferred_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: inferred_ty.clone(), right: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term, ty: inferred_ty, })); Ok(()) } } } fn solve_inf_app( &mut self, func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, ) -> TypeResult<()> { match func_ty { CoreType::Arrow(param_ty, ret_ty) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: *param_ty, })); Ok(()) } CoreType::Forall(var, body) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(&var, &CoreType::ETVar(fresh_evar), &body); self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: substituted, arg, result_ty, })); Ok(()) } CoreType::ETVar(a) => { let param_ty_name = self.worklist.fresh_evar(); let ret_ty_name = self.worklist.fresh_evar(); let param_ty = CoreType::ETVar(param_ty_name.clone()); let ret_ty = CoreType::ETVar(ret_ty_name.clone()); // Add the fresh existential variables to the worklist self.worklist .push(WorklistEntry::TVar(param_ty_name, TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(ret_ty_name, TyVarKind::Existential)); let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(ret_ty.clone())); self.worklist.solve_evar(&a, arrow_ty)?; self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: param_ty, })); Ok(()) } _ => Err(TypeError::NotAFunction { ty: func_ty, span: None, }), } } fn instantiate_left(&mut self, var: &str, ty: &CoreType) -> TypeResult<()> { match ty { CoreType::ETVar(b) if self.worklist.before(var, b) => { self.worklist .solve_evar(b, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::Forall(b, t) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted = self.substitute_type(b, &CoreType::Var(fresh_var), t); self.instantiate_left(var, &substituted) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn instantiate_right(&mut self, ty: &CoreType, var: &str) -> TypeResult<()> { match ty { CoreType::ETVar(a) if self.worklist.before(var, a) => { self.worklist .solve_evar(a, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::Forall(a, t) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(a, &CoreType::ETVar(fresh_evar), t); self.instantiate_right(&substituted, var) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn occurs_check(&self, var: &str, ty: &CoreType) -> bool { match ty { CoreType::ETVar(name) | CoreType::Var(name) => name == var, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.occurs_check(var, t1) || self.occurs_check(var, t2) } CoreType::Forall(_, t) => self.occurs_check(var, t), CoreType::Product(types) => types.iter().any(|t| self.occurs_check(var, t)), _ => false, } } fn is_monotype(&self, ty: &CoreType) -> bool { match ty { CoreType::Con(_) | CoreType::Var(_) | CoreType::ETVar(_) => true, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.is_monotype(t1) && self.is_monotype(t2) } CoreType::Product(types) => types.iter().all(|t| self.is_monotype(t)), CoreType::Forall(_, _) => false, } } fn substitute_type(&self, var: &str, replacement: &CoreType, ty: &CoreType) -> CoreType { match ty { CoreType::Var(name) if name == var => replacement.clone(), CoreType::Arrow(t1, t2) => CoreType::Arrow( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Forall(bound_var, body) if bound_var != var => CoreType::Forall( bound_var.clone(), Box::new(self.substitute_type(var, replacement, body)), ), CoreType::App(t1, t2) => CoreType::App( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.substitute_type(var, replacement, t)) .collect(), ), _ => ty.clone(), } } fn term_to_string(&self, term: &CoreTerm) -> String { match term { CoreTerm::Var(name) => name.clone(), CoreTerm::LitInt(n) => n.to_string(), _ => format!("{:?}", term), // XXX: Simplified for now } } pub fn get_trace(&self) -> &[String] { &self.trace } fn infer_binop_types(&mut self, op: &CoreBinOp) -> (CoreType, CoreType, CoreType) { match op { // Arithmetic operations: Int -> Int -> Int CoreBinOp::Add | CoreBinOp::Sub | CoreBinOp::Mul | CoreBinOp::Div => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), ), // Comparison operations: Int -> Int -> Bool CoreBinOp::Lt | CoreBinOp::Le => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Bool".to_string()), ), } } fn add_etvars_to_worklist(&mut self, ty: &CoreType) { match ty { CoreType::ETVar(var_name) => { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.add_etvars_to_worklist(t1); self.add_etvars_to_worklist(t2); } CoreType::Forall(_, t) => { self.add_etvars_to_worklist(t); } CoreType::Product(types) => { for t in types { self.add_etvars_to_worklist(t); } } CoreType::Var(_) | CoreType::Con(_) => { // No existential variables to add } } } /// Check a pattern against a type and return variable bindings /// This implements pattern type checking with unification fn check_pattern( &mut self, pattern: &CorePattern, expected_ty: &CoreType, ) -> TypeResult<HashMap<String, CoreType>> { let mut bindings = HashMap::new(); match pattern { CorePattern::Wildcard => { // Wildcard matches anything, no bindings Ok(bindings) } CorePattern::Var(var_name) => { // Variable patterns bind the scrutinee type bindings.insert(var_name.clone(), expected_ty.clone()); Ok(bindings) } CorePattern::Constructor { name, args } => { // Look up constructor type from data constructor environment if let Some(constructor_ty) = self.data_constructors.get(name).cloned() { // Constructor type should be of the form: T1 -> T2 -> ... -> DataType // We need to unify the result type with expected_ty and // check argument patterns against parameter types let (param_types, result_type) = self.extract_constructor_signature(&constructor_ty)?; // The result type should unify with the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_type, right: expected_ty.clone(), })); // Check that we have the right number of pattern arguments if args.len() != param_types.len() { return Err(TypeError::ArityMismatch { expected: param_types.len(), actual: args.len(), span: None, }); } // Recursively check argument patterns for (arg_pattern, param_ty) in args.iter().zip(param_types.iter()) { let arg_bindings = self.check_pattern(arg_pattern, param_ty)?; // Merge bindings (should check for conflicts in a real implementation) for (var, ty) in arg_bindings { bindings.insert(var, ty); } } Ok(bindings) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } } } /// Extract parameter types and result type from a constructor type /// signature e.g., Int -> String -> Bool -> MyData => ([Int, String, /// Bool], MyData) fn extract_constructor_signature( &mut self, constructor_ty: &CoreType, ) -> TypeResult<(Vec<CoreType>, CoreType)> { let mut param_types = Vec::new(); let mut current_ty = constructor_ty.clone(); let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type current_ty = self.apply_type_substitutions(¤t_ty, &substitutions); // Extract parameter types from arrows while let CoreType::Arrow(param_ty, result_ty) = current_ty { param_types.push(*param_ty.clone()); current_ty = *result_ty; } // The final type is the result type Ok((param_types, current_ty)) } fn instantiate_constructor_type(&mut self, constructor_ty: CoreType) -> CoreType { let mut current_ty = constructor_ty; let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type self.apply_type_substitutions(¤t_ty, &substitutions) } fn apply_type_substitutions( &self, ty: &CoreType, substitutions: &HashMap<String, CoreType>, ) -> CoreType { match ty { CoreType::Var(name) => substitutions .get(name) .cloned() .unwrap_or_else(|| ty.clone()), CoreType::Con(name) => CoreType::Con(name.clone()), CoreType::ETVar(name) => CoreType::ETVar(name.clone()), CoreType::Arrow(left, right) => CoreType::Arrow( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::App(left, right) => CoreType::App( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::Forall(var, body) => { // Don't substitute under forall bindings - this is a simplification CoreType::Forall( var.clone(), Box::new(self.apply_type_substitutions(body, substitutions)), ) } CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.apply_type_substitutions(t, substitutions)) .collect(), ), } } } #[derive(Debug, Clone, PartialEq)] pub enum WorklistEntry { /// Type variable binding: α TVar(TyVar, TyVarKind), /// Term variable binding: x : T Var(TmVar, CoreType), /// Judgment: Sub A B | Inf e ⊢ A | Chk e ⇐ A Judgment(Judgment), } }
The worklist contains three fundamental kinds of entries that work together to manage the type checking process. Type variable bindings track type variables and their current status, which can be universal (from explicit quantifiers), existential (representing unknown types that need inference), or solved (existential variables that have been determined through constraint solving). Term variable bindings associate program variables with their inferred or declared types, maintaining the mapping between identifiers in the source code and their type information. Judgments represent the core type checking and inference tasks that remain to be completed, encoding operations like subtyping checks, type synthesis, and type verification.
This tripartite structure allows the algorithm to defer complex decisions while systematically accumulating the information needed to make them correctly. By separating variable management from the actual type checking work, the algorithm can handle intricate dependencies and ensure that all constraints are resolved in the proper order.
Type Variable Kinds
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::core::{CoreBinOp, CorePattern, CoreTerm, CoreType}; use crate::errors::{TypeError, TypeResult}; /// DK Worklist Algorithm for System-F-ω /// Based on "A Mechanical Formalization of Higher-Ranked Polymorphic Type /// Inference" pub type TyVar = String; pub type TmVar = String; #[derive(Debug, Clone, PartialEq)] pub enum WorklistEntry { /// Type variable binding: α TVar(TyVar, TyVarKind), /// Term variable binding: x : T Var(TmVar, CoreType), /// Judgment: Sub A B | Inf e ⊢ A | Chk e ⇐ A Judgment(Judgment), } #[derive(Debug, Clone, PartialEq)] pub enum Judgment { /// Subtyping: A <: B Sub { left: CoreType, right: CoreType }, /// Type inference: e ⊢ A Inf { term: CoreTerm, ty: CoreType }, /// Type checking: e ⇐ A Chk { term: CoreTerm, ty: CoreType }, /// Application inference helper: A • e ⊢ C InfApp { func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, }, } #[derive(Debug, Clone)] pub struct Worklist { entries: Vec<WorklistEntry>, next_var: usize, } impl Default for Worklist { fn default() -> Self { Self::new() } } impl Worklist { pub fn new() -> Self { Worklist { entries: Vec::new(), next_var: 0, } } pub fn fresh_var(&mut self) -> TyVar { let var = format!("α{}", self.next_var); self.next_var += 1; var } pub fn fresh_evar(&mut self) -> TyVar { let var = format!("^α{}", self.next_var); self.next_var += 1; var } pub fn push(&mut self, entry: WorklistEntry) { self.entries.push(entry); } pub fn pop(&mut self) -> Option<WorklistEntry> { self.entries.pop() } pub fn find_var(&self, name: &str) -> Option<&CoreType> { for entry in self.entries.iter().rev() { if let WorklistEntry::Var(var_name, ty) = entry { if var_name == name { return Some(ty); } } } None } pub fn solve_evar(&mut self, name: &str, ty: CoreType) -> TypeResult<()> { for entry in self.entries.iter_mut() { if let WorklistEntry::TVar(var_name, kind) = entry { if var_name == name { match kind { TyVarKind::Existential => { *kind = TyVarKind::Solved(ty); return Ok(()); } TyVarKind::Solved(_) => { // Variable already solved, that's OK return Ok(()); } _ => { // Skip universal variables, markers, etc. continue; } } } } } Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } pub fn before(&self, a: &str, b: &str) -> bool { let mut pos_a = None; let mut pos_b = None; for (i, entry) in self.entries.iter().enumerate() { if let WorklistEntry::TVar(name, _) = entry { if name == a { pos_a = Some(i); } if name == b { pos_b = Some(i); } } } match (pos_a, pos_b) { (Some(pa), Some(pb)) => pa < pb, _ => false, } } } pub struct DKInference { worklist: Worklist, trace: Vec<String>, data_constructors: HashMap<String, CoreType>, /// Variable typing context for pattern-bound variables var_context: HashMap<String, CoreType>, } impl DKInference { pub fn with_context( data_constructors: HashMap<String, CoreType>, var_context: HashMap<String, CoreType>, ) -> Self { DKInference { worklist: Worklist::new(), trace: Vec::new(), data_constructors, var_context, } } pub fn check_type(&mut self, term: &CoreTerm, expected_ty: &CoreType) -> TypeResult<()> { self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: term.clone(), ty: expected_ty.clone(), })); self.solve() } fn solve(&mut self) -> TypeResult<()> { while let Some(entry) = self.worklist.pop() { match entry { WorklistEntry::TVar(_, _) => { // Skip variable bindings during processing continue; } WorklistEntry::Var(_, _) => { // Skip term variable bindings during processing continue; } WorklistEntry::Judgment(judgment) => { self.solve_judgment(judgment)?; } } } Ok(()) } fn solve_judgment(&mut self, judgment: Judgment) -> TypeResult<()> { match judgment { Judgment::Sub { left, right } => self.solve_subtype(left, right), Judgment::Inf { term, ty } => self.solve_inference(term, ty), Judgment::Chk { term, ty } => self.solve_checking(term, ty), Judgment::InfApp { func_ty, arg, result_ty, } => self.solve_inf_app(func_ty, arg, result_ty), } } fn solve_subtype(&mut self, left: CoreType, right: CoreType) -> TypeResult<()> { self.trace.push(format!("Sub {} <: {}", left, right)); if left == right { return Ok(()); } match (&left, &right) { // Reflexivity (CoreType::Con(a), CoreType::Con(b)) if a == b => Ok(()), (CoreType::Var(a), CoreType::Var(b)) if a == b => Ok(()), (CoreType::ETVar(a), CoreType::ETVar(b)) if a == b => Ok(()), // Function subtyping (contravariant in argument, covariant in result) (CoreType::Arrow(a1, a2), CoreType::Arrow(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *b1.clone(), right: *a1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Application subtyping (covariant in both components) (CoreType::App(a1, a2), CoreType::App(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a1.clone(), right: *b1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Forall right (_, CoreType::Forall(var, ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left, right: substituted_ty, })); Ok(()) } // Forall left (CoreType::Forall(var, ty), _) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted_ty = self.substitute_type(var, &CoreType::ETVar(fresh_evar), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: substituted_ty, right, })); Ok(()) } // Existential variable instantiation (CoreType::ETVar(a), _) if !self.occurs_check(a, &right) => { self.instantiate_left(a, &right) } (_, CoreType::ETVar(a)) if !self.occurs_check(a, &left) => { self.instantiate_right(&left, a) } _ => Err(TypeError::SubtypingError { left, right, span: None, }), } } fn solve_inference(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Inf {} ⊢ {}", self.term_to_string(&term), ty)); match term { CoreTerm::Var(name) => { // Check pattern variable context first if let Some(var_ty) = self.var_context.get(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.worklist.find_var(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.data_constructors.get(&name).cloned() { // Check data constructors for constructor variables self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } } CoreTerm::LitInt(_) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::Con("Int".to_string()), right: ty, })); Ok(()) } CoreTerm::Lambda { param, param_ty, body, } => { let result_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &result_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(result_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: arrow_ty, right: ty, })); self.worklist.push(WorklistEntry::Var(param, param_ty)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: result_ty, })); Ok(()) } CoreTerm::App { func, arg } => { let func_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &func_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: func_ty.clone(), arg: *arg, result_ty: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *func, ty: func_ty, })); Ok(()) } CoreTerm::TypeLambda { param, body } => { let body_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &body_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let forall_ty = CoreType::Forall(param.clone(), Box::new(body_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: forall_ty, right: ty, })); self.worklist .push(WorklistEntry::TVar(param, TyVarKind::Universal)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: body_ty, })); Ok(()) } CoreTerm::Constructor { name, args: _ } => { if let Some(constructor_ty) = self.data_constructors.get(&name) { // Instantiate the constructor type with fresh existential variables let instantiated_ty = self.instantiate_constructor_type(constructor_ty.clone()); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: instantiated_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } CoreTerm::BinOp { op, left, right } => { let (left_ty, right_ty, result_ty) = self.infer_binop_types(&op); // Add any existential variables to the worklist self.add_etvars_to_worklist(&left_ty); self.add_etvars_to_worklist(&right_ty); self.add_etvars_to_worklist(&result_ty); // Check that the operands have the expected types self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *left, ty: left_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *right, ty: right_ty, })); // Check that the result type matches the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_ty, right: ty, })); Ok(()) } CoreTerm::If { cond, then_branch, else_branch, } => { // The condition must be Bool self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *cond, ty: CoreType::Con("Bool".to_string()), })); // Both branches must have the same type as the expected result self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *then_branch, ty: ty.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *else_branch, ty, })); Ok(()) } CoreTerm::Case { scrutinee, arms } => { // Create a fresh type variable for the scrutinee let scrutinee_ty = CoreType::ETVar(self.worklist.fresh_evar()); self.add_etvars_to_worklist(&scrutinee_ty); // Check that the scrutinee has the inferred type self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *scrutinee, ty: scrutinee_ty.clone(), })); // Process each pattern arm for arm in arms { // Check pattern constraints and get pattern variable bindings let pattern_bindings = self.check_pattern(&arm.pattern, &scrutinee_ty)?; // Add pattern variable bindings to worklist as regular variables for (var_name, var_type) in pattern_bindings { self.worklist.push(WorklistEntry::Var(var_name, var_type)); } // Check the body with pattern variables in the worklist self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arm.body.clone(), ty: ty.clone(), })); } Ok(()) } } } fn solve_checking(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Chk {} ⇐ {}", self.term_to_string(&term), ty)); match (&term, &ty) { ( CoreTerm::Lambda { param, param_ty, body, }, CoreType::Arrow(expected_param, result_ty), ) => { // Check that parameter types match self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: param_ty.clone(), right: *expected_param.clone(), })); self.worklist .push(WorklistEntry::Var(param.clone(), param_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *body.clone(), ty: *result_ty.clone(), })); Ok(()) } (_, CoreType::Forall(var, body_ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), body_ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term, ty: substituted_ty, })); Ok(()) } _ => { // Fallback: infer type and check subtyping let inferred_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &inferred_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: inferred_ty.clone(), right: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term, ty: inferred_ty, })); Ok(()) } } } fn solve_inf_app( &mut self, func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, ) -> TypeResult<()> { match func_ty { CoreType::Arrow(param_ty, ret_ty) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: *param_ty, })); Ok(()) } CoreType::Forall(var, body) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(&var, &CoreType::ETVar(fresh_evar), &body); self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: substituted, arg, result_ty, })); Ok(()) } CoreType::ETVar(a) => { let param_ty_name = self.worklist.fresh_evar(); let ret_ty_name = self.worklist.fresh_evar(); let param_ty = CoreType::ETVar(param_ty_name.clone()); let ret_ty = CoreType::ETVar(ret_ty_name.clone()); // Add the fresh existential variables to the worklist self.worklist .push(WorklistEntry::TVar(param_ty_name, TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(ret_ty_name, TyVarKind::Existential)); let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(ret_ty.clone())); self.worklist.solve_evar(&a, arrow_ty)?; self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: param_ty, })); Ok(()) } _ => Err(TypeError::NotAFunction { ty: func_ty, span: None, }), } } fn instantiate_left(&mut self, var: &str, ty: &CoreType) -> TypeResult<()> { match ty { CoreType::ETVar(b) if self.worklist.before(var, b) => { self.worklist .solve_evar(b, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::Forall(b, t) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted = self.substitute_type(b, &CoreType::Var(fresh_var), t); self.instantiate_left(var, &substituted) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn instantiate_right(&mut self, ty: &CoreType, var: &str) -> TypeResult<()> { match ty { CoreType::ETVar(a) if self.worklist.before(var, a) => { self.worklist .solve_evar(a, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::Forall(a, t) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(a, &CoreType::ETVar(fresh_evar), t); self.instantiate_right(&substituted, var) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn occurs_check(&self, var: &str, ty: &CoreType) -> bool { match ty { CoreType::ETVar(name) | CoreType::Var(name) => name == var, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.occurs_check(var, t1) || self.occurs_check(var, t2) } CoreType::Forall(_, t) => self.occurs_check(var, t), CoreType::Product(types) => types.iter().any(|t| self.occurs_check(var, t)), _ => false, } } fn is_monotype(&self, ty: &CoreType) -> bool { match ty { CoreType::Con(_) | CoreType::Var(_) | CoreType::ETVar(_) => true, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.is_monotype(t1) && self.is_monotype(t2) } CoreType::Product(types) => types.iter().all(|t| self.is_monotype(t)), CoreType::Forall(_, _) => false, } } fn substitute_type(&self, var: &str, replacement: &CoreType, ty: &CoreType) -> CoreType { match ty { CoreType::Var(name) if name == var => replacement.clone(), CoreType::Arrow(t1, t2) => CoreType::Arrow( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Forall(bound_var, body) if bound_var != var => CoreType::Forall( bound_var.clone(), Box::new(self.substitute_type(var, replacement, body)), ), CoreType::App(t1, t2) => CoreType::App( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.substitute_type(var, replacement, t)) .collect(), ), _ => ty.clone(), } } fn term_to_string(&self, term: &CoreTerm) -> String { match term { CoreTerm::Var(name) => name.clone(), CoreTerm::LitInt(n) => n.to_string(), _ => format!("{:?}", term), // XXX: Simplified for now } } pub fn get_trace(&self) -> &[String] { &self.trace } fn infer_binop_types(&mut self, op: &CoreBinOp) -> (CoreType, CoreType, CoreType) { match op { // Arithmetic operations: Int -> Int -> Int CoreBinOp::Add | CoreBinOp::Sub | CoreBinOp::Mul | CoreBinOp::Div => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), ), // Comparison operations: Int -> Int -> Bool CoreBinOp::Lt | CoreBinOp::Le => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Bool".to_string()), ), } } fn add_etvars_to_worklist(&mut self, ty: &CoreType) { match ty { CoreType::ETVar(var_name) => { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.add_etvars_to_worklist(t1); self.add_etvars_to_worklist(t2); } CoreType::Forall(_, t) => { self.add_etvars_to_worklist(t); } CoreType::Product(types) => { for t in types { self.add_etvars_to_worklist(t); } } CoreType::Var(_) | CoreType::Con(_) => { // No existential variables to add } } } /// Check a pattern against a type and return variable bindings /// This implements pattern type checking with unification fn check_pattern( &mut self, pattern: &CorePattern, expected_ty: &CoreType, ) -> TypeResult<HashMap<String, CoreType>> { let mut bindings = HashMap::new(); match pattern { CorePattern::Wildcard => { // Wildcard matches anything, no bindings Ok(bindings) } CorePattern::Var(var_name) => { // Variable patterns bind the scrutinee type bindings.insert(var_name.clone(), expected_ty.clone()); Ok(bindings) } CorePattern::Constructor { name, args } => { // Look up constructor type from data constructor environment if let Some(constructor_ty) = self.data_constructors.get(name).cloned() { // Constructor type should be of the form: T1 -> T2 -> ... -> DataType // We need to unify the result type with expected_ty and // check argument patterns against parameter types let (param_types, result_type) = self.extract_constructor_signature(&constructor_ty)?; // The result type should unify with the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_type, right: expected_ty.clone(), })); // Check that we have the right number of pattern arguments if args.len() != param_types.len() { return Err(TypeError::ArityMismatch { expected: param_types.len(), actual: args.len(), span: None, }); } // Recursively check argument patterns for (arg_pattern, param_ty) in args.iter().zip(param_types.iter()) { let arg_bindings = self.check_pattern(arg_pattern, param_ty)?; // Merge bindings (should check for conflicts in a real implementation) for (var, ty) in arg_bindings { bindings.insert(var, ty); } } Ok(bindings) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } } } /// Extract parameter types and result type from a constructor type /// signature e.g., Int -> String -> Bool -> MyData => ([Int, String, /// Bool], MyData) fn extract_constructor_signature( &mut self, constructor_ty: &CoreType, ) -> TypeResult<(Vec<CoreType>, CoreType)> { let mut param_types = Vec::new(); let mut current_ty = constructor_ty.clone(); let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type current_ty = self.apply_type_substitutions(¤t_ty, &substitutions); // Extract parameter types from arrows while let CoreType::Arrow(param_ty, result_ty) = current_ty { param_types.push(*param_ty.clone()); current_ty = *result_ty; } // The final type is the result type Ok((param_types, current_ty)) } fn instantiate_constructor_type(&mut self, constructor_ty: CoreType) -> CoreType { let mut current_ty = constructor_ty; let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type self.apply_type_substitutions(¤t_ty, &substitutions) } fn apply_type_substitutions( &self, ty: &CoreType, substitutions: &HashMap<String, CoreType>, ) -> CoreType { match ty { CoreType::Var(name) => substitutions .get(name) .cloned() .unwrap_or_else(|| ty.clone()), CoreType::Con(name) => CoreType::Con(name.clone()), CoreType::ETVar(name) => CoreType::ETVar(name.clone()), CoreType::Arrow(left, right) => CoreType::Arrow( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::App(left, right) => CoreType::App( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::Forall(var, body) => { // Don't substitute under forall bindings - this is a simplification CoreType::Forall( var.clone(), Box::new(self.apply_type_substitutions(body, substitutions)), ) } CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.apply_type_substitutions(t, substitutions)) .collect(), ), } } } #[derive(Debug, Clone, PartialEq)] pub enum TyVarKind { /// Universal type variable: α Universal, /// Existential type variable: ^α Existential, /// Solved existential: ^α = τ Solved(CoreType), /// Marker: ►α (for scoping) Marker, } }
Type variables in the worklist can have different statuses that reflect their role in the type checking process. Universal type variables represent ordinary type variables that arise from explicit quantifiers in the source code, such as the \( \alpha \) in \( \forall\alpha. \ldots \). These variables have fixed scope and represent abstract types that can be instantiated with concrete types during polymorphic function application. Existential type variables, denoted as \( \hat{\alpha} \), represent unknown types that need to be inferred through constraint solving. The algorithm generates these variables when it encounters expressions whose types are not immediately apparent and must be determined through unification and constraint propagation.
Solved existential variables represent the successful resolution of inference problems, taking the form \( \hat{\alpha} = \tau \) where the unknown type \( \hat{\alpha} \) has been determined to be the concrete type \( \tau \). Marker variables, denoted as \( \triangleright\alpha \), serve as scope markers that enable garbage collection of type variables when their scope is exited. This stratification enables precise control over variable scoping and solution propagation, ensuring that type variables are managed correctly throughout the inference process.
Judgment Types
#![allow(unused)] fn main() { use std::collections::HashMap; use crate::core::{CoreBinOp, CorePattern, CoreTerm, CoreType}; use crate::errors::{TypeError, TypeResult}; /// DK Worklist Algorithm for System-F-ω /// Based on "A Mechanical Formalization of Higher-Ranked Polymorphic Type /// Inference" pub type TyVar = String; pub type TmVar = String; #[derive(Debug, Clone, PartialEq)] pub enum WorklistEntry { /// Type variable binding: α TVar(TyVar, TyVarKind), /// Term variable binding: x : T Var(TmVar, CoreType), /// Judgment: Sub A B | Inf e ⊢ A | Chk e ⇐ A Judgment(Judgment), } #[derive(Debug, Clone, PartialEq)] pub enum TyVarKind { /// Universal type variable: α Universal, /// Existential type variable: ^α Existential, /// Solved existential: ^α = τ Solved(CoreType), /// Marker: ►α (for scoping) Marker, } #[derive(Debug, Clone)] pub struct Worklist { entries: Vec<WorklistEntry>, next_var: usize, } impl Default for Worklist { fn default() -> Self { Self::new() } } impl Worklist { pub fn new() -> Self { Worklist { entries: Vec::new(), next_var: 0, } } pub fn fresh_var(&mut self) -> TyVar { let var = format!("α{}", self.next_var); self.next_var += 1; var } pub fn fresh_evar(&mut self) -> TyVar { let var = format!("^α{}", self.next_var); self.next_var += 1; var } pub fn push(&mut self, entry: WorklistEntry) { self.entries.push(entry); } pub fn pop(&mut self) -> Option<WorklistEntry> { self.entries.pop() } pub fn find_var(&self, name: &str) -> Option<&CoreType> { for entry in self.entries.iter().rev() { if let WorklistEntry::Var(var_name, ty) = entry { if var_name == name { return Some(ty); } } } None } pub fn solve_evar(&mut self, name: &str, ty: CoreType) -> TypeResult<()> { for entry in self.entries.iter_mut() { if let WorklistEntry::TVar(var_name, kind) = entry { if var_name == name { match kind { TyVarKind::Existential => { *kind = TyVarKind::Solved(ty); return Ok(()); } TyVarKind::Solved(_) => { // Variable already solved, that's OK return Ok(()); } _ => { // Skip universal variables, markers, etc. continue; } } } } } Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } pub fn before(&self, a: &str, b: &str) -> bool { let mut pos_a = None; let mut pos_b = None; for (i, entry) in self.entries.iter().enumerate() { if let WorklistEntry::TVar(name, _) = entry { if name == a { pos_a = Some(i); } if name == b { pos_b = Some(i); } } } match (pos_a, pos_b) { (Some(pa), Some(pb)) => pa < pb, _ => false, } } } pub struct DKInference { worklist: Worklist, trace: Vec<String>, data_constructors: HashMap<String, CoreType>, /// Variable typing context for pattern-bound variables var_context: HashMap<String, CoreType>, } impl DKInference { pub fn with_context( data_constructors: HashMap<String, CoreType>, var_context: HashMap<String, CoreType>, ) -> Self { DKInference { worklist: Worklist::new(), trace: Vec::new(), data_constructors, var_context, } } pub fn check_type(&mut self, term: &CoreTerm, expected_ty: &CoreType) -> TypeResult<()> { self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: term.clone(), ty: expected_ty.clone(), })); self.solve() } fn solve(&mut self) -> TypeResult<()> { while let Some(entry) = self.worklist.pop() { match entry { WorklistEntry::TVar(_, _) => { // Skip variable bindings during processing continue; } WorklistEntry::Var(_, _) => { // Skip term variable bindings during processing continue; } WorklistEntry::Judgment(judgment) => { self.solve_judgment(judgment)?; } } } Ok(()) } fn solve_judgment(&mut self, judgment: Judgment) -> TypeResult<()> { match judgment { Judgment::Sub { left, right } => self.solve_subtype(left, right), Judgment::Inf { term, ty } => self.solve_inference(term, ty), Judgment::Chk { term, ty } => self.solve_checking(term, ty), Judgment::InfApp { func_ty, arg, result_ty, } => self.solve_inf_app(func_ty, arg, result_ty), } } fn solve_subtype(&mut self, left: CoreType, right: CoreType) -> TypeResult<()> { self.trace.push(format!("Sub {} <: {}", left, right)); if left == right { return Ok(()); } match (&left, &right) { // Reflexivity (CoreType::Con(a), CoreType::Con(b)) if a == b => Ok(()), (CoreType::Var(a), CoreType::Var(b)) if a == b => Ok(()), (CoreType::ETVar(a), CoreType::ETVar(b)) if a == b => Ok(()), // Function subtyping (contravariant in argument, covariant in result) (CoreType::Arrow(a1, a2), CoreType::Arrow(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *b1.clone(), right: *a1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Application subtyping (covariant in both components) (CoreType::App(a1, a2), CoreType::App(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a1.clone(), right: *b1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Forall right (_, CoreType::Forall(var, ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left, right: substituted_ty, })); Ok(()) } // Forall left (CoreType::Forall(var, ty), _) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted_ty = self.substitute_type(var, &CoreType::ETVar(fresh_evar), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: substituted_ty, right, })); Ok(()) } // Existential variable instantiation (CoreType::ETVar(a), _) if !self.occurs_check(a, &right) => { self.instantiate_left(a, &right) } (_, CoreType::ETVar(a)) if !self.occurs_check(a, &left) => { self.instantiate_right(&left, a) } _ => Err(TypeError::SubtypingError { left, right, span: None, }), } } fn solve_inference(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Inf {} ⊢ {}", self.term_to_string(&term), ty)); match term { CoreTerm::Var(name) => { // Check pattern variable context first if let Some(var_ty) = self.var_context.get(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.worklist.find_var(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.data_constructors.get(&name).cloned() { // Check data constructors for constructor variables self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } } CoreTerm::LitInt(_) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::Con("Int".to_string()), right: ty, })); Ok(()) } CoreTerm::Lambda { param, param_ty, body, } => { let result_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &result_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(result_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: arrow_ty, right: ty, })); self.worklist.push(WorklistEntry::Var(param, param_ty)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: result_ty, })); Ok(()) } CoreTerm::App { func, arg } => { let func_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &func_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: func_ty.clone(), arg: *arg, result_ty: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *func, ty: func_ty, })); Ok(()) } CoreTerm::TypeLambda { param, body } => { let body_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &body_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let forall_ty = CoreType::Forall(param.clone(), Box::new(body_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: forall_ty, right: ty, })); self.worklist .push(WorklistEntry::TVar(param, TyVarKind::Universal)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: body_ty, })); Ok(()) } CoreTerm::Constructor { name, args: _ } => { if let Some(constructor_ty) = self.data_constructors.get(&name) { // Instantiate the constructor type with fresh existential variables let instantiated_ty = self.instantiate_constructor_type(constructor_ty.clone()); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: instantiated_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } CoreTerm::BinOp { op, left, right } => { let (left_ty, right_ty, result_ty) = self.infer_binop_types(&op); // Add any existential variables to the worklist self.add_etvars_to_worklist(&left_ty); self.add_etvars_to_worklist(&right_ty); self.add_etvars_to_worklist(&result_ty); // Check that the operands have the expected types self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *left, ty: left_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *right, ty: right_ty, })); // Check that the result type matches the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_ty, right: ty, })); Ok(()) } CoreTerm::If { cond, then_branch, else_branch, } => { // The condition must be Bool self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *cond, ty: CoreType::Con("Bool".to_string()), })); // Both branches must have the same type as the expected result self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *then_branch, ty: ty.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *else_branch, ty, })); Ok(()) } CoreTerm::Case { scrutinee, arms } => { // Create a fresh type variable for the scrutinee let scrutinee_ty = CoreType::ETVar(self.worklist.fresh_evar()); self.add_etvars_to_worklist(&scrutinee_ty); // Check that the scrutinee has the inferred type self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *scrutinee, ty: scrutinee_ty.clone(), })); // Process each pattern arm for arm in arms { // Check pattern constraints and get pattern variable bindings let pattern_bindings = self.check_pattern(&arm.pattern, &scrutinee_ty)?; // Add pattern variable bindings to worklist as regular variables for (var_name, var_type) in pattern_bindings { self.worklist.push(WorklistEntry::Var(var_name, var_type)); } // Check the body with pattern variables in the worklist self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arm.body.clone(), ty: ty.clone(), })); } Ok(()) } } } fn solve_checking(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Chk {} ⇐ {}", self.term_to_string(&term), ty)); match (&term, &ty) { ( CoreTerm::Lambda { param, param_ty, body, }, CoreType::Arrow(expected_param, result_ty), ) => { // Check that parameter types match self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: param_ty.clone(), right: *expected_param.clone(), })); self.worklist .push(WorklistEntry::Var(param.clone(), param_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *body.clone(), ty: *result_ty.clone(), })); Ok(()) } (_, CoreType::Forall(var, body_ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), body_ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term, ty: substituted_ty, })); Ok(()) } _ => { // Fallback: infer type and check subtyping let inferred_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &inferred_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: inferred_ty.clone(), right: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term, ty: inferred_ty, })); Ok(()) } } } fn solve_inf_app( &mut self, func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, ) -> TypeResult<()> { match func_ty { CoreType::Arrow(param_ty, ret_ty) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: *param_ty, })); Ok(()) } CoreType::Forall(var, body) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(&var, &CoreType::ETVar(fresh_evar), &body); self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: substituted, arg, result_ty, })); Ok(()) } CoreType::ETVar(a) => { let param_ty_name = self.worklist.fresh_evar(); let ret_ty_name = self.worklist.fresh_evar(); let param_ty = CoreType::ETVar(param_ty_name.clone()); let ret_ty = CoreType::ETVar(ret_ty_name.clone()); // Add the fresh existential variables to the worklist self.worklist .push(WorklistEntry::TVar(param_ty_name, TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(ret_ty_name, TyVarKind::Existential)); let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(ret_ty.clone())); self.worklist.solve_evar(&a, arrow_ty)?; self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: ret_ty, right: result_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arg, ty: param_ty, })); Ok(()) } _ => Err(TypeError::NotAFunction { ty: func_ty, span: None, }), } } fn instantiate_left(&mut self, var: &str, ty: &CoreType) -> TypeResult<()> { match ty { CoreType::ETVar(b) if self.worklist.before(var, b) => { self.worklist .solve_evar(b, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::Forall(b, t) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted = self.substitute_type(b, &CoreType::Var(fresh_var), t); self.instantiate_left(var, &substituted) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn instantiate_right(&mut self, ty: &CoreType, var: &str) -> TypeResult<()> { match ty { CoreType::ETVar(a) if self.worklist.before(var, a) => { self.worklist .solve_evar(a, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t2.clone(), right: CoreType::ETVar(a2), })); Ok(()) } CoreType::Forall(a, t) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted = self.substitute_type(a, &CoreType::ETVar(fresh_evar), t); self.instantiate_right(&substituted, var) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } fn occurs_check(&self, var: &str, ty: &CoreType) -> bool { match ty { CoreType::ETVar(name) | CoreType::Var(name) => name == var, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.occurs_check(var, t1) || self.occurs_check(var, t2) } CoreType::Forall(_, t) => self.occurs_check(var, t), CoreType::Product(types) => types.iter().any(|t| self.occurs_check(var, t)), _ => false, } } fn is_monotype(&self, ty: &CoreType) -> bool { match ty { CoreType::Con(_) | CoreType::Var(_) | CoreType::ETVar(_) => true, CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.is_monotype(t1) && self.is_monotype(t2) } CoreType::Product(types) => types.iter().all(|t| self.is_monotype(t)), CoreType::Forall(_, _) => false, } } fn substitute_type(&self, var: &str, replacement: &CoreType, ty: &CoreType) -> CoreType { match ty { CoreType::Var(name) if name == var => replacement.clone(), CoreType::Arrow(t1, t2) => CoreType::Arrow( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Forall(bound_var, body) if bound_var != var => CoreType::Forall( bound_var.clone(), Box::new(self.substitute_type(var, replacement, body)), ), CoreType::App(t1, t2) => CoreType::App( Box::new(self.substitute_type(var, replacement, t1)), Box::new(self.substitute_type(var, replacement, t2)), ), CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.substitute_type(var, replacement, t)) .collect(), ), _ => ty.clone(), } } fn term_to_string(&self, term: &CoreTerm) -> String { match term { CoreTerm::Var(name) => name.clone(), CoreTerm::LitInt(n) => n.to_string(), _ => format!("{:?}", term), // XXX: Simplified for now } } pub fn get_trace(&self) -> &[String] { &self.trace } fn infer_binop_types(&mut self, op: &CoreBinOp) -> (CoreType, CoreType, CoreType) { match op { // Arithmetic operations: Int -> Int -> Int CoreBinOp::Add | CoreBinOp::Sub | CoreBinOp::Mul | CoreBinOp::Div => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), ), // Comparison operations: Int -> Int -> Bool CoreBinOp::Lt | CoreBinOp::Le => ( CoreType::Con("Int".to_string()), CoreType::Con("Int".to_string()), CoreType::Con("Bool".to_string()), ), } } fn add_etvars_to_worklist(&mut self, ty: &CoreType) { match ty { CoreType::ETVar(var_name) => { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } CoreType::Arrow(t1, t2) | CoreType::App(t1, t2) => { self.add_etvars_to_worklist(t1); self.add_etvars_to_worklist(t2); } CoreType::Forall(_, t) => { self.add_etvars_to_worklist(t); } CoreType::Product(types) => { for t in types { self.add_etvars_to_worklist(t); } } CoreType::Var(_) | CoreType::Con(_) => { // No existential variables to add } } } /// Check a pattern against a type and return variable bindings /// This implements pattern type checking with unification fn check_pattern( &mut self, pattern: &CorePattern, expected_ty: &CoreType, ) -> TypeResult<HashMap<String, CoreType>> { let mut bindings = HashMap::new(); match pattern { CorePattern::Wildcard => { // Wildcard matches anything, no bindings Ok(bindings) } CorePattern::Var(var_name) => { // Variable patterns bind the scrutinee type bindings.insert(var_name.clone(), expected_ty.clone()); Ok(bindings) } CorePattern::Constructor { name, args } => { // Look up constructor type from data constructor environment if let Some(constructor_ty) = self.data_constructors.get(name).cloned() { // Constructor type should be of the form: T1 -> T2 -> ... -> DataType // We need to unify the result type with expected_ty and // check argument patterns against parameter types let (param_types, result_type) = self.extract_constructor_signature(&constructor_ty)?; // The result type should unify with the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_type, right: expected_ty.clone(), })); // Check that we have the right number of pattern arguments if args.len() != param_types.len() { return Err(TypeError::ArityMismatch { expected: param_types.len(), actual: args.len(), span: None, }); } // Recursively check argument patterns for (arg_pattern, param_ty) in args.iter().zip(param_types.iter()) { let arg_bindings = self.check_pattern(arg_pattern, param_ty)?; // Merge bindings (should check for conflicts in a real implementation) for (var, ty) in arg_bindings { bindings.insert(var, ty); } } Ok(bindings) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } } } /// Extract parameter types and result type from a constructor type /// signature e.g., Int -> String -> Bool -> MyData => ([Int, String, /// Bool], MyData) fn extract_constructor_signature( &mut self, constructor_ty: &CoreType, ) -> TypeResult<(Vec<CoreType>, CoreType)> { let mut param_types = Vec::new(); let mut current_ty = constructor_ty.clone(); let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type current_ty = self.apply_type_substitutions(¤t_ty, &substitutions); // Extract parameter types from arrows while let CoreType::Arrow(param_ty, result_ty) = current_ty { param_types.push(*param_ty.clone()); current_ty = *result_ty; } // The final type is the result type Ok((param_types, current_ty)) } fn instantiate_constructor_type(&mut self, constructor_ty: CoreType) -> CoreType { let mut current_ty = constructor_ty; let mut substitutions = HashMap::new(); // Instantiate forall quantifiers with fresh existential variables while let CoreType::Forall(var, body) = current_ty { let fresh_var_name = self.worklist.fresh_evar(); let fresh_evar = CoreType::ETVar(fresh_var_name.clone()); // Add the existential variable to the worklist self.worklist.push(WorklistEntry::TVar( fresh_var_name.clone(), TyVarKind::Existential, )); substitutions.insert(var.clone(), fresh_evar); current_ty = *body; } // Apply substitutions to the type self.apply_type_substitutions(¤t_ty, &substitutions) } fn apply_type_substitutions( &self, ty: &CoreType, substitutions: &HashMap<String, CoreType>, ) -> CoreType { match ty { CoreType::Var(name) => substitutions .get(name) .cloned() .unwrap_or_else(|| ty.clone()), CoreType::Con(name) => CoreType::Con(name.clone()), CoreType::ETVar(name) => CoreType::ETVar(name.clone()), CoreType::Arrow(left, right) => CoreType::Arrow( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::App(left, right) => CoreType::App( Box::new(self.apply_type_substitutions(left, substitutions)), Box::new(self.apply_type_substitutions(right, substitutions)), ), CoreType::Forall(var, body) => { // Don't substitute under forall bindings - this is a simplification CoreType::Forall( var.clone(), Box::new(self.apply_type_substitutions(body, substitutions)), ) } CoreType::Product(types) => CoreType::Product( types .iter() .map(|t| self.apply_type_substitutions(t, substitutions)) .collect(), ), } } } #[derive(Debug, Clone, PartialEq)] pub enum Judgment { /// Subtyping: A <: B Sub { left: CoreType, right: CoreType }, /// Type inference: e ⊢ A Inf { term: CoreTerm, ty: CoreType }, /// Type checking: e ⇐ A Chk { term: CoreTerm, ty: CoreType }, /// Application inference helper: A • e ⊢ C InfApp { func_ty: CoreType, arg: CoreTerm, result_ty: CoreType, }, } }
Judgments represent the core type checking tasks that drive the DK algorithm forward. Subtyping judgments, written as \( A \leq B \), verify that type \( A \) is a subtype of type \( B \), which is essential for handling the contravariant and covariant relationships that arise in function types and polymorphic instantiation. Inference judgments, denoted \( e \Rightarrow A \), synthesize a type \( A \) for a given expression \( e \), allowing the algorithm to determine types from expressions when no expected type is available. Checking judgments, written as \( e \Leftarrow A \), verify that a given expression \( e \) conforms to an expected type \( A \), which is often more efficient than synthesis when the target type is known.
Instantiation judgments handle the complex process of polymorphic type instantiation, managing the creation and resolution of existential variables that arise when applying polymorphic functions to arguments. Application judgments provide specialized handling for function application inference, dealing with the intricate constraint generation that occurs when the function type may not be immediately known. The algorithm processes these judgments by pattern matching on their structure and generating new worklist entries as needed, creating a systematic approach to constraint solving that ensures all type relationships are properly established.
Bidirectional Type Checking
The DK algorithm employs bidirectional type checking, splitting inference into two complementary modes that work together to handle System F-ω’s complexity.
Synthesis Mode (⇒)
#![allow(unused)] fn main() { fn solve_inference(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Inf {} ⊢ {}", self.term_to_string(&term), ty)); match term { CoreTerm::Var(name) => { // Check pattern variable context first if let Some(var_ty) = self.var_context.get(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.worklist.find_var(&name).cloned() { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else if let Some(var_ty) = self.data_constructors.get(&name).cloned() { // Check data constructors for constructor variables self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: var_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundVariable { name: name.to_string(), span: None, }) } } CoreTerm::LitInt(_) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::Con("Int".to_string()), right: ty, })); Ok(()) } CoreTerm::Lambda { param, param_ty, body, } => { let result_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &result_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let arrow_ty = CoreType::Arrow(Box::new(param_ty.clone()), Box::new(result_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: arrow_ty, right: ty, })); self.worklist.push(WorklistEntry::Var(param, param_ty)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: result_ty, })); Ok(()) } CoreTerm::App { func, arg } => { let func_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &func_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist .push(WorklistEntry::Judgment(Judgment::InfApp { func_ty: func_ty.clone(), arg: *arg, result_ty: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *func, ty: func_ty, })); Ok(()) } CoreTerm::TypeLambda { param, body } => { let body_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &body_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } let forall_ty = CoreType::Forall(param.clone(), Box::new(body_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: forall_ty, right: ty, })); self.worklist .push(WorklistEntry::TVar(param, TyVarKind::Universal)); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term: *body, ty: body_ty, })); Ok(()) } CoreTerm::Constructor { name, args: _ } => { if let Some(constructor_ty) = self.data_constructors.get(&name) { // Instantiate the constructor type with fresh existential variables let instantiated_ty = self.instantiate_constructor_type(constructor_ty.clone()); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: instantiated_ty, right: ty, })); Ok(()) } else { Err(TypeError::UnboundDataConstructor { name: name.clone(), span: None, }) } } CoreTerm::BinOp { op, left, right } => { let (left_ty, right_ty, result_ty) = self.infer_binop_types(&op); // Add any existential variables to the worklist self.add_etvars_to_worklist(&left_ty); self.add_etvars_to_worklist(&right_ty); self.add_etvars_to_worklist(&result_ty); // Check that the operands have the expected types self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *left, ty: left_ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *right, ty: right_ty, })); // Check that the result type matches the expected type self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: result_ty, right: ty, })); Ok(()) } CoreTerm::If { cond, then_branch, else_branch, } => { // The condition must be Bool self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *cond, ty: CoreType::Con("Bool".to_string()), })); // Both branches must have the same type as the expected result self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *then_branch, ty: ty.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *else_branch, ty, })); Ok(()) } CoreTerm::Case { scrutinee, arms } => { // Create a fresh type variable for the scrutinee let scrutinee_ty = CoreType::ETVar(self.worklist.fresh_evar()); self.add_etvars_to_worklist(&scrutinee_ty); // Check that the scrutinee has the inferred type self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *scrutinee, ty: scrutinee_ty.clone(), })); // Process each pattern arm for arm in arms { // Check pattern constraints and get pattern variable bindings let pattern_bindings = self.check_pattern(&arm.pattern, &scrutinee_ty)?; // Add pattern variable bindings to worklist as regular variables for (var_name, var_type) in pattern_bindings { self.worklist.push(WorklistEntry::Var(var_name, var_type)); } // Check the body with pattern variables in the worklist self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: arm.body.clone(), ty: ty.clone(), })); } Ok(()) } } } }
Synthesis mode analyzes expressions to determine their types, working from the structure of expressions to produce type information. When encountering variables, the algorithm looks up their types in the current typing context, instantiating any polymorphic schemes as needed to produce concrete types for the current usage. Function applications require the algorithm to infer both the function and argument types, then unify them to ensure the application is well-typed. Type applications instantiate polymorphic types with concrete type arguments, requiring careful management of type variable substitution and scope.
Type annotations provide explicit guidance to the inference process, allowing programmers to specify expected types that the algorithm can use to constrain its search space. Synthesis mode produces not only a type but also any constraints that must hold for the typing to be valid, enabling the algorithm to handle complex interdependencies between different parts of the expression being analyzed.
Checking Mode (⇐)
#![allow(unused)] fn main() { fn solve_checking(&mut self, term: CoreTerm, ty: CoreType) -> TypeResult<()> { self.trace .push(format!("Chk {} ⇐ {}", self.term_to_string(&term), ty)); match (&term, &ty) { ( CoreTerm::Lambda { param, param_ty, body, }, CoreType::Arrow(expected_param, result_ty), ) => { // Check that parameter types match self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: param_ty.clone(), right: *expected_param.clone(), })); self.worklist .push(WorklistEntry::Var(param.clone(), param_ty.clone())); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term: *body.clone(), ty: *result_ty.clone(), })); Ok(()) } (_, CoreType::Forall(var, body_ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), body_ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Chk { term, ty: substituted_ty, })); Ok(()) } _ => { // Fallback: infer type and check subtyping let inferred_ty = CoreType::ETVar(self.worklist.fresh_evar()); if let CoreType::ETVar(var_name) = &inferred_ty { self.worklist.push(WorklistEntry::TVar( var_name.clone(), TyVarKind::Existential, )); } self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: inferred_ty.clone(), right: ty, })); self.worklist.push(WorklistEntry::Judgment(Judgment::Inf { term, ty: inferred_ty, })); Ok(()) } } } }
Checking mode verifies that expressions conform to expected types, working backwards from known type information to validate expression structure. For lambda expressions, the algorithm can immediately decompose the expected function type to extract parameter and return types, then check the lambda parameter against the expected parameter type and recursively check the body against the expected return type. When checking against polymorphic types, the algorithm introduces fresh type variables for the quantified variables and checks the expression against the instantiated type.
When direct checking strategies are not applicable, the algorithm falls back to a synthesis-plus-subtyping approach, where it first synthesizes a type for the expression and then verifies that this synthesized type is a subtype of the expected type. Checking mode is often more efficient than synthesis because it can make stronger assumptions about the expected type structure, allowing the algorithm to prune the search space and make more directed inferences.
Existential Type Variables
Existential variables represent the unknown types that make type inference possible. They act as placeholders that get solved through unification and constraint propagation.
Variable Generation
#![allow(unused)] fn main() { pub fn fresh_evar(&mut self) -> TyVar { let var = format!("^α{}", self.next_var); self.next_var += 1; var } }
Fresh existential variables are generated with unique names and added to the worklist. The algorithm ensures that each unknown type gets a distinct variable, preventing accidental unification.
Constraint Generation
When the algorithm encounters expressions with unknown types, it follows a systematic constraint generation process. The algorithm creates fresh existential variables to represent the unknown types, ensuring each unknown gets a unique placeholder that can be tracked throughout the solving process. These existential variables are then related to known types through constraint generation, creating equations and inequalities that capture the type relationships implied by the program structure.
The generated constraints are added to the worklist for systematic resolution, allowing the algorithm to defer complex solving decisions until sufficient information is available. As constraints get resolved and existential variables receive concrete solutions, these solutions are propagated throughout the constraint system, potentially enabling the resolution of additional constraints in a cascading effect that gradually determines all unknown types.
Solving Process
#![allow(unused)] fn main() { fn solve(&mut self) -> TypeResult<()> { while let Some(entry) = self.worklist.pop() { match entry { WorklistEntry::TVar(_, _) => { // Skip variable bindings during processing continue; } WorklistEntry::Var(_, _) => { // Skip term variable bindings during processing continue; } WorklistEntry::Judgment(judgment) => { self.solve_judgment(judgment)?; } } } Ok(()) } }
Constraint solving proceeds through a systematic pattern matching process that determines which constraint solving rule applies to each judgment in the worklist. The algorithm examines the structure of constraints and applies appropriate decomposition strategies to break complex constraints into simpler, more manageable pieces. For instance, a constraint involving function types might be decomposed into separate constraints for the argument and return types.
Substitution plays a crucial role as solved variables are applied throughout the constraint system, replacing existential variables with their determined types wherever they appear. The occurs check prevents the creation of infinite types during unification by ensuring that a type variable does not appear within its own solution, maintaining the soundness of the type system. The solving process is guaranteed to terminate because System F-ω has decidable type inference, meaning that every well-typed program will eventually reach a state where all constraints are resolved and all existential variables have concrete solutions.
Subtyping and Polymorphic Instantiation
System F-ω’s subtyping relation captures the idea that more polymorphic types are subtypes of less polymorphic ones. This enables flexible use of polymorphic functions.
Subtyping Rules
#![allow(unused)] fn main() { fn solve_subtype(&mut self, left: CoreType, right: CoreType) -> TypeResult<()> { self.trace.push(format!("Sub {} <: {}", left, right)); if left == right { return Ok(()); } match (&left, &right) { // Reflexivity (CoreType::Con(a), CoreType::Con(b)) if a == b => Ok(()), (CoreType::Var(a), CoreType::Var(b)) if a == b => Ok(()), (CoreType::ETVar(a), CoreType::ETVar(b)) if a == b => Ok(()), // Function subtyping (contravariant in argument, covariant in result) (CoreType::Arrow(a1, a2), CoreType::Arrow(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *b1.clone(), right: *a1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Application subtyping (covariant in both components) (CoreType::App(a1, a2), CoreType::App(b1, b2)) => { self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a1.clone(), right: *b1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *a2.clone(), right: *b2.clone(), })); Ok(()) } // Forall right (_, CoreType::Forall(var, ty)) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted_ty = self.substitute_type(var, &CoreType::Var(fresh_var), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left, right: substituted_ty, })); Ok(()) } // Forall left (CoreType::Forall(var, ty), _) => { let fresh_evar = self.worklist.fresh_evar(); self.worklist .push(WorklistEntry::TVar(fresh_evar.clone(), TyVarKind::Marker)); self.worklist.push(WorklistEntry::TVar( fresh_evar.clone(), TyVarKind::Existential, )); let substituted_ty = self.substitute_type(var, &CoreType::ETVar(fresh_evar), ty); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: substituted_ty, right, })); Ok(()) } // Existential variable instantiation (CoreType::ETVar(a), _) if !self.occurs_check(a, &right) => { self.instantiate_left(a, &right) } (_, CoreType::ETVar(a)) if !self.occurs_check(a, &left) => { self.instantiate_right(&left, a) } _ => Err(TypeError::SubtypingError { left, right, span: None, }), } } }
The subtyping algorithm handles several fundamental relationships that govern type compatibility in System F-ω. Reflexivity ensures that every type is considered a subtype of itself, providing the base case for subtyping derivations. Transitivity allows subtyping relationships to compose through intermediate types, so if \( A \leq B \) and \( B \leq C \), then \( A \leq C \) holds automatically.
Function types exhibit the classic contravariant-covariant pattern, where a function type \( A_1 \to B_1 \) is a subtype of \( A_2 \to B_2 \) if \( A_2 \leq A_1 \) (contravariant in arguments) and \( B_1 \leq B_2 \) (covariant in results). Universal quantification follows the principle that \( \forall\alpha. A \leq B \) holds if \( A \leq B \) when \( \alpha \) is instantiated with a fresh existential variable. Existential instantiation requires the algorithm to solve existential variables in ways that satisfy the subtyping constraints, often leading to the creation of additional constraints that must be resolved.
Polymorphic Instantiation
#![allow(unused)] fn main() { fn instantiate_left(&mut self, var: &str, ty: &CoreType) -> TypeResult<()> { match ty { CoreType::ETVar(b) if self.worklist.before(var, b) => { self.worklist .solve_evar(b, CoreType::ETVar(var.to_string()))?; Ok(()) } CoreType::Arrow(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let arrow_ty = CoreType::Arrow( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, arrow_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: *t1.clone(), right: CoreType::ETVar(a1), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::App(t1, t2) => { let a1 = self.worklist.fresh_evar(); let a2 = self.worklist.fresh_evar(); let app_ty = CoreType::App( Box::new(CoreType::ETVar(a1.clone())), Box::new(CoreType::ETVar(a2.clone())), ); self.worklist.solve_evar(var, app_ty)?; self.worklist .push(WorklistEntry::TVar(a1.clone(), TyVarKind::Existential)); self.worklist .push(WorklistEntry::TVar(a2.clone(), TyVarKind::Existential)); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a1), right: *t1.clone(), })); self.worklist.push(WorklistEntry::Judgment(Judgment::Sub { left: CoreType::ETVar(a2), right: *t2.clone(), })); Ok(()) } CoreType::Forall(b, t) => { let fresh_var = self.worklist.fresh_var(); self.worklist .push(WorklistEntry::TVar(fresh_var.clone(), TyVarKind::Universal)); let substituted = self.substitute_type(b, &CoreType::Var(fresh_var), t); self.instantiate_left(var, &substituted) } _ if self.is_monotype(ty) => { self.worklist.solve_evar(var, ty.clone())?; Ok(()) } _ => Err(TypeError::InstantiationError { var: var.to_string(), ty: ty.clone(), span: None, }), } } }
Instantiation handles the complex process of applying polymorphic functions by systematically managing the relationship between universal and existential quantification. The algorithm begins by identifying quantified variables in polymorphic types, analyzing the structure of \( \forall \)-types to determine which type variables need instantiation. For each quantified variable, the algorithm generates fresh existential variables that will serve as placeholders for the concrete types to be determined through constraint solving.
The substitution phase replaces quantified variables with their corresponding existential variables throughout the type, effectively converting a polymorphic type scheme into a concrete type with unknown components. Additional constraints are added to ensure proper instantiation, capturing any relationships that must hold between the instantiated types and the context in which the polymorphic function is used. This systematic process enables the same polymorphic function to be used with different types in different contexts while maintaining type safety and ensuring that all instantiations are consistent with the function’s type signature.
Error Handling and Diagnostics
The DK algorithm provides precise error reporting by tracking the source of constraints and the reasoning that led to type checking failures.
#![allow(unused)] fn main() { use std::ops::Range; use ariadne::{Color, Label, Report, ReportKind}; use thiserror::Error; use crate::core::CoreType; pub type Span = Range<usize>; #[derive(Error, Debug, Clone)] pub enum ParseError { #[error("Unexpected token '{token}' at position {span:?}")] UnexpectedToken { token: String, span: Span }, #[error("Expected {expected} but found '{found}' at position {span:?}")] Expected { expected: String, found: String, span: Span, }, #[error("Unexpected end of file, expected {expected}")] UnexpectedEof { expected: String }, } #[derive(Error, Debug, Clone)] pub enum CompilerError { #[error("Parse error")] Parse(#[from] ParseError), #[error("Type error")] Type(#[from] TypeError), } pub type ParseResult<T> = Result<T, ParseError>; pub type TypeResult<T> = Result<T, TypeError>; pub type CompilerResult<T> = Result<T, CompilerError>; impl ParseError { pub fn report<'a>( &self, source: &str, filename: &'a str, ) -> Report<'a, (&'a str, Range<usize>)> { match self { ParseError::UnexpectedToken { token, span } => { Report::build(ReportKind::Error, filename, span.start) .with_message(format!("Unexpected token '{}'", token)) .with_label( Label::new((filename, span.clone())) .with_message("unexpected token here") .with_color(Color::Red), ) .finish() } ParseError::Expected { expected, found, span, } => Report::build(ReportKind::Error, filename, span.start) .with_message(format!("Expected {}, found '{}'", expected, found)) .with_label( Label::new((filename, span.clone())) .with_message(format!("expected {}", expected)) .with_color(Color::Red), ) .finish(), ParseError::UnexpectedEof { expected } => { Report::build(ReportKind::Error, filename, source.len()) .with_message(format!("Unexpected end of file, expected {}", expected)) .finish() } } } } impl TypeError { pub fn report<'a>( &self, source: &str, filename: &'a str, ) -> Report<'a, (&'a str, Range<usize>)> { match self { TypeError::UnboundVariable { name, span } => { let span = span.clone().unwrap_or(0..source.len()); Report::build(ReportKind::Error, filename, span.start) .with_message(format!("Variable '{}' not found in scope", name)) .with_label( Label::new((filename, span)) .with_message("undefined variable") .with_color(Color::Red), ) .finish() } // Add more specific error reporting as needed _ => Report::build(ReportKind::Error, filename, 0) .with_message(self.to_string()) .finish(), } } } #[derive(Error, Debug, Clone)] pub enum TypeError { #[error("Variable '{name}' not found in scope")] UnboundVariable { name: String, span: Option<Span> }, #[error("Data constructor '{name}' not found")] UnboundDataConstructor { name: String, span: Option<Span> }, #[error("Type '{ty}' is not a function type")] NotAFunction { ty: CoreType, span: Option<Span> }, #[error("Arity mismatch: expected {expected} arguments, got {actual}")] ArityMismatch { expected: usize, actual: usize, span: Option<Span>, }, #[error("Function '{name}' has definition but no type signature")] MissingTypeSignature { name: String, span: Option<Span> }, #[error("Subtyping failure: '{left}' is not a subtype of '{right}'")] SubtypingError { left: CoreType, right: CoreType, span: Option<Span>, }, #[error("Instantiation failure: cannot instantiate '{var}' with '{ty}'")] InstantiationError { var: String, ty: CoreType, span: Option<Span>, }, } }
The error system encompasses several categories of failures that can occur during type checking. Unification failures arise when the algorithm attempts to make two types equal but discovers they are fundamentally incompatible, such as trying to unify \( \text{Int} \) with \( \text{Bool} \to \text{String} \). Occurs check violations prevent the creation of infinite types by detecting when a type variable would appear within its own solution, such as attempting to solve \( \hat{\alpha} = \hat{\alpha} \to \text{Int} \).
Scope violations occur when type variables escape their intended scope, typically when an existential variable that should be local to a particular constraint solving context appears in the final type. Kind mismatches arise when type constructors are applied incorrectly, such as applying a type constructor that expects a higher-kinded argument to a concrete type. Each error includes location information and a description of the type checking rule that failed, enabling precise diagnostics that help programmers understand and fix type errors in their code.
When the algorithm succeeds, it finds the most general type for each expression. This means users get the maximum possible polymorphism without losing type safety.
Worklist Optimizations
There are a couple of optimizations that can also be added to make this process more efficient.
#![allow(unused)] fn main() { fn solve_judgment(&mut self, judgment: Judgment) -> TypeResult<()> { match judgment { Judgment::Sub { left, right } => self.solve_subtype(left, right), Judgment::Inf { term, ty } => self.solve_inference(term, ty), Judgment::Chk { term, ty } => self.solve_checking(term, ty), Judgment::InfApp { func_ty, arg, result_ty, } => self.solve_inf_app(func_ty, arg, result_ty), } } }
Smart scheduling of worklist entries improves performance through strategic constraint ordering. The algorithm prioritizes simple constraints that can be solved immediately, such as reflexive subtyping relationships or direct unification of concrete types, allowing these trivial cases to be resolved quickly and potentially simplify other constraints. Complex constraints that require extensive reasoning or depend on the resolution of other constraints are deferred until more information becomes available through the solving of simpler constraints.
Related constraints are batched together to reduce redundant work, enabling the algorithm to solve groups of interdependent constraints in a single pass rather than revisiting them multiple times. This scheduling strategy significantly reduces the overall computational cost of constraint solving by ensuring that each constraint is processed when it is most likely to be resolvable.
Constraints undergo systematic simplification before being added to the worklist to improve both performance and clarity. The algorithm eliminates trivial constraints such as \( A \leq A \) that are always satisfied, preventing unnecessary work and reducing clutter in the constraint system. Related constraints are combined when possible to reduce the overall worklist size, such as merging multiple subtyping constraints involving the same types into more comprehensive relationships.
The simplification process also enables early detection of unsatisfiable constraints, allowing the algorithm to report type errors immediately rather than continuing with doomed constraint solving attempts. This preprocessing step ensures that the worklist contains only meaningful constraints that contribute to the type inference process, making the overall algorithm more efficient and the resulting error messages more precise.
Putting It All Together
And there we have it - a complete System F-ω type checker with bidirectional inference, higher-kinded types, and constraint solving! The DK algorithm transforms what could be an intractable type inference problem into a systematic, decidable process that handles some of the most advanced features in type theory.
Let’s see our type checker in action with a simple polymorphic example. First, create a test file:
-- test_identity.hs
identity :: forall a. a -> a;
identity x = x;
test_int :: Int;
test_int = identity 42;
Now run the type checker:
$ cd system-f-omega
$ cargo run -- check test_identity.hs
The system produces output showing the successful type checking:
Parsed 4 declarations
Compiled to 0 type definitions and 2 term definitions
Checking identity : ∀a. a -> a ... ✓
Checking test_int : Int ... ✓
✓ Module 'test_identity.hs' typechecks successfully!
Perfect! Our type checker correctly verified that identity has the polymorphic type \( \forall a. a \to a \) and that test_int properly instantiates it with Int. The DK algorithm handled the universal quantification, constraint generation, and instantiation with all the sophistication of a production-quality type system.