Implementation
Types and Predicates
The type language is the small core of variables, type constructors with arguments, and arrows. Predicates are the new syntactic category that travels alongside types throughout inference.
#![allow(unused)] fn main() { use std::fmt; pub type Name = String; #[derive(Debug, Clone, PartialEq)] pub enum Lit { Int(i64), Bool(bool), } #[derive(Debug, Clone, PartialEq)] pub enum Expr { Var(Name), Lit(Lit), Abs(Name, Box<Expr>), App(Box<Expr>, Box<Expr>), Let(Name, Box<Expr>, Box<Expr>), } impl Type { pub fn int() -> Type { Type::Con("Int".into(), vec![]) } pub fn bool() -> Type { Type::Con("Bool".into(), vec![]) } pub fn arrow(a: Type, b: Type) -> Type { Type::Arrow(Box::new(a), Box::new(b)) } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct Pred { pub class: Name, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct Qual { pub preds: Vec<Pred>, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct Scheme { pub vars: Vec<Name>, pub qual: Qual, } #[derive(Debug, Clone, PartialEq)] pub struct ClassDecl { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub struct InstanceDecl { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub enum Decl { Class(ClassDecl), Instance(InstanceDecl), Let(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum TopLevelItem { Decl(Decl), Expr(Expr), } #[derive(Debug, Clone, PartialEq)] pub enum ClassItemAst { Sig(Name, Type), Default(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum Core { Var(Name), Lit(Lit), Abs(Name, Box<Core>), App(Box<Core>, Box<Core>), Let(Name, Box<Core>, Box<Core>), DictAbs(Vec<(Name, Pred)>, Box<Core>), DictApp(Box<Core>, Vec<Core>), DictProj(Box<Core>, Name), DictRec(Name, Type, Vec<(Name, Core)>), } impl fmt::Display for Lit { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Lit::Int(n) => write!(f, "{}", n), Lit::Bool(b) => write!(f, "{}", b), } } } impl fmt::Display for Expr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Expr::Var(n) => write!(f, "{}", n), Expr::Lit(l) => write!(f, "{}", l), Expr::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Expr::App(g, x) => match (g.as_ref(), x.as_ref()) { (Expr::Abs(_, _), _) => write!(f, "({}) {}", g, x), (_, Expr::App(_, _)) | (_, Expr::Abs(_, _)) => write!(f, "{} ({})", g, x), _ => write!(f, "{} {}", g, x), }, Expr::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), } } } impl fmt::Display for Type { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Type::Var(n) => write!(f, "{}", n), Type::Con(n, args) if args.is_empty() => write!(f, "{}", n), Type::Con(n, args) => { write!(f, "{}", n)?; for a in args { match a { Type::Con(_, inner) if inner.is_empty() => write!(f, " {}", a)?, Type::Var(_) => write!(f, " {}", a)?, _ => write!(f, " ({})", a)?, } } Ok(()) } Type::Arrow(a, b) => match a.as_ref() { Type::Arrow(_, _) => write!(f, "({}) -> {}", a, b), _ => write!(f, "{} -> {}", a, b), }, } } } impl fmt::Display for Pred { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match &self.ty { Type::Con(_, args) if !args.is_empty() => write!(f, "{} ({})", self.class, self.ty), Type::Arrow(_, _) => write!(f, "{} ({})", self.class, self.ty), _ => write!(f, "{} {}", self.class, self.ty), } } } impl fmt::Display for Qual { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.preds.is_empty() { write!(f, "{}", self.ty) } else if self.preds.len() == 1 { write!(f, "{} => {}", self.preds[0], self.ty) } else { write!(f, "(")?; for (i, p) in self.preds.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", p)?; } write!(f, ") => {}", self.ty) } } } impl fmt::Display for Scheme { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.vars.is_empty() { write!(f, "{}", self.qual) } else { write!(f, "forall {}. {}", self.vars.join(" "), self.qual) } } } impl fmt::Display for Core { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Core::Var(n) => write!(f, "{}", n), Core::Lit(l) => write!(f, "{}", l), Core::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Core::App(g, x) => match (g.as_ref(), x.as_ref()) { (Core::Abs(_, _) | Core::DictAbs(_, _), _) => write!(f, "({}) {}", g, x), (_, Core::App(_, _) | Core::Abs(_, _) | Core::DictAbs(_, _)) => { write!(f, "{} ({})", g, x) } _ => write!(f, "{} {}", g, x), }, Core::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), Core::DictAbs(binders, body) => { write!(f, "\\")?; for (i, (d, p)) in binders.iter().enumerate() { if i > 0 { write!(f, " ")?; } write!(f, "({} : {})", d, p)?; } write!(f, " -> {}", body) } Core::DictApp(g, args) => { write!(f, "{}", g)?; for a in args { match a { Core::Var(_) | Core::DictProj(_, _) => write!(f, " @{}", a)?, _ => write!(f, " @({})", a)?, } } Ok(()) } Core::DictProj(d, m) => write!(f, "{}.{}", d, m), Core::DictRec(cls, ty, methods) => { write!(f, "<{} {}: ", cls, ty)?; for (i, (m, e)) in methods.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{} = {}", m, e)?; } write!(f, ">") } } } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Type { Var(Name), Con(Name, Vec<Type>), Arrow(Box<Type>, Box<Type>), } }
The Var constructor wraps a type variable name, the workhorse of polymorphism. The Con constructor pairs a type constructor name with a vector of argument types and covers everything from nullary primitives like Int (encoded as Con("Int", [])) to parameterised constructors like List Int (encoded as Con("List", [Con("Int", [])])). The Arr constructor builds a function type from an argument and a result. Arrows are not encoded as a special two-argument constructor because the inference engine specialises on them, and the dedicated case keeps the substitution and unification code transparent.
#![allow(unused)] fn main() { use std::fmt; pub type Name = String; #[derive(Debug, Clone, PartialEq)] pub enum Lit { Int(i64), Bool(bool), } #[derive(Debug, Clone, PartialEq)] pub enum Expr { Var(Name), Lit(Lit), Abs(Name, Box<Expr>), App(Box<Expr>, Box<Expr>), Let(Name, Box<Expr>, Box<Expr>), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Type { Var(Name), Con(Name, Vec<Type>), Arrow(Box<Type>, Box<Type>), } impl Type { pub fn int() -> Type { Type::Con("Int".into(), vec![]) } pub fn bool() -> Type { Type::Con("Bool".into(), vec![]) } pub fn arrow(a: Type, b: Type) -> Type { Type::Arrow(Box::new(a), Box::new(b)) } } #[derive(Debug, Clone, PartialEq)] pub struct Qual { pub preds: Vec<Pred>, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct Scheme { pub vars: Vec<Name>, pub qual: Qual, } #[derive(Debug, Clone, PartialEq)] pub struct ClassDecl { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub struct InstanceDecl { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub enum Decl { Class(ClassDecl), Instance(InstanceDecl), Let(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum TopLevelItem { Decl(Decl), Expr(Expr), } #[derive(Debug, Clone, PartialEq)] pub enum ClassItemAst { Sig(Name, Type), Default(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum Core { Var(Name), Lit(Lit), Abs(Name, Box<Core>), App(Box<Core>, Box<Core>), Let(Name, Box<Core>, Box<Core>), DictAbs(Vec<(Name, Pred)>, Box<Core>), DictApp(Box<Core>, Vec<Core>), DictProj(Box<Core>, Name), DictRec(Name, Type, Vec<(Name, Core)>), } impl fmt::Display for Lit { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Lit::Int(n) => write!(f, "{}", n), Lit::Bool(b) => write!(f, "{}", b), } } } impl fmt::Display for Expr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Expr::Var(n) => write!(f, "{}", n), Expr::Lit(l) => write!(f, "{}", l), Expr::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Expr::App(g, x) => match (g.as_ref(), x.as_ref()) { (Expr::Abs(_, _), _) => write!(f, "({}) {}", g, x), (_, Expr::App(_, _)) | (_, Expr::Abs(_, _)) => write!(f, "{} ({})", g, x), _ => write!(f, "{} {}", g, x), }, Expr::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), } } } impl fmt::Display for Type { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Type::Var(n) => write!(f, "{}", n), Type::Con(n, args) if args.is_empty() => write!(f, "{}", n), Type::Con(n, args) => { write!(f, "{}", n)?; for a in args { match a { Type::Con(_, inner) if inner.is_empty() => write!(f, " {}", a)?, Type::Var(_) => write!(f, " {}", a)?, _ => write!(f, " ({})", a)?, } } Ok(()) } Type::Arrow(a, b) => match a.as_ref() { Type::Arrow(_, _) => write!(f, "({}) -> {}", a, b), _ => write!(f, "{} -> {}", a, b), }, } } } impl fmt::Display for Pred { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match &self.ty { Type::Con(_, args) if !args.is_empty() => write!(f, "{} ({})", self.class, self.ty), Type::Arrow(_, _) => write!(f, "{} ({})", self.class, self.ty), _ => write!(f, "{} {}", self.class, self.ty), } } } impl fmt::Display for Qual { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.preds.is_empty() { write!(f, "{}", self.ty) } else if self.preds.len() == 1 { write!(f, "{} => {}", self.preds[0], self.ty) } else { write!(f, "(")?; for (i, p) in self.preds.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", p)?; } write!(f, ") => {}", self.ty) } } } impl fmt::Display for Scheme { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.vars.is_empty() { write!(f, "{}", self.qual) } else { write!(f, "forall {}. {}", self.vars.join(" "), self.qual) } } } impl fmt::Display for Core { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Core::Var(n) => write!(f, "{}", n), Core::Lit(l) => write!(f, "{}", l), Core::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Core::App(g, x) => match (g.as_ref(), x.as_ref()) { (Core::Abs(_, _) | Core::DictAbs(_, _), _) => write!(f, "({}) {}", g, x), (_, Core::App(_, _) | Core::Abs(_, _) | Core::DictAbs(_, _)) => { write!(f, "{} ({})", g, x) } _ => write!(f, "{} {}", g, x), }, Core::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), Core::DictAbs(binders, body) => { write!(f, "\\")?; for (i, (d, p)) in binders.iter().enumerate() { if i > 0 { write!(f, " ")?; } write!(f, "({} : {})", d, p)?; } write!(f, " -> {}", body) } Core::DictApp(g, args) => { write!(f, "{}", g)?; for a in args { match a { Core::Var(_) | Core::DictProj(_, _) => write!(f, " @{}", a)?, _ => write!(f, " @({})", a)?, } } Ok(()) } Core::DictProj(d, m) => write!(f, "{}.{}", d, m), Core::DictRec(cls, ty, methods) => { write!(f, "<{} {}: ", cls, ty)?; for (i, (m, e)) in methods.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{} = {}", m, e)?; } write!(f, ">") } } } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct Pred { pub class: Name, pub ty: Type, } }
The class field is the name of the class being asserted and the ty field is the single type the assertion is about. A predicate Eq Int has class "Eq" and type Type::int(). A predicate Ord (List a) has class "Ord" and type Type::Con("List", [Type::Var("a")]). There is no separate notion of multi-parameter classes in this fragment, so the type field is always a single type rather than a vector.
A qualified type pairs a list of predicates with a head type.
#![allow(unused)] fn main() { use std::fmt; pub type Name = String; #[derive(Debug, Clone, PartialEq)] pub enum Lit { Int(i64), Bool(bool), } #[derive(Debug, Clone, PartialEq)] pub enum Expr { Var(Name), Lit(Lit), Abs(Name, Box<Expr>), App(Box<Expr>, Box<Expr>), Let(Name, Box<Expr>, Box<Expr>), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Type { Var(Name), Con(Name, Vec<Type>), Arrow(Box<Type>, Box<Type>), } impl Type { pub fn int() -> Type { Type::Con("Int".into(), vec![]) } pub fn bool() -> Type { Type::Con("Bool".into(), vec![]) } pub fn arrow(a: Type, b: Type) -> Type { Type::Arrow(Box::new(a), Box::new(b)) } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct Pred { pub class: Name, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct Scheme { pub vars: Vec<Name>, pub qual: Qual, } #[derive(Debug, Clone, PartialEq)] pub struct ClassDecl { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub struct InstanceDecl { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub enum Decl { Class(ClassDecl), Instance(InstanceDecl), Let(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum TopLevelItem { Decl(Decl), Expr(Expr), } #[derive(Debug, Clone, PartialEq)] pub enum ClassItemAst { Sig(Name, Type), Default(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum Core { Var(Name), Lit(Lit), Abs(Name, Box<Core>), App(Box<Core>, Box<Core>), Let(Name, Box<Core>, Box<Core>), DictAbs(Vec<(Name, Pred)>, Box<Core>), DictApp(Box<Core>, Vec<Core>), DictProj(Box<Core>, Name), DictRec(Name, Type, Vec<(Name, Core)>), } impl fmt::Display for Lit { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Lit::Int(n) => write!(f, "{}", n), Lit::Bool(b) => write!(f, "{}", b), } } } impl fmt::Display for Expr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Expr::Var(n) => write!(f, "{}", n), Expr::Lit(l) => write!(f, "{}", l), Expr::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Expr::App(g, x) => match (g.as_ref(), x.as_ref()) { (Expr::Abs(_, _), _) => write!(f, "({}) {}", g, x), (_, Expr::App(_, _)) | (_, Expr::Abs(_, _)) => write!(f, "{} ({})", g, x), _ => write!(f, "{} {}", g, x), }, Expr::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), } } } impl fmt::Display for Type { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Type::Var(n) => write!(f, "{}", n), Type::Con(n, args) if args.is_empty() => write!(f, "{}", n), Type::Con(n, args) => { write!(f, "{}", n)?; for a in args { match a { Type::Con(_, inner) if inner.is_empty() => write!(f, " {}", a)?, Type::Var(_) => write!(f, " {}", a)?, _ => write!(f, " ({})", a)?, } } Ok(()) } Type::Arrow(a, b) => match a.as_ref() { Type::Arrow(_, _) => write!(f, "({}) -> {}", a, b), _ => write!(f, "{} -> {}", a, b), }, } } } impl fmt::Display for Pred { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match &self.ty { Type::Con(_, args) if !args.is_empty() => write!(f, "{} ({})", self.class, self.ty), Type::Arrow(_, _) => write!(f, "{} ({})", self.class, self.ty), _ => write!(f, "{} {}", self.class, self.ty), } } } impl fmt::Display for Qual { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.preds.is_empty() { write!(f, "{}", self.ty) } else if self.preds.len() == 1 { write!(f, "{} => {}", self.preds[0], self.ty) } else { write!(f, "(")?; for (i, p) in self.preds.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", p)?; } write!(f, ") => {}", self.ty) } } } impl fmt::Display for Scheme { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.vars.is_empty() { write!(f, "{}", self.qual) } else { write!(f, "forall {}. {}", self.vars.join(" "), self.qual) } } } impl fmt::Display for Core { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Core::Var(n) => write!(f, "{}", n), Core::Lit(l) => write!(f, "{}", l), Core::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Core::App(g, x) => match (g.as_ref(), x.as_ref()) { (Core::Abs(_, _) | Core::DictAbs(_, _), _) => write!(f, "({}) {}", g, x), (_, Core::App(_, _) | Core::Abs(_, _) | Core::DictAbs(_, _)) => { write!(f, "{} ({})", g, x) } _ => write!(f, "{} {}", g, x), }, Core::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), Core::DictAbs(binders, body) => { write!(f, "\\")?; for (i, (d, p)) in binders.iter().enumerate() { if i > 0 { write!(f, " ")?; } write!(f, "({} : {})", d, p)?; } write!(f, " -> {}", body) } Core::DictApp(g, args) => { write!(f, "{}", g)?; for a in args { match a { Core::Var(_) | Core::DictProj(_, _) => write!(f, " @{}", a)?, _ => write!(f, " @({})", a)?, } } Ok(()) } Core::DictProj(d, m) => write!(f, "{}.{}", d, m), Core::DictRec(cls, ty, methods) => { write!(f, "<{} {}: ", cls, ty)?; for (i, (m, e)) in methods.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{} = {}", m, e)?; } write!(f, ">") } } } } #[derive(Debug, Clone, PartialEq)] pub struct Qual { pub preds: Vec<Pred>, pub ty: Type, } }
The preds field is the context of predicates that must be discharged before the term takes on its head type, and the ty field is the head type itself. The qualified type Eq a => a -> a -> Bool has predicates [Eq a] and head a -> a -> Bool. The empty context is the degenerate qualified type that is indistinguishable from a plain monotype.
A scheme quantifies over type variables with a qualified body.
#![allow(unused)] fn main() { use std::fmt; pub type Name = String; #[derive(Debug, Clone, PartialEq)] pub enum Lit { Int(i64), Bool(bool), } #[derive(Debug, Clone, PartialEq)] pub enum Expr { Var(Name), Lit(Lit), Abs(Name, Box<Expr>), App(Box<Expr>, Box<Expr>), Let(Name, Box<Expr>, Box<Expr>), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Type { Var(Name), Con(Name, Vec<Type>), Arrow(Box<Type>, Box<Type>), } impl Type { pub fn int() -> Type { Type::Con("Int".into(), vec![]) } pub fn bool() -> Type { Type::Con("Bool".into(), vec![]) } pub fn arrow(a: Type, b: Type) -> Type { Type::Arrow(Box::new(a), Box::new(b)) } } #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct Pred { pub class: Name, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct Qual { pub preds: Vec<Pred>, pub ty: Type, } #[derive(Debug, Clone, PartialEq)] pub struct ClassDecl { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub struct InstanceDecl { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Expr)>, } #[derive(Debug, Clone, PartialEq)] pub enum Decl { Class(ClassDecl), Instance(InstanceDecl), Let(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum TopLevelItem { Decl(Decl), Expr(Expr), } #[derive(Debug, Clone, PartialEq)] pub enum ClassItemAst { Sig(Name, Type), Default(Name, Expr), } #[derive(Debug, Clone, PartialEq)] pub enum Core { Var(Name), Lit(Lit), Abs(Name, Box<Core>), App(Box<Core>, Box<Core>), Let(Name, Box<Core>, Box<Core>), DictAbs(Vec<(Name, Pred)>, Box<Core>), DictApp(Box<Core>, Vec<Core>), DictProj(Box<Core>, Name), DictRec(Name, Type, Vec<(Name, Core)>), } impl fmt::Display for Lit { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Lit::Int(n) => write!(f, "{}", n), Lit::Bool(b) => write!(f, "{}", b), } } } impl fmt::Display for Expr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Expr::Var(n) => write!(f, "{}", n), Expr::Lit(l) => write!(f, "{}", l), Expr::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Expr::App(g, x) => match (g.as_ref(), x.as_ref()) { (Expr::Abs(_, _), _) => write!(f, "({}) {}", g, x), (_, Expr::App(_, _)) | (_, Expr::Abs(_, _)) => write!(f, "{} ({})", g, x), _ => write!(f, "{} {}", g, x), }, Expr::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), } } } impl fmt::Display for Type { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Type::Var(n) => write!(f, "{}", n), Type::Con(n, args) if args.is_empty() => write!(f, "{}", n), Type::Con(n, args) => { write!(f, "{}", n)?; for a in args { match a { Type::Con(_, inner) if inner.is_empty() => write!(f, " {}", a)?, Type::Var(_) => write!(f, " {}", a)?, _ => write!(f, " ({})", a)?, } } Ok(()) } Type::Arrow(a, b) => match a.as_ref() { Type::Arrow(_, _) => write!(f, "({}) -> {}", a, b), _ => write!(f, "{} -> {}", a, b), }, } } } impl fmt::Display for Pred { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match &self.ty { Type::Con(_, args) if !args.is_empty() => write!(f, "{} ({})", self.class, self.ty), Type::Arrow(_, _) => write!(f, "{} ({})", self.class, self.ty), _ => write!(f, "{} {}", self.class, self.ty), } } } impl fmt::Display for Qual { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.preds.is_empty() { write!(f, "{}", self.ty) } else if self.preds.len() == 1 { write!(f, "{} => {}", self.preds[0], self.ty) } else { write!(f, "(")?; for (i, p) in self.preds.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", p)?; } write!(f, ") => {}", self.ty) } } } impl fmt::Display for Scheme { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { if self.vars.is_empty() { write!(f, "{}", self.qual) } else { write!(f, "forall {}. {}", self.vars.join(" "), self.qual) } } } impl fmt::Display for Core { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Core::Var(n) => write!(f, "{}", n), Core::Lit(l) => write!(f, "{}", l), Core::Abs(p, b) => write!(f, "\\{} -> {}", p, b), Core::App(g, x) => match (g.as_ref(), x.as_ref()) { (Core::Abs(_, _) | Core::DictAbs(_, _), _) => write!(f, "({}) {}", g, x), (_, Core::App(_, _) | Core::Abs(_, _) | Core::DictAbs(_, _)) => { write!(f, "{} ({})", g, x) } _ => write!(f, "{} {}", g, x), }, Core::Let(v, e1, e2) => write!(f, "let {} = {} in {}", v, e1, e2), Core::DictAbs(binders, body) => { write!(f, "\\")?; for (i, (d, p)) in binders.iter().enumerate() { if i > 0 { write!(f, " ")?; } write!(f, "({} : {})", d, p)?; } write!(f, " -> {}", body) } Core::DictApp(g, args) => { write!(f, "{}", g)?; for a in args { match a { Core::Var(_) | Core::DictProj(_, _) => write!(f, " @{}", a)?, _ => write!(f, " @({})", a)?, } } Ok(()) } Core::DictProj(d, m) => write!(f, "{}.{}", d, m), Core::DictRec(cls, ty, methods) => { write!(f, "<{} {}: ", cls, ty)?; for (i, (m, e)) in methods.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{} = {}", m, e)?; } write!(f, ">") } } } } #[derive(Debug, Clone, PartialEq)] pub struct Scheme { pub vars: Vec<Name>, pub qual: Qual, } }
The vars field is the list of universally quantified type variables and the qual field is the qualified body the quantifiers bind. The scheme forall a. Eq a => a -> a -> Bool is Scheme { vars: ["a"], qual: Qual { preds: [Eq a], ty: a -> a -> Bool } }. The pretty printer writes the empty context invisibly and the singleton context without parentheses, so a class with no predicates prints as ordinary HM.
Inference
Inference is Algorithm W with one additional output: a list of pending predicates collected from each subterm. The return type is a quadruple of substitution, type, pending predicates, and an elaborated core term.
#![allow(unused)] fn main() { pub fn infer_expr(&mut self, expr: &Expr) -> Result<Inferred> { match expr { Expr::Lit(Lit::Int(_)) => Ok(( Subst::empty(), Type::int(), vec![], Core::Lit(match expr { Expr::Lit(l) => l.clone(), _ => unreachable!(), }), )), Expr::Lit(Lit::Bool(_)) => Ok(( Subst::empty(), Type::bool(), vec![], Core::Lit(match expr { Expr::Lit(l) => l.clone(), _ => unreachable!(), }), )), Expr::Var(name) => self.infer_var(name), Expr::Abs(param, body) => self.infer_abs(param, body), Expr::App(f, x) => self.infer_app(f, x), Expr::Let(v, e1, e2) => self.infer_let(v, e1, e2), } } }
The variable case instantiates the bound scheme, replacing each universally quantified variable with a fresh type variable and each context predicate with a fresh dictionary variable. The list of fresh dictionary variables threaded through the result is the source of all pending predicates in the system.
#![allow(unused)] fn main() { /// T-Var: x : ∀ᾱ. Q ⇒ τ ∈ Γ β̄ fresh σ = [β̄/ᾱ] /// ─────────────────────────────────────────── /// σ(Q) | Γ ⊢ x : σ(τ) fn infer_var(&mut self, name: &str) -> Result<Inferred> { let sch = self .env .get(name) .cloned() .ok_or_else(|| InferenceError::UnboundVariable { name: name.to_string(), })?; let (ty, pending) = self.instantiate(&sch); let core = if let Some((ci, _)) = self.class_env.lookup_method(&name.to_string()) { let class_name = ci.name.clone(); let dict_var = pending .iter() .find(|(_, p)| p.class == class_name) .map(|(d, _)| d.clone()) .ok_or_else(|| InferenceError::UnknownMethod { name: name.to_string(), })?; Core::DictProj(Box::new(Core::Var(dict_var)), name.to_string()) } else if pending.is_empty() { Core::Var(name.to_string()) } else { let args: Vec<Core> = pending.iter().map(|(d, _)| Core::Var(d.clone())).collect(); Core::DictApp(Box::new(Core::Var(name.to_string())), args) }; Ok((Subst::empty(), ty, pending, core)) } }
When the referenced name is a class method rather than an ordinary binding, the elaborated form is a projection out of the freshly introduced dictionary variable rather than a use of the source name. This is what justifies erasing the method’s source identity entirely once elaboration is done. When the name is an ordinary qualified binding such as a generalised let-bound function, the elaborated form is an explicit dictionary application that supplies the fresh dictionary variables as type-class arguments.
Abstraction extends the environment with a monomorphic scheme for the parameter, infers the body, and assembles an arrow.
#![allow(unused)] fn main() { /// T-Abs: P | Γ, x:α ⊢ e : τ α fresh /// ──────────────────────────── /// P | Γ ⊢ λx.e : α → τ fn infer_abs(&mut self, param: &str, body: &Expr) -> Result<Inferred> { let param_ty = Type::Var(self.fresh_tyvar()); let prev = self.env.insert( param.to_string(), Scheme { vars: vec![], qual: Qual { preds: vec![], ty: param_ty.clone(), }, }, ); let (s, body_ty, preds, body_core) = self.infer_expr(body)?; match prev { Some(old) => { self.env.insert(param.to_string(), old); } None => { self.env.remove(param); } } let arrow = Type::arrow(apply_type(&s, ¶m_ty), body_ty); let core = Core::Abs(param.to_string(), Box::new(body_core)); Ok((s, arrow, preds, core)) } }
Predicates collected from the body pass through unchanged. The scheme for the parameter is monomorphic because Hindley-Milner does not generalise inside a lambda, so any predicate that arises inside the body must wait until at least the surrounding let-binding for a chance to be generalised or discharged.
Application is the standard rule with predicate union. The function and the argument both produce pending predicates, and the result inherits both.
#![allow(unused)] fn main() { /// T-App: P | Γ ⊢ e₁ : τ₁ Q | Γ ⊢ e₂ : τ₂ S = unify(τ₁, τ₂ → α) /// ───────────────────────────────────────────────────────── /// S(P ∪ Q) | Γ ⊢ e₁ e₂ : S(α) fn infer_app(&mut self, f: &Expr, x: &Expr) -> Result<Inferred> { let result_ty = Type::Var(self.fresh_tyvar()); let (s1, f_ty, p1, f_core) = self.infer_expr(f)?; self.apply_env(&s1); let (s2, x_ty, p2, x_core) = self.infer_expr(x)?; let f_ty2 = apply_type(&s2, &f_ty); let expected = Type::arrow(x_ty, result_ty.clone()); let s3 = unify(&f_ty2, &expected)?; let s = s3.compose(&s2.compose(&s1)); let ty = apply_type(&s3, &result_ty); let mut preds = apply_preds_pending(&s, &p1); preds.extend(apply_preds_pending(&s, &p2)); let core = Core::App(Box::new(f_core), Box::new(x_core)); Ok((s, ty, preds, core)) } }
Let is where generalisation happens and where predicates are split between the new scheme and the deferred context.
#![allow(unused)] fn main() { /// T-Let: P | Γ ⊢ e₁ : τ σ = gen(Γ, P ⇒ τ) Q | Γ, x:σ ⊢ e₂ : τ' /// ──────────────────────────────────────────────────────── /// Q | Γ ⊢ let x = e₁ in e₂ : τ' fn infer_let(&mut self, v: &str, e1: &Expr, e2: &Expr) -> Result<Inferred> { let (s1, t1, p1, c1) = self.infer_expr(e1)?; self.apply_env(&s1); let p1 = apply_preds_pending(&s1, &p1); let (scheme, c1_final, deferred) = self.generalize_binding(&t1, &p1, &c1)?; let prev = self.env.insert(v.to_string(), scheme); let (s2, t2, p2, c2) = self.infer_expr(e2)?; match prev { Some(old) => { self.env.insert(v.to_string(), old); } None => { self.env.remove(v); } } let mut preds = apply_preds_pending(&s2, &deferred); preds.extend(p2); let s = s2.compose(&s1); let core = Core::Let(v.to_string(), Box::new(c1_final), Box::new(c2)); Ok((s, t2, preds, core)) } }
After inferring the body of the binding, the inference engine calls generalize_binding to compute the scheme, the elaborated core term wrapped in a dictionary abstraction over the kept predicates, and the deferred predicates that escape into the surrounding context. The body of the let is then inferred under the new scheme, and its predicates pass through to the result.
Predicate Resolution
The class environment stores every declared class and every declared instance. Instance lookup is a structural match against the head pattern, and superclass projection walks the chain of declared superclasses.
#![allow(unused)] fn main() { use std::collections::BTreeMap; use crate::ast::{Core, Expr, Name, Pred, Type}; use crate::errors::{InferenceError, Result}; use crate::subst::{apply_pred, apply_type, match_pred, match_ty, Subst}; pub type Given = (Core, Pred); pub type Binder = (Name, Pred); pub type Discharged = (Pred, Core); pub type Removed = (Name, Core); #[derive(Debug, Clone)] pub struct ClassInfo { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone)] pub struct InstanceInfo { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Core)>, } #[derive(Debug, Default, Clone)] pub struct ClassEnv { pub classes: BTreeMap<Name, ClassInfo>, pub method_of: BTreeMap<Name, Name>, pub instances: Vec<InstanceInfo>, } impl ClassEnv { pub fn new() -> Self { Self::default() } pub fn add_class(&mut self, info: ClassInfo) -> Result<()> { for s in &info.supers { if !self.classes.contains_key(s) { return Err(InferenceError::MissingSuperclass { class: info.name.clone(), superclass: s.clone(), }); } } for (m, _) in &info.sigs { self.method_of.insert(m.clone(), info.name.clone()); } self.classes.insert(info.name.clone(), info); Ok(()) } pub fn add_instance(&mut self, inst: InstanceInfo) -> Result<()> { if !self.classes.contains_key(&inst.head.class) { return Err(InferenceError::UnknownClass { name: inst.head.class.clone(), }); } for existing in &self.instances { if existing.head.class == inst.head.class && overlaps(&existing.head.ty, &inst.head.ty) { return Err(InferenceError::DuplicateInstance { pred: inst.head.clone(), }); } } self.instances.push(inst); Ok(()) } pub fn lookup_method(&self, m: &Name) -> Option<(&ClassInfo, &Type)> { let cname = self.method_of.get(m)?; let ci = self.classes.get(cname)?; let sig = ci.sigs.iter().find(|(n, _)| n == m)?; Some((ci, &sig.1)) } pub fn class(&self, name: &Name) -> Option<&ClassInfo> { self.classes.get(name) } } fn overlaps(a: &Type, b: &Type) -> bool { match_ty(a, b).is_ok() || match_ty(b, a).is_ok() } pub fn by_super(ce: &ClassEnv, d: &Core, p: &Pred) -> Vec<(Core, Pred)> { let mut out = vec![(d.clone(), p.clone())]; if let Some(ci) = ce.class(&p.class) { for s in &ci.supers { let proj = Core::DictProj(Box::new(d.clone()), super_field(&p.class, s)); let sp = Pred { class: s.clone(), ty: p.ty.clone(), }; out.extend(by_super(ce, &proj, &sp)); } } out } pub fn super_field(class: &str, sup: &str) -> Name { format!("__super_{}__{}", class, sup) } pub fn resolve(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Result<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Ok(d2); } } } let (subgoals, idx) = by_inst(ce, p)?; let inst = &ce.instances[idx]; let s = match_pred(&inst.head, p)?; let sub_dicts: Result<Vec<Core>> = subgoals.iter().map(|sg| resolve(ce, givens, sg)).collect(); let sub_dicts = sub_dicts?; let instance_dict = build_instance_dict(inst, &s); if sub_dicts.is_empty() { Ok(instance_dict) } else { Ok(Core::DictApp(Box::new(instance_dict), sub_dicts)) } } fn build_instance_dict(inst: &InstanceInfo, s: &Subst) -> Core { let head_ty = apply_type(s, &inst.head.ty); Core::DictRec(inst.head.class.clone(), head_ty, inst.methods.clone()) } pub fn reduce( ce: &ClassEnv, givens: &[Given], preds: &[Pred], ) -> Result<(Vec<Discharged>, Vec<Pred>)> { let mut residual: Vec<Pred> = Vec::new(); let mut discharged: Vec<(Pred, Core)> = Vec::new(); for p in preds { if is_head_normal(p) { match resolve_from_givens(ce, givens, p) { Some(d) => discharged.push((p.clone(), d)), None => { if !residual.contains(p) { residual.push(p.clone()); } } } } else { let d = resolve(ce, givens, p)?; discharged.push((p.clone(), d)); } } Ok((discharged, residual)) } pub fn simplify_context(ce: &ClassEnv, binders: &[Binder]) -> (Vec<Binder>, Vec<Removed>) { let mut kept: Vec<Binder> = Vec::new(); let mut removed: Vec<Removed> = Vec::new(); for (i, (d, p)) in binders.iter().enumerate() { let context: Vec<Binder> = kept .iter() .cloned() .chain(binders.iter().skip(i + 1).cloned()) .collect(); match find_super_proof(ce, &context, p) { Some(core) => removed.push((d.clone(), core)), None => kept.push((d.clone(), p.clone())), } } (kept, removed) } fn find_super_proof(ce: &ClassEnv, context: &[Binder], goal: &Pred) -> Option<Core> { for (d, q) in context { let root = Core::Var(d.clone()); for (proj, sp) in by_super(ce, &root, q) { if &sp == goal && proj != root { return Some(proj); } } } None } fn is_head_normal(p: &Pred) -> bool { matches!(p.ty, Type::Var(_)) } fn resolve_from_givens(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Option<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Some(d2); } } } None } pub fn by_inst(ce: &ClassEnv, p: &Pred) -> Result<(Vec<Pred>, usize)> { for (idx, inst) in ce.instances.iter().enumerate() { if inst.head.class != p.class { continue; } if let Ok(s) = match_pred(&inst.head, p) { let subgoals = inst.context.iter().map(|q| apply_pred(&s, q)).collect(); return Ok((subgoals, idx)); } } Err(InferenceError::NoInstance { pred: p.clone() }) } }
The function returns the list of subgoals and the index of the matching instance. Subgoals are the instance’s context with the matcher substitution applied, which captures the standard Prolog-style resolution step: to prove Eq (List a), look up the instance Eq a => Eq (List a), substitute a for itself, and recurse to prove the subgoal Eq a.
Superclass projection is the dual: to prove Eq a from a hypothesis Ord a, project the hidden Eq field out of the Ord dictionary.
#![allow(unused)] fn main() { use std::collections::BTreeMap; use crate::ast::{Core, Expr, Name, Pred, Type}; use crate::errors::{InferenceError, Result}; use crate::subst::{apply_pred, apply_type, match_pred, match_ty, Subst}; pub type Given = (Core, Pred); pub type Binder = (Name, Pred); pub type Discharged = (Pred, Core); pub type Removed = (Name, Core); #[derive(Debug, Clone)] pub struct ClassInfo { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone)] pub struct InstanceInfo { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Core)>, } #[derive(Debug, Default, Clone)] pub struct ClassEnv { pub classes: BTreeMap<Name, ClassInfo>, pub method_of: BTreeMap<Name, Name>, pub instances: Vec<InstanceInfo>, } impl ClassEnv { pub fn new() -> Self { Self::default() } pub fn add_class(&mut self, info: ClassInfo) -> Result<()> { for s in &info.supers { if !self.classes.contains_key(s) { return Err(InferenceError::MissingSuperclass { class: info.name.clone(), superclass: s.clone(), }); } } for (m, _) in &info.sigs { self.method_of.insert(m.clone(), info.name.clone()); } self.classes.insert(info.name.clone(), info); Ok(()) } pub fn add_instance(&mut self, inst: InstanceInfo) -> Result<()> { if !self.classes.contains_key(&inst.head.class) { return Err(InferenceError::UnknownClass { name: inst.head.class.clone(), }); } for existing in &self.instances { if existing.head.class == inst.head.class && overlaps(&existing.head.ty, &inst.head.ty) { return Err(InferenceError::DuplicateInstance { pred: inst.head.clone(), }); } } self.instances.push(inst); Ok(()) } pub fn lookup_method(&self, m: &Name) -> Option<(&ClassInfo, &Type)> { let cname = self.method_of.get(m)?; let ci = self.classes.get(cname)?; let sig = ci.sigs.iter().find(|(n, _)| n == m)?; Some((ci, &sig.1)) } pub fn class(&self, name: &Name) -> Option<&ClassInfo> { self.classes.get(name) } } fn overlaps(a: &Type, b: &Type) -> bool { match_ty(a, b).is_ok() || match_ty(b, a).is_ok() } pub fn super_field(class: &str, sup: &str) -> Name { format!("__super_{}__{}", class, sup) } pub fn by_inst(ce: &ClassEnv, p: &Pred) -> Result<(Vec<Pred>, usize)> { for (idx, inst) in ce.instances.iter().enumerate() { if inst.head.class != p.class { continue; } if let Ok(s) = match_pred(&inst.head, p) { let subgoals = inst.context.iter().map(|q| apply_pred(&s, q)).collect(); return Ok((subgoals, idx)); } } Err(InferenceError::NoInstance { pred: p.clone() }) } pub fn resolve(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Result<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Ok(d2); } } } let (subgoals, idx) = by_inst(ce, p)?; let inst = &ce.instances[idx]; let s = match_pred(&inst.head, p)?; let sub_dicts: Result<Vec<Core>> = subgoals.iter().map(|sg| resolve(ce, givens, sg)).collect(); let sub_dicts = sub_dicts?; let instance_dict = build_instance_dict(inst, &s); if sub_dicts.is_empty() { Ok(instance_dict) } else { Ok(Core::DictApp(Box::new(instance_dict), sub_dicts)) } } fn build_instance_dict(inst: &InstanceInfo, s: &Subst) -> Core { let head_ty = apply_type(s, &inst.head.ty); Core::DictRec(inst.head.class.clone(), head_ty, inst.methods.clone()) } pub fn reduce( ce: &ClassEnv, givens: &[Given], preds: &[Pred], ) -> Result<(Vec<Discharged>, Vec<Pred>)> { let mut residual: Vec<Pred> = Vec::new(); let mut discharged: Vec<(Pred, Core)> = Vec::new(); for p in preds { if is_head_normal(p) { match resolve_from_givens(ce, givens, p) { Some(d) => discharged.push((p.clone(), d)), None => { if !residual.contains(p) { residual.push(p.clone()); } } } } else { let d = resolve(ce, givens, p)?; discharged.push((p.clone(), d)); } } Ok((discharged, residual)) } pub fn simplify_context(ce: &ClassEnv, binders: &[Binder]) -> (Vec<Binder>, Vec<Removed>) { let mut kept: Vec<Binder> = Vec::new(); let mut removed: Vec<Removed> = Vec::new(); for (i, (d, p)) in binders.iter().enumerate() { let context: Vec<Binder> = kept .iter() .cloned() .chain(binders.iter().skip(i + 1).cloned()) .collect(); match find_super_proof(ce, &context, p) { Some(core) => removed.push((d.clone(), core)), None => kept.push((d.clone(), p.clone())), } } (kept, removed) } fn find_super_proof(ce: &ClassEnv, context: &[Binder], goal: &Pred) -> Option<Core> { for (d, q) in context { let root = Core::Var(d.clone()); for (proj, sp) in by_super(ce, &root, q) { if &sp == goal && proj != root { return Some(proj); } } } None } fn is_head_normal(p: &Pred) -> bool { matches!(p.ty, Type::Var(_)) } fn resolve_from_givens(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Option<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Some(d2); } } } None } pub fn by_super(ce: &ClassEnv, d: &Core, p: &Pred) -> Vec<(Core, Pred)> { let mut out = vec![(d.clone(), p.clone())]; if let Some(ci) = ce.class(&p.class) { for s in &ci.supers { let proj = Core::DictProj(Box::new(d.clone()), super_field(&p.class, s)); let sp = Pred { class: s.clone(), ty: p.ty.clone(), }; out.extend(by_super(ce, &proj, &sp)); } } out } }
The function returns every predicate reachable from the starting hypothesis by following declared superclasses, paired with the corresponding core term that performs the projections. The name super_field(class, sup) is a deterministic mangling that picks out the slot for the superclass dictionary inside the subclass dictionary record. The chapter on Dictionary Elaboration explains how that slot is filled when the instance is declared.
The full resolver combines these two mechanisms.
#![allow(unused)] fn main() { use std::collections::BTreeMap; use crate::ast::{Core, Expr, Name, Pred, Type}; use crate::errors::{InferenceError, Result}; use crate::subst::{apply_pred, apply_type, match_pred, match_ty, Subst}; pub type Given = (Core, Pred); pub type Binder = (Name, Pred); pub type Discharged = (Pred, Core); pub type Removed = (Name, Core); #[derive(Debug, Clone)] pub struct ClassInfo { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone)] pub struct InstanceInfo { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Core)>, } #[derive(Debug, Default, Clone)] pub struct ClassEnv { pub classes: BTreeMap<Name, ClassInfo>, pub method_of: BTreeMap<Name, Name>, pub instances: Vec<InstanceInfo>, } impl ClassEnv { pub fn new() -> Self { Self::default() } pub fn add_class(&mut self, info: ClassInfo) -> Result<()> { for s in &info.supers { if !self.classes.contains_key(s) { return Err(InferenceError::MissingSuperclass { class: info.name.clone(), superclass: s.clone(), }); } } for (m, _) in &info.sigs { self.method_of.insert(m.clone(), info.name.clone()); } self.classes.insert(info.name.clone(), info); Ok(()) } pub fn add_instance(&mut self, inst: InstanceInfo) -> Result<()> { if !self.classes.contains_key(&inst.head.class) { return Err(InferenceError::UnknownClass { name: inst.head.class.clone(), }); } for existing in &self.instances { if existing.head.class == inst.head.class && overlaps(&existing.head.ty, &inst.head.ty) { return Err(InferenceError::DuplicateInstance { pred: inst.head.clone(), }); } } self.instances.push(inst); Ok(()) } pub fn lookup_method(&self, m: &Name) -> Option<(&ClassInfo, &Type)> { let cname = self.method_of.get(m)?; let ci = self.classes.get(cname)?; let sig = ci.sigs.iter().find(|(n, _)| n == m)?; Some((ci, &sig.1)) } pub fn class(&self, name: &Name) -> Option<&ClassInfo> { self.classes.get(name) } } fn overlaps(a: &Type, b: &Type) -> bool { match_ty(a, b).is_ok() || match_ty(b, a).is_ok() } pub fn by_super(ce: &ClassEnv, d: &Core, p: &Pred) -> Vec<(Core, Pred)> { let mut out = vec![(d.clone(), p.clone())]; if let Some(ci) = ce.class(&p.class) { for s in &ci.supers { let proj = Core::DictProj(Box::new(d.clone()), super_field(&p.class, s)); let sp = Pred { class: s.clone(), ty: p.ty.clone(), }; out.extend(by_super(ce, &proj, &sp)); } } out } pub fn super_field(class: &str, sup: &str) -> Name { format!("__super_{}__{}", class, sup) } pub fn by_inst(ce: &ClassEnv, p: &Pred) -> Result<(Vec<Pred>, usize)> { for (idx, inst) in ce.instances.iter().enumerate() { if inst.head.class != p.class { continue; } if let Ok(s) = match_pred(&inst.head, p) { let subgoals = inst.context.iter().map(|q| apply_pred(&s, q)).collect(); return Ok((subgoals, idx)); } } Err(InferenceError::NoInstance { pred: p.clone() }) } fn build_instance_dict(inst: &InstanceInfo, s: &Subst) -> Core { let head_ty = apply_type(s, &inst.head.ty); Core::DictRec(inst.head.class.clone(), head_ty, inst.methods.clone()) } pub fn reduce( ce: &ClassEnv, givens: &[Given], preds: &[Pred], ) -> Result<(Vec<Discharged>, Vec<Pred>)> { let mut residual: Vec<Pred> = Vec::new(); let mut discharged: Vec<(Pred, Core)> = Vec::new(); for p in preds { if is_head_normal(p) { match resolve_from_givens(ce, givens, p) { Some(d) => discharged.push((p.clone(), d)), None => { if !residual.contains(p) { residual.push(p.clone()); } } } } else { let d = resolve(ce, givens, p)?; discharged.push((p.clone(), d)); } } Ok((discharged, residual)) } pub fn simplify_context(ce: &ClassEnv, binders: &[Binder]) -> (Vec<Binder>, Vec<Removed>) { let mut kept: Vec<Binder> = Vec::new(); let mut removed: Vec<Removed> = Vec::new(); for (i, (d, p)) in binders.iter().enumerate() { let context: Vec<Binder> = kept .iter() .cloned() .chain(binders.iter().skip(i + 1).cloned()) .collect(); match find_super_proof(ce, &context, p) { Some(core) => removed.push((d.clone(), core)), None => kept.push((d.clone(), p.clone())), } } (kept, removed) } fn find_super_proof(ce: &ClassEnv, context: &[Binder], goal: &Pred) -> Option<Core> { for (d, q) in context { let root = Core::Var(d.clone()); for (proj, sp) in by_super(ce, &root, q) { if &sp == goal && proj != root { return Some(proj); } } } None } fn is_head_normal(p: &Pred) -> bool { matches!(p.ty, Type::Var(_)) } fn resolve_from_givens(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Option<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Some(d2); } } } None } pub fn resolve(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Result<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Ok(d2); } } } let (subgoals, idx) = by_inst(ce, p)?; let inst = &ce.instances[idx]; let s = match_pred(&inst.head, p)?; let sub_dicts: Result<Vec<Core>> = subgoals.iter().map(|sg| resolve(ce, givens, sg)).collect(); let sub_dicts = sub_dicts?; let instance_dict = build_instance_dict(inst, &s); if sub_dicts.is_empty() { Ok(instance_dict) } else { Ok(Core::DictApp(Box::new(instance_dict), sub_dicts)) } } }
The first pass tries to discharge the goal from the local givens, walking each given’s superclass chain in case the goal sits behind a chain of declared superclass relationships. The second pass tries to match the goal against an instance head, and recursively resolves the subgoals that the instance’s context introduces.
Context Reduction
After inference, the pending predicates may contain duplicates, predicates that are implied by other predicates in the same context, and predicates that can be discharged against the instance database without waiting for a more concrete call site. Context reduction collapses the list before generalisation.
#![allow(unused)] fn main() { use std::collections::BTreeMap; use crate::ast::{Core, Expr, Name, Pred, Type}; use crate::errors::{InferenceError, Result}; use crate::subst::{apply_pred, apply_type, match_pred, match_ty, Subst}; pub type Given = (Core, Pred); pub type Binder = (Name, Pred); pub type Discharged = (Pred, Core); pub type Removed = (Name, Core); #[derive(Debug, Clone)] pub struct ClassInfo { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone)] pub struct InstanceInfo { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Core)>, } #[derive(Debug, Default, Clone)] pub struct ClassEnv { pub classes: BTreeMap<Name, ClassInfo>, pub method_of: BTreeMap<Name, Name>, pub instances: Vec<InstanceInfo>, } impl ClassEnv { pub fn new() -> Self { Self::default() } pub fn add_class(&mut self, info: ClassInfo) -> Result<()> { for s in &info.supers { if !self.classes.contains_key(s) { return Err(InferenceError::MissingSuperclass { class: info.name.clone(), superclass: s.clone(), }); } } for (m, _) in &info.sigs { self.method_of.insert(m.clone(), info.name.clone()); } self.classes.insert(info.name.clone(), info); Ok(()) } pub fn add_instance(&mut self, inst: InstanceInfo) -> Result<()> { if !self.classes.contains_key(&inst.head.class) { return Err(InferenceError::UnknownClass { name: inst.head.class.clone(), }); } for existing in &self.instances { if existing.head.class == inst.head.class && overlaps(&existing.head.ty, &inst.head.ty) { return Err(InferenceError::DuplicateInstance { pred: inst.head.clone(), }); } } self.instances.push(inst); Ok(()) } pub fn lookup_method(&self, m: &Name) -> Option<(&ClassInfo, &Type)> { let cname = self.method_of.get(m)?; let ci = self.classes.get(cname)?; let sig = ci.sigs.iter().find(|(n, _)| n == m)?; Some((ci, &sig.1)) } pub fn class(&self, name: &Name) -> Option<&ClassInfo> { self.classes.get(name) } } fn overlaps(a: &Type, b: &Type) -> bool { match_ty(a, b).is_ok() || match_ty(b, a).is_ok() } pub fn by_super(ce: &ClassEnv, d: &Core, p: &Pred) -> Vec<(Core, Pred)> { let mut out = vec![(d.clone(), p.clone())]; if let Some(ci) = ce.class(&p.class) { for s in &ci.supers { let proj = Core::DictProj(Box::new(d.clone()), super_field(&p.class, s)); let sp = Pred { class: s.clone(), ty: p.ty.clone(), }; out.extend(by_super(ce, &proj, &sp)); } } out } pub fn super_field(class: &str, sup: &str) -> Name { format!("__super_{}__{}", class, sup) } pub fn by_inst(ce: &ClassEnv, p: &Pred) -> Result<(Vec<Pred>, usize)> { for (idx, inst) in ce.instances.iter().enumerate() { if inst.head.class != p.class { continue; } if let Ok(s) = match_pred(&inst.head, p) { let subgoals = inst.context.iter().map(|q| apply_pred(&s, q)).collect(); return Ok((subgoals, idx)); } } Err(InferenceError::NoInstance { pred: p.clone() }) } pub fn resolve(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Result<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Ok(d2); } } } let (subgoals, idx) = by_inst(ce, p)?; let inst = &ce.instances[idx]; let s = match_pred(&inst.head, p)?; let sub_dicts: Result<Vec<Core>> = subgoals.iter().map(|sg| resolve(ce, givens, sg)).collect(); let sub_dicts = sub_dicts?; let instance_dict = build_instance_dict(inst, &s); if sub_dicts.is_empty() { Ok(instance_dict) } else { Ok(Core::DictApp(Box::new(instance_dict), sub_dicts)) } } fn build_instance_dict(inst: &InstanceInfo, s: &Subst) -> Core { let head_ty = apply_type(s, &inst.head.ty); Core::DictRec(inst.head.class.clone(), head_ty, inst.methods.clone()) } pub fn simplify_context(ce: &ClassEnv, binders: &[Binder]) -> (Vec<Binder>, Vec<Removed>) { let mut kept: Vec<Binder> = Vec::new(); let mut removed: Vec<Removed> = Vec::new(); for (i, (d, p)) in binders.iter().enumerate() { let context: Vec<Binder> = kept .iter() .cloned() .chain(binders.iter().skip(i + 1).cloned()) .collect(); match find_super_proof(ce, &context, p) { Some(core) => removed.push((d.clone(), core)), None => kept.push((d.clone(), p.clone())), } } (kept, removed) } fn find_super_proof(ce: &ClassEnv, context: &[Binder], goal: &Pred) -> Option<Core> { for (d, q) in context { let root = Core::Var(d.clone()); for (proj, sp) in by_super(ce, &root, q) { if &sp == goal && proj != root { return Some(proj); } } } None } fn is_head_normal(p: &Pred) -> bool { matches!(p.ty, Type::Var(_)) } fn resolve_from_givens(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Option<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Some(d2); } } } None } pub fn reduce( ce: &ClassEnv, givens: &[Given], preds: &[Pred], ) -> Result<(Vec<Discharged>, Vec<Pred>)> { let mut residual: Vec<Pred> = Vec::new(); let mut discharged: Vec<(Pred, Core)> = Vec::new(); for p in preds { if is_head_normal(p) { match resolve_from_givens(ce, givens, p) { Some(d) => discharged.push((p.clone(), d)), None => { if !residual.contains(p) { residual.push(p.clone()); } } } } else { let d = resolve(ce, givens, p)?; discharged.push((p.clone(), d)); } } Ok((discharged, residual)) } }
A predicate is in head-normal form when its type is a type variable rather than a constructor applied to arguments. Predicates not in head-normal form, such as Eq (List a), cannot wait for a concrete instantiation because the head constructor is already concrete, so they are resolved immediately and their core proofs replace the dictionary variable in the elaborated term. Predicates in head-normal form, such as Eq a, may still be discharged against the local givens via superclass projection, but otherwise become part of the residual context that flows into the scheme.
Simplification removes predicates that are implied by others in the same context. The classic case is (Eq a, Ord a) => ... which collapses to Ord a => ... because the superclass declaration class Eq a => Ord a makes the Eq part recoverable from the Ord dictionary.
#![allow(unused)] fn main() { use std::collections::BTreeMap; use crate::ast::{Core, Expr, Name, Pred, Type}; use crate::errors::{InferenceError, Result}; use crate::subst::{apply_pred, apply_type, match_pred, match_ty, Subst}; pub type Given = (Core, Pred); pub type Binder = (Name, Pred); pub type Discharged = (Pred, Core); pub type Removed = (Name, Core); #[derive(Debug, Clone)] pub struct ClassInfo { pub name: Name, pub tyvar: Name, pub supers: Vec<Name>, pub sigs: Vec<(Name, Type)>, pub defaults: Vec<(Name, Expr)>, } #[derive(Debug, Clone)] pub struct InstanceInfo { pub context: Vec<Pred>, pub head: Pred, pub methods: Vec<(Name, Core)>, } #[derive(Debug, Default, Clone)] pub struct ClassEnv { pub classes: BTreeMap<Name, ClassInfo>, pub method_of: BTreeMap<Name, Name>, pub instances: Vec<InstanceInfo>, } impl ClassEnv { pub fn new() -> Self { Self::default() } pub fn add_class(&mut self, info: ClassInfo) -> Result<()> { for s in &info.supers { if !self.classes.contains_key(s) { return Err(InferenceError::MissingSuperclass { class: info.name.clone(), superclass: s.clone(), }); } } for (m, _) in &info.sigs { self.method_of.insert(m.clone(), info.name.clone()); } self.classes.insert(info.name.clone(), info); Ok(()) } pub fn add_instance(&mut self, inst: InstanceInfo) -> Result<()> { if !self.classes.contains_key(&inst.head.class) { return Err(InferenceError::UnknownClass { name: inst.head.class.clone(), }); } for existing in &self.instances { if existing.head.class == inst.head.class && overlaps(&existing.head.ty, &inst.head.ty) { return Err(InferenceError::DuplicateInstance { pred: inst.head.clone(), }); } } self.instances.push(inst); Ok(()) } pub fn lookup_method(&self, m: &Name) -> Option<(&ClassInfo, &Type)> { let cname = self.method_of.get(m)?; let ci = self.classes.get(cname)?; let sig = ci.sigs.iter().find(|(n, _)| n == m)?; Some((ci, &sig.1)) } pub fn class(&self, name: &Name) -> Option<&ClassInfo> { self.classes.get(name) } } fn overlaps(a: &Type, b: &Type) -> bool { match_ty(a, b).is_ok() || match_ty(b, a).is_ok() } pub fn by_super(ce: &ClassEnv, d: &Core, p: &Pred) -> Vec<(Core, Pred)> { let mut out = vec![(d.clone(), p.clone())]; if let Some(ci) = ce.class(&p.class) { for s in &ci.supers { let proj = Core::DictProj(Box::new(d.clone()), super_field(&p.class, s)); let sp = Pred { class: s.clone(), ty: p.ty.clone(), }; out.extend(by_super(ce, &proj, &sp)); } } out } pub fn super_field(class: &str, sup: &str) -> Name { format!("__super_{}__{}", class, sup) } pub fn by_inst(ce: &ClassEnv, p: &Pred) -> Result<(Vec<Pred>, usize)> { for (idx, inst) in ce.instances.iter().enumerate() { if inst.head.class != p.class { continue; } if let Ok(s) = match_pred(&inst.head, p) { let subgoals = inst.context.iter().map(|q| apply_pred(&s, q)).collect(); return Ok((subgoals, idx)); } } Err(InferenceError::NoInstance { pred: p.clone() }) } pub fn resolve(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Result<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Ok(d2); } } } let (subgoals, idx) = by_inst(ce, p)?; let inst = &ce.instances[idx]; let s = match_pred(&inst.head, p)?; let sub_dicts: Result<Vec<Core>> = subgoals.iter().map(|sg| resolve(ce, givens, sg)).collect(); let sub_dicts = sub_dicts?; let instance_dict = build_instance_dict(inst, &s); if sub_dicts.is_empty() { Ok(instance_dict) } else { Ok(Core::DictApp(Box::new(instance_dict), sub_dicts)) } } fn build_instance_dict(inst: &InstanceInfo, s: &Subst) -> Core { let head_ty = apply_type(s, &inst.head.ty); Core::DictRec(inst.head.class.clone(), head_ty, inst.methods.clone()) } pub fn reduce( ce: &ClassEnv, givens: &[Given], preds: &[Pred], ) -> Result<(Vec<Discharged>, Vec<Pred>)> { let mut residual: Vec<Pred> = Vec::new(); let mut discharged: Vec<(Pred, Core)> = Vec::new(); for p in preds { if is_head_normal(p) { match resolve_from_givens(ce, givens, p) { Some(d) => discharged.push((p.clone(), d)), None => { if !residual.contains(p) { residual.push(p.clone()); } } } } else { let d = resolve(ce, givens, p)?; discharged.push((p.clone(), d)); } } Ok((discharged, residual)) } fn find_super_proof(ce: &ClassEnv, context: &[Binder], goal: &Pred) -> Option<Core> { for (d, q) in context { let root = Core::Var(d.clone()); for (proj, sp) in by_super(ce, &root, q) { if &sp == goal && proj != root { return Some(proj); } } } None } fn is_head_normal(p: &Pred) -> bool { matches!(p.ty, Type::Var(_)) } fn resolve_from_givens(ce: &ClassEnv, givens: &[Given], p: &Pred) -> Option<Core> { for (d, q) in givens { for (d2, q2) in by_super(ce, d, q) { if &q2 == p { return Some(d2); } } } None } pub fn simplify_context(ce: &ClassEnv, binders: &[Binder]) -> (Vec<Binder>, Vec<Removed>) { let mut kept: Vec<Binder> = Vec::new(); let mut removed: Vec<Removed> = Vec::new(); for (i, (d, p)) in binders.iter().enumerate() { let context: Vec<Binder> = kept .iter() .cloned() .chain(binders.iter().skip(i + 1).cloned()) .collect(); match find_super_proof(ce, &context, p) { Some(core) => removed.push((d.clone(), core)), None => kept.push((d.clone(), p.clone())), } } (kept, removed) } }
The function walks the context one binder at a time. For each binder it asks whether the predicate can be recovered as a superclass projection from any of the remaining binders. If yes, the binder is removed and its dictionary variable is rewritten to the projection. If no, the binder is kept.
Generalisation
Generalisation builds the final scheme and the final elaborated body.
#![allow(unused)] fn main() { fn generalize_binding( &mut self, ty: &Type, pending: &[Binder], core: &Core, ) -> Result<(Scheme, Core, Pending)> { let env_ftv = self.env_ftv(); let mut ty_ftv = HashSet::new(); ftv_type(ty, &mut ty_ftv); let pending_preds: Vec<Pred> = pending.iter().map(|(_, p)| p.clone()).collect(); let (discharged, residual) = reduce(&self.class_env, &[], &pending_preds)?; let mut sub_map: HashMap<Name, Core> = HashMap::new(); for (p, c) in &discharged { for (d, q) in pending { if q == p { sub_map.insert(d.clone(), c.clone()); } } } let (residual_binders, deferred): (Vec<_>, Vec<_>) = residual .iter() .filter_map(|p| { pending .iter() .find(|(_, q)| q == p) .map(|(d, _)| (d.clone(), p.clone())) }) .partition(|(_, p)| { let mut pf = HashSet::new(); ftv_type(&p.ty, &mut pf); !pf.is_disjoint(&ty_ftv) || !pf.is_subset(&env_ftv) }); for (canonical_d, p) in &residual_binders { for (d, q) in pending { if q == p && d != canonical_d { sub_map.insert(d.clone(), Core::Var(canonical_d.clone())); } } } let binders = residual_binders; let (binders, removed) = simplify_context(&self.class_env, &binders); for (d, c) in &removed { sub_map.insert(d.clone(), c.clone()); } let kept_preds: Vec<Pred> = binders.iter().map(|(_, p)| p.clone()).collect(); let core1 = subst_core(core, &sub_map); let core_final = if binders.is_empty() { core1 } else { Core::DictAbs(binders.clone(), Box::new(core1)) }; let mut ambig = HashSet::new(); for p in &kept_preds { ftv_type(&p.ty, &mut ambig); } for v in &ambig { if !ty_ftv.contains(v) && !env_ftv.contains(v) { return Err(InferenceError::Ambiguous { pred: kept_preds .iter() .find(|p| { let mut s = HashSet::new(); ftv_type(&p.ty, &mut s); s.contains(v) }) .cloned() .unwrap(), }); } } let qual = Qual { preds: kept_preds, ty: ty.clone(), }; let quant: Vec<Name> = ftv_qual(&qual).difference(&env_ftv).cloned().collect(); let (scheme, core_final) = canonical_scheme_and_core(Scheme { vars: quant, qual }, core_final); Ok((scheme, core_final, deferred)) } }
The procedure runs in four passes. The first pass calls reduce to discharge non-head-normal predicates against the instance database. The second pass partitions the residual into those that touch the inferred type or escape into the surrounding environment, which are kept, and those that touch only variables already free in the environment, which are deferred. The third pass runs simplify_context to drop superclass-implied predicates from the kept list. The fourth pass builds a DictAbs wrapping the original core in a binder for each kept predicate, and assembles the final scheme with the kept predicates as its context and the kept type variables as its quantifiers.
The ambiguity check at the tail of the function rejects schemes that quantify over a type variable that appears only in a predicate and nowhere in the head type or the environment. The standard offender is \f -> primAndBool (eq (f 1)) ... where f has type Int -> a for some fresh a, the predicate Eq a is generated, and a appears nowhere in the head type so no call site could ever pick a witness. The error is the qualified-types analogue of an unsolvable metavariable.