diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index fd9bd96..4c8a9eb 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -753,7 +753,7 @@ fn collect_refs(def: &ailang_core::Def) -> std::collections::BTreeSet { // A type def references the types of its fields. for c in &td.ctors { for ft in &c.fields { - if let ailang_core::Type::Con { name } = ft { + if let ailang_core::Type::Con { name, .. } = ft { out.insert(format!("type:{name}")); } } diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 7d4b48a..cda0a65 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -73,7 +73,10 @@ impl Subst { } Type::Var { name: name.clone() } } - Type::Con { .. } => t.clone(), + Type::Con { name, args } => Type::Con { + name: name.clone(), + args: args.iter().map(|a| self.apply(a)).collect(), + }, Type::Fn { params, ret, effects } => Type::Fn { params: params.iter().map(|p| self.apply(p)).collect(), ret: Box::new(self.apply(ret)), @@ -108,7 +111,10 @@ fn instantiate(forall_vars: &[String], body: &Type, counter: &mut u32) -> (Vec) -> Type { match t { Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()), - Type::Con { .. } => t.clone(), + Type::Con { name, args } => Type::Con { + name: name.clone(), + args: args.iter().map(|a| substitute_rigids(a, mapping)).collect(), + }, Type::Fn { params, ret, effects } => Type::Fn { params: params.iter().map(|p| substitute_rigids(p, mapping)).collect(), ret: Box::new(substitute_rigids(ret, mapping)), @@ -135,7 +141,7 @@ fn occurs(id: u32, t: &Type, subst: &Subst) -> bool { let t = subst.apply(t); match &t { Type::Var { name } => Subst::meta_id(name) == Some(id), - Type::Con { .. } => false, + Type::Con { args, .. } => args.iter().any(|a| occurs(id, a, subst)), Type::Fn { params, ret, .. } => { params.iter().any(|p| occurs(id, p, subst)) || occurs(id, ret, subst) } @@ -179,8 +185,17 @@ fn unify(a: &Type, b: &Type, subst: &mut Subst) -> Result<()> { } // Rigid vars: only unify with the same name. (Type::Var { name: an }, Type::Var { name: bn }) if an == bn => Ok(()), - // Concrete con: same name. - (Type::Con { name: an }, Type::Con { name: bn }) if an == bn => Ok(()), + // Concrete con: same name and same arity, then unify args + // pointwise. Iter 13a: parameterised ADTs unify arg-by-arg. + ( + Type::Con { name: an, args: aa }, + Type::Con { name: bn, args: ba }, + ) if an == bn && aa.len() == ba.len() => { + for (x, y) in aa.iter().zip(ba.iter()) { + unify(x, y, subst)?; + } + Ok(()) + } // Function types: zip params, unify ret, effects must match as a set. ( Type::Fn { params: ap, ret: ar, effects: ae }, @@ -521,6 +536,7 @@ pub fn check(m: &Module) -> Result { Def::Const(c) => c.ty.clone(), Def::Type(_) => Type::Con { name: def.name().to_string(), + args: vec![], }, }; symbols.insert(def.name().to_string(), (ty, h)); @@ -558,6 +574,7 @@ fn build_module_globals( Def::Const(c) => c.ty.clone(), Def::Type(_) => Type::Con { name: def_name.to_string(), + args: vec![], }, }; globals.insert(def_name.to_string(), ty); @@ -666,11 +683,17 @@ fn check_def(def: &Def, env: &Env) -> Result<()> { } fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> { - // All fields must reference known types (or other ADTs from this - // module; recursion is allowed). + // Iter 13a: a parameterised ADT (`vars` non-empty) installs its + // type parameters as rigid vars while checking the ctor field + // types, so `List a = ... | Cons(a, List a)` resolves both + // occurrences of `a` and the recursive use of `List a` correctly. + let mut env = env.clone(); + for v in &td.vars { + env.rigid_vars.insert(v.clone()); + } for c in &td.ctors { for f in &c.fields { - check_type_well_formed(f, env)?; + check_type_well_formed(f, &env)?; } } Ok(()) @@ -678,9 +701,27 @@ fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> { fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> { match t { - Type::Con { name } => { + Type::Con { name, args } => { let is_primitive = matches!(name.as_str(), "Int" | "Bool" | "Unit" | "Str"); - if is_primitive || env.types.contains_key(name) { + if is_primitive { + if !args.is_empty() { + return Err(CheckError::UnknownType(format!( + "{name} (primitive does not take type args)" + ))); + } + return Ok(()); + } + if let Some(td) = env.types.get(name) { + if td.vars.len() != args.len() { + return Err(CheckError::UnknownType(format!( + "{name} expects {} type arg(s), got {}", + td.vars.len(), + args.len() + ))); + } + for a in args { + check_type_well_formed(a, env)?; + } Ok(()) } else { Err(CheckError::UnknownType(name.clone())) @@ -694,7 +735,8 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> { } Type::Var { name } => { // Rigid var: legal iff it is in scope. Used inside a forall - // body when checking a polymorphic def. + // body when checking a polymorphic def, or inside a + // parameterised ADT's ctor fields. if env.rigid_vars.contains(name) { Ok(()) } else { @@ -746,6 +788,15 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { env.rigid_vars.insert(v.clone()); } + // Iter 13a: validate the declared parameter and return types + // against the type environment. Catches misuses like + // `Box` (arity mismatch on a parameterised ADT) before + // they leak into the body and produce confusing downstream errors. + for p in ¶m_tys { + check_type_well_formed(p, &env)?; + } + check_type_well_formed(&ret_ty, &env)?; + let mut locals = IndexMap::new(); for (n, t) in f.params.iter().zip(param_tys.iter()) { locals.insert(n.clone(), t.clone()); @@ -948,12 +999,27 @@ fn synth( got: args.len(), }); } + // Iter 13a: parameterised ADT — instantiate the type's vars + // with fresh metavars, substitute them through every ctor + // field type, and let the field types' metavars be solved by + // unifying against the actual arg types. The result type + // carries the same metavars as type-args, so the surrounding + // context can pin them down. + let mut mapping: BTreeMap = BTreeMap::new(); + let mut type_args: Vec = Vec::with_capacity(td.vars.len()); + for v in &td.vars { + let m = Subst::fresh(counter); + mapping.insert(v.clone(), m.clone()); + type_args.push(m); + } for (a, exp) in args.iter().zip(cdef.fields.iter()) { + let exp_inst = substitute_rigids(exp, &mapping); let actual = synth(a, env, locals, effects, in_def, subst, counter)?; - unify(exp, &actual, subst)?; + unify(&exp_inst, &actual, subst)?; } Ok(Type::Con { name: type_name.clone(), + args: type_args, }) } Term::Match { scrutinee, arms } => { @@ -1008,7 +1074,7 @@ fn synth( if !has_open_arm { match &s_ty { - Type::Con { name } if env.types.contains_key(name) => { + Type::Con { name, .. } if env.types.contains_key(name) => { let td = &env.types[name]; let missing: Vec = td .ctors @@ -1117,16 +1183,18 @@ fn type_check_pattern( .ctor_index .get(ctor) .ok_or_else(|| CheckError::UnknownCtorInPattern(ctor.clone()))?; - // expected must be this ADT. - match expected { - Type::Con { name } if name == &cref.type_name => {} + // expected must be this ADT. For parameterised ADTs, capture + // the type-args so we can substitute them into the cdef's + // field types when binding sub-patterns. + let scrutinee_args: Vec = match expected { + Type::Con { name, args } if name == &cref.type_name => args.clone(), _ => { return Err(CheckError::PatternTypeMismatch { ctor: ctor.clone(), ty: ailang_core::pretty::type_to_string(expected), }); } - } + }; let td = &env.types[&cref.type_name]; let cdef = td .ctors @@ -1141,9 +1209,20 @@ fn type_check_pattern( got: fields.len(), }); } + // Iter 13a: substitute the scrutinee's concrete type-args + // into each cdef field type (e.g. `Cons(a, List a)` checked + // against a `List Int` scrutinee yields field types + // `Int, List Int`). + let mapping: BTreeMap = td + .vars + .iter() + .cloned() + .zip(scrutinee_args) + .collect(); let mut out = Vec::new(); for (sub, sub_ty) in fields.iter().zip(cdef.fields.iter()) { - out.extend(type_check_pattern(sub, sub_ty, env)?); + let sub_ty_inst = substitute_rigids(sub_ty, &mapping); + out.extend(type_check_pattern(sub, &sub_ty_inst, env)?); } Ok(out) } @@ -1332,6 +1411,7 @@ mod tests { defs: vec![ Def::Type(TypeDef { name: "Maybe".into(), + vars: vec![], ctors: vec![ Ctor { name: "None".into(), fields: vec![] }, Ctor { @@ -1344,7 +1424,7 @@ mod tests { fn_def( "f", Type::Fn { - params: vec![Type::Con { name: "Maybe".into() }], + params: vec![Type::Con { name: "Maybe".into(), args: vec![] }], ret: Box::new(Type::int()), effects: vec![], }, @@ -1379,6 +1459,7 @@ mod tests { defs: vec![ Def::Type(TypeDef { name: "Maybe".into(), + vars: vec![], ctors: vec![ Ctor { name: "None".into(), fields: vec![] }, Ctor { @@ -1391,7 +1472,7 @@ mod tests { fn_def( "f", Type::Fn { - params: vec![Type::Con { name: "Maybe".into() }], + params: vec![Type::Con { name: "Maybe".into(), args: vec![] }], ret: Box::new(Type::int()), effects: vec![], }, @@ -1646,6 +1727,167 @@ mod tests { check(&m).expect("apply instantiation should typecheck"); } + /// Iter 13a: parameterised ADT — `type Box[a] = MkBox(a)` is well- + /// formed and `MkBox(42)` typechecks at result type `Box`. + #[test] + fn parameterised_adt_ctor_at_int() { + let box_def = Def::Type(TypeDef { + name: "Box".into(), + vars: vec!["a".into()], + ctors: vec![Ctor { + name: "MkBox".into(), + fields: vec![Type::Var { name: "a".into() }], + }], + doc: None, + }); + // fn make :: () -> Box = MkBox(42) + let make = fn_def( + "make", + Type::Fn { + params: vec![], + ret: Box::new(Type::Con { + name: "Box".into(), + args: vec![Type::int()], + }), + effects: vec![], + }, + vec![], + Term::Ctor { + type_name: "Box".into(), + ctor: "MkBox".into(), + args: vec![Term::Lit { lit: Literal::Int { value: 42 } }], + }, + ); + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![box_def, make], + }; + check(&m).expect("Box ctor should typecheck"); + } + + /// Iter 13a: ctor field type substitution and match-arm bindings. + /// `unbox :: forall a. (Box) -> a` extracts the wrapped value. + #[test] + fn parameterised_adt_polymorphic_unbox() { + let box_def = Def::Type(TypeDef { + name: "Box".into(), + vars: vec!["a".into()], + ctors: vec![Ctor { + name: "MkBox".into(), + fields: vec![Type::Var { name: "a".into() }], + }], + doc: None, + }); + let unbox = Def::Fn(FnDef { + name: "unbox".into(), + ty: Type::Forall { + vars: vec!["a".into()], + body: Box::new(Type::Fn { + params: vec![Type::Con { + name: "Box".into(), + args: vec![Type::Var { name: "a".into() }], + }], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + }), + }, + params: vec!["b".into()], + body: Term::Match { + scrutinee: Box::new(Term::Var { name: "b".into() }), + arms: vec![Arm { + pat: Pattern::Ctor { + ctor: "MkBox".into(), + fields: vec![Pattern::Var { name: "x".into() }], + }, + body: Term::Var { name: "x".into() }, + }], + }, + doc: None, + }); + // Use unbox at Int and at Bool — both must succeed and not + // cross-contaminate the polymorphic variable. + let use_int = fn_def( + "ui", + Type::Fn { + params: vec![], + ret: Box::new(Type::int()), + effects: vec![], + }, + vec![], + Term::App { + callee: Box::new(Term::Var { name: "unbox".into() }), + args: vec![Term::Ctor { + type_name: "Box".into(), + ctor: "MkBox".into(), + args: vec![Term::Lit { lit: Literal::Int { value: 7 } }], + }], + }, + ); + let use_bool = fn_def( + "ub", + Type::Fn { + params: vec![], + ret: Box::new(Type::bool_()), + effects: vec![], + }, + vec![], + Term::App { + callee: Box::new(Term::Var { name: "unbox".into() }), + args: vec![Term::Ctor { + type_name: "Box".into(), + ctor: "MkBox".into(), + args: vec![Term::Lit { lit: Literal::Bool { value: true } }], + }], + }, + ); + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![box_def, unbox, use_int, use_bool], + }; + check(&m).expect("polymorphic Box should typecheck at both instantiations"); + } + + /// Iter 13a: parameterised-ADT arity is enforced. `Box` (1 var) + /// used as `Box` must error. + #[test] + fn parameterised_adt_arity_is_enforced() { + let box_def = Def::Type(TypeDef { + name: "Box".into(), + vars: vec!["a".into()], + ctors: vec![Ctor { + name: "MkBox".into(), + fields: vec![Type::Var { name: "a".into() }], + }], + doc: None, + }); + let bad = fn_def( + "bad", + Type::Fn { + params: vec![Type::Con { + name: "Box".into(), + args: vec![Type::int(), Type::bool_()], + }], + ret: Box::new(Type::int()), + effects: vec![], + }, + vec!["b"], + Term::Lit { lit: Literal::Int { value: 0 } }, + ); + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![box_def, bad], + }; + let err = check(&m).unwrap_err(); + let msg = format!("{err}"); + assert!(msg.contains("expects 1 type arg"), "got: {msg}"); + } + /// Iter 10: `seq` requires lhs to be Unit. A non-Unit lhs is a /// type error — the value of lhs gets discarded so a useful (non- /// Unit) value would silently vanish. diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index f5bb55b..bf4347a 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -217,7 +217,7 @@ fn main_is_void(t: &Type) -> bool { match t { Type::Fn { params, ret, .. } => { params.is_empty() - && matches!(ret.as_ref(), Type::Con { name } if name == "Unit") + && matches!(ret.as_ref(), Type::Con { name, .. } if name == "Unit") } _ => false, } @@ -1881,6 +1881,7 @@ impl<'a> Emitter<'a> { }), Term::Ctor { type_name, .. } => Ok(Type::Con { name: type_name.clone(), + args: vec![], }), Term::Match { arms, .. } => { if let Some(first) = arms.first() { @@ -1898,7 +1899,7 @@ impl<'a> Emitter<'a> { fn llvm_type(t: &Type) -> Result { match t { - Type::Con { name } => match name.as_str() { + Type::Con { name, .. } => match name.as_str() { "Int" => Ok("i64".into()), "Bool" => Ok("i1".into()), "Unit" => Ok("i8".into()), @@ -2031,7 +2032,15 @@ fn unify_for_subst( subst.insert(name.clone(), arg.clone()); Ok(()) } - (Type::Con { name: pn }, Type::Con { name: an }) if pn == an => Ok(()), + ( + Type::Con { name: pn, args: pa }, + Type::Con { name: an, args: aa }, + ) if pn == an && pa.len() == aa.len() => { + for (p, a) in pa.iter().zip(aa.iter()) { + unify_for_subst(p, a, vars, subst)?; + } + Ok(()) + } ( Type::Fn { params: pp, ret: pr, .. }, Type::Fn { params: ap, ret: ar, .. }, @@ -2061,7 +2070,10 @@ fn unify_for_subst( fn apply_subst_to_type(t: &Type, subst: &BTreeMap) -> Type { match t { Type::Var { name } => subst.get(name).cloned().unwrap_or_else(|| t.clone()), - Type::Con { .. } => t.clone(), + Type::Con { name, args } => Type::Con { + name: name.clone(), + args: args.iter().map(|a| apply_subst_to_type(a, subst)).collect(), + }, Type::Fn { params, ret, effects } => Type::Fn { params: params.iter().map(|p| apply_subst_to_type(p, subst)).collect(), ret: Box::new(apply_subst_to_type(ret, subst)), @@ -2159,13 +2171,27 @@ fn descriptor_for_subst(vars: &[String], subst: &BTreeMap) -> Stri /// the MVP are non-recursive at the type level). fn type_descriptor(t: &Type) -> String { match t { - Type::Con { name } => match name.as_str() { - "Int" => "I".into(), - "Bool" => "B".into(), - "Unit" => "U".into(), - "Str" => "S".into(), - other => format!("F{other}"), - }, + Type::Con { name, args } => { + let head = match name.as_str() { + "Int" => "I".into(), + "Bool" => "B".into(), + "Unit" => "U".into(), + "Str" => "S".into(), + other => format!("F{other}"), + }; + if args.is_empty() { + head + } else { + // Iter 13a: parameterised ADTs get their type-arg + // descriptors appended, e.g. `FBox` of `Int` → `FBox_I`. + let mut s = head; + for a in args { + s.push('_'); + s.push_str(&type_descriptor(a)); + } + s + } + } Type::Fn { params, ret, .. } => { let mut s = String::from("Fn"); for p in params { diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 0017ad6..6e4b20c 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -55,6 +55,12 @@ pub fn def_kind(def: &Def) -> &'static str { #[derive(Debug, Clone, Serialize, Deserialize)] pub struct TypeDef { pub name: String, + /// Type parameters (Iter 13a). A monomorphic ADT has `vars` empty + /// and is serialized identically to the pre-13a schema (the field is + /// skipped when empty), preserving the canonical-JSON hash of every + /// existing module on disk. + #[serde(default, skip_serializing_if = "Vec::is_empty")] + pub vars: Vec, pub ctors: Vec, #[serde(default, skip_serializing_if = "Option::is_none")] pub doc: Option, @@ -189,6 +195,12 @@ pub enum Literal { pub enum Type { Con { name: String, + /// Type arguments (Iter 13a). For pre-13a uses (`Int`, `Bool`, + /// non-parameterised user ADTs) this stays empty and is skipped + /// during serialization, so the canonical-JSON hash of every + /// pre-existing module remains bit-identical. + #[serde(default, skip_serializing_if = "Vec::is_empty")] + args: Vec, }, Fn { params: Vec, @@ -207,23 +219,26 @@ pub enum Type { impl Type { pub fn int() -> Type { - Type::Con { name: "Int".into() } + Type::Con { name: "Int".into(), args: vec![] } } pub fn bool_() -> Type { - Type::Con { name: "Bool".into() } + Type::Con { name: "Bool".into(), args: vec![] } } pub fn unit() -> Type { - Type::Con { name: "Unit".into() } + Type::Con { name: "Unit".into(), args: vec![] } } pub fn str_() -> Type { - Type::Con { name: "Str".into() } + Type::Con { name: "Str".into(), args: vec![] } } } impl PartialEq for Type { fn eq(&self, other: &Self) -> bool { match (self, other) { - (Type::Con { name: a }, Type::Con { name: b }) => a == b, + ( + Type::Con { name: a, args: aa }, + Type::Con { name: b, args: ba }, + ) => a == b && aa == ba, ( Type::Fn { params: ap, ret: ar, effects: ae }, Type::Fn { params: bp, ret: br, effects: be }, diff --git a/crates/ailang-core/src/hash.rs b/crates/ailang-core/src/hash.rs index 9bf047e..06e5342 100644 --- a/crates/ailang-core/src/hash.rs +++ b/crates/ailang-core/src/hash.rs @@ -59,4 +59,29 @@ mod tests { let h2 = def_hash(&def); assert_ne!(h1, h2); } + + /// Iter 13a regression: adding `vars` to TypeDef and `args` to + /// `Type::Con` must NOT change canonical-JSON hashes of any pre-13a + /// definition. Recorded hashes were captured from on-disk modules + /// before the schema extension; if this fires, a + /// `skip_serializing_if` is missing or wrong. We deserialise the + /// real example modules from disk to avoid drift between the test + /// and the source-of-truth JSON. + #[test] + fn iter13a_schema_extension_preserves_pre_13a_hashes() { + let manifest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let examples = manifest_dir.join("../../examples"); + + let sum_src = std::fs::read(examples.join("sum.ail.json")) + .expect("examples/sum.ail.json present"); + let sum_mod: crate::ast::Module = serde_json::from_slice(&sum_src).unwrap(); + let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap(); + assert_eq!(def_hash(sum_def), "db33f57cb329935e"); + + let list_src = std::fs::read(examples.join("list.ail.json")) + .expect("examples/list.ail.json present"); + let list_mod: crate::ast::Module = serde_json::from_slice(&list_src).unwrap(); + let int_list_def = list_mod.defs.iter().find(|d| d.name() == "IntList").unwrap(); + assert_eq!(def_hash(int_list_def), "b082192bd0c99202"); + } } diff --git a/crates/ailang-core/src/pretty.rs b/crates/ailang-core/src/pretty.rs index ed7ad77..379c257 100644 --- a/crates/ailang-core/src/pretty.rs +++ b/crates/ailang-core/src/pretty.rs @@ -61,7 +61,12 @@ pub fn manifest(m: &Module) -> String { }) .collect::>() .join(" | "); - ("type", ctors) + let body = if t.vars.is_empty() { + ctors + } else { + format!("forall {}. {}", t.vars.join(" "), ctors) + }; + ("type", body) } }; writeln!( @@ -110,7 +115,17 @@ fn def_block(def: &Def, indent: usize) -> String { s } Def::Type(t) => { - let mut s = format!("{pad}(type {name}\n", pad = pad, name = t.name); + let header = if t.vars.is_empty() { + format!("{pad}(type {name}\n", pad = pad, name = t.name) + } else { + format!( + "{pad}(type {name} [{vars}]\n", + pad = pad, + name = t.name, + vars = t.vars.join(" "), + ) + }; + let mut s = header; let inner = " ".repeat(indent + 2); for ctor in &t.ctors { if ctor.fields.is_empty() { @@ -327,7 +342,18 @@ fn lit_to_string(l: &Literal) -> String { pub fn type_to_string(t: &Type) -> String { match t { - Type::Con { name } => name.clone(), + Type::Con { name, args } => { + if args.is_empty() { + name.clone() + } else { + let xs = args + .iter() + .map(type_to_string) + .collect::>() + .join(", "); + format!("{name}<{xs}>") + } + } Type::Var { name } => name.clone(), Type::Fn { params, ret, effects } => { let p = params