diff --git a/docs/internal/SCOREBOARD.md b/docs/internal/SCOREBOARD.md index 305cfcc0..274b460f 100644 --- a/docs/internal/SCOREBOARD.md +++ b/docs/internal/SCOREBOARD.md @@ -29,7 +29,7 @@ compaction, above it is not. | surface AST | 2,125 | 1,502 | 363 | 205 | 0.14 | | syntax codecs | none | none | 2,996 | 2,456 | n/a | | lint | none | none | 1,190 | 866 | n/a | -| checker | 12,726 | 10,049 | 4,239 | 3,390 | 0.34 | +| checker | 12,789 | 10,093 | 4,239 | 3,390 | 0.34 | What each row counts: diff --git a/docs/src/stdlib/data-vec.md b/docs/src/stdlib/data-vec.md index fd27eaf6..1e4ebf6b 100644 --- a/docs/src/stdlib/data-vec.md +++ b/docs/src/stdlib/data-vec.md @@ -8,6 +8,8 @@ Fixed-length vectors indexed by a `Nat` dimension. - `vempty` and `vsingle` pin a literal length (`0`, `1`). - `vmap` preserves the length (`n` appears on both sides). - `vzip` requires equal lengths (both `n`); a length clash is a compile error that names both lengths. +A list **literal** may be passed where a `Vec` is expected: `use_vec([1, 2, 3])`, with the literal's length fixing the `Vec`'s size. However, a list value can't be passed here as it has dynamic length: binding `let l = [1, 2, 3]` and then calling `use_vec(l)` is a type error. + Two operations are deliberately absent because their result length is not expressible under equality-only unification: a length-changing `vcons : (a, Vec(a, n)) -> Vec(a, n + 1)` and an append `(Vec(a, n), Vec(a, m)) -> Vec(a, n + m)`. That is the declined line; writing either `n + 1` produces a pointed rejection rather than a bare parse error. `vhead` accepts any length, so it cannot statically forbid the empty vector (ruling it out needs `n = m + 1`, again arithmetic). On an empty vector it raises `Fail` rather than guarding with an `Option`; this is the head-on-empty consequence of the declined line. diff --git a/lib/std/Data/Vec.pr b/lib/std/Data/Vec.pr index 594daa8b..355db5be 100644 --- a/lib/std/Data/Vec.pr +++ b/lib/std/Data/Vec.pr @@ -11,6 +11,11 @@ -- - `vzip` requires equal lengths (both `n`); a length clash is a compile -- error that names both lengths. -- +-- A list **literal** may be passed where a `Vec` is expected: `use_vec([1, 2, 3])`, +-- with the literal's length fixing the `Vec`'s size. However, a list value can't +-- be passed here as it has dynamic length: binding `let l = [1, 2, 3]` and then +-- calling `use_vec(l)` is a type error. +-- -- Two operations are deliberately absent because their result length is not -- expressible under equality-only unification: a length-changing -- `vcons : (a, Vec(a, n)) -> Vec(a, n + 1)` and an append diff --git a/src/core/elaborate/expr.rs b/src/core/elaborate/expr.rs index 211f7e9b..c76722a1 100644 --- a/src/core/elaborate/expr.rs +++ b/src/core/elaborate/expr.rs @@ -926,7 +926,35 @@ impl Elab<'_> { Box::new(Comp::Bind(Box::new(acc), vrest.into(), Box::new(cons))), ); } - acc + // A literal checked against a shape-indexed type is that type's own + // constructor applied to the element chain above. Checking recorded + // which one, since the expected type is not visible here. + match self.hir.res(e.id) { + Some(NodeRes::ShapeIndexed(ctor)) => { + let ctor = *ctor; + let vlist = self.fresh(); + let tag = self + .ctors + .get(ctor.as_str()) + .ok_or_else(|| { + Error::InternalInvariant(format!( + "no tag for constructor `{}`", + ctor.as_str() + )) + })? + .tag; + Comp::Bind( + Box::new(acc), + vlist.clone().into(), + Box::new(Comp::Return(Value::Ctor( + ctor, + tag, + vec![Value::Var(vlist.into())], + ))), + ) + } + _ => acc, + } } Expr::FieldAccess(recv, field) => self.field_access(e.id, recv, field, locals)?, Expr::RecordCreate(ctor_name, field_exprs) => { diff --git a/src/driver/dump.rs b/src/driver/dump.rs index 8e69a3fc..4aef13cc 100644 --- a/src/driver/dump.rs +++ b/src/driver/dump.rs @@ -1316,6 +1316,10 @@ enum HirRes { }, #[serde(rename = "unboxed")] Unboxed { index: usize, arity: usize }, + // A list literal that constructs a shape-indexed type: the constructor + // elaboration wraps its element chain in. + #[serde(rename = "shape_indexed")] + ShapeIndexed { ctor: String }, #[serde(rename = "paths")] Paths { chains: Vec> }, } @@ -1414,6 +1418,9 @@ fn render_res(res: &NodeRes) -> HirRes { index: *index, arity: *arity, }, + NodeRes::ShapeIndexed(ctor) => HirRes::ShapeIndexed { + ctor: ctor.as_str().to_string(), + }, NodeRes::Paths(chains) => HirRes::Paths { chains: chains .iter() diff --git a/src/hir/lint.rs b/src/hir/lint.rs index 8a381ef5..29358ad1 100644 --- a/src/hir/lint.rs +++ b/src/hir/lint.rs @@ -121,7 +121,7 @@ pub fn lint_hir(hir: &CheckedHir<'_>) -> Vec { }; for (i, fact) in hir.facts.res.iter().enumerate() { match fact { - None => {} + None | Some(NodeRes::ShapeIndexed(_)) => {} Some(NodeRes::Field(field)) => { if let Some(msg) = check_step(field) { push(&mut out, i, msg); diff --git a/src/hir/mod.rs b/src/hir/mod.rs index 9db665c3..79df5f7a 100644 --- a/src/hir/mod.rs +++ b/src/hir/mod.rs @@ -41,6 +41,10 @@ pub enum NodeRes { /// A record update path `e { p.q = v }`: one rebuild chain per path, one /// [`FieldRef`] step per path segment. Paths(Vec>), + /// A list literal checked against a shape-indexed expected type: the constructor + /// to wrap the literal's element chain in, so `[1, 2, 3]` in a `Vec(Int, 3)` + /// position elaborates to that type's own constructor applied to the list. + ShapeIndexed(Sym), } /// Operation-local residual evidence for one checked handler expression. @@ -332,6 +336,7 @@ impl NodeFacts { pub(crate) fn from_tables( field_res: BTreeMap, unboxed_field: BTreeMap, + shape_indexed: BTreeMap, path_res: PathRes, fixed: BTreeMap, span_types: BTreeMap, @@ -355,6 +360,9 @@ impl NodeFacts { for (id, (idx, arity)) in unboxed_field { place(&mut res, id, NodeRes::UnboxedField(idx, arity)); } + for (id, ctor) in shape_indexed { + place(&mut res, id, NodeRes::ShapeIndexed(ctor)); + } for (id, chains) in path_res { place(&mut res, id, NodeRes::Paths(chains)); } diff --git a/src/repl/mod.rs b/src/repl/mod.rs index 2aedbfb1..db8db2ba 100644 --- a/src/repl/mod.rs +++ b/src/repl/mod.rs @@ -1730,6 +1730,7 @@ mod tests { BTreeMap::new(), BTreeMap::new(), BTreeMap::new(), + BTreeMap::new(), BTreeSet::new(), BTreeMap::new(), BTreeSet::new(), diff --git a/src/tc/infer.rs b/src/tc/infer.rs index 39340577..79f58401 100644 --- a/src/tc/infer.rs +++ b/src/tc/infer.rs @@ -16,9 +16,9 @@ use crate::names; use crate::sym::Sym; use crate::syntax::ast::{self, Core, Expr, Grade, HandlerArm, HandlerMode, NodeId, S}; use crate::syntax::desugar::referenced_names; -use crate::types::ty::{EffRow, Label, Type, LIST, NUM_CLASS, SHOW_CLASS}; +use crate::types::ty::{EffRow, Kind, Label, Type, LIST, NUM_CLASS, SHOW_CLASS}; use crate::types::EffOpInfo; -use crate::wired::Indexable; +use crate::wired::{self, Indexable}; // Red zone / segment size for the checker's per-node recursion, matching the // desugar and typed-Core-builder guards. @@ -273,6 +273,30 @@ impl Tc<'_> { handled } + /// The constructor a list literal builds when the expected type is the standard + /// library's vector, as `(element position, dimension position, constructor)`, or + /// `None` for any other type: naming `Data.Vec.Vec` here is a stepping stone. + fn shape_indexed_ctor(&self, ty: &Type) -> Option<(usize, usize, Sym)> { + let Type::Con(head, args) = ty else { + return None; + }; + if head.as_str() != wired::TY_VEC || args.len() != 2 { + return None; + } + // The declaration is known, so this is a sanity check rather than a way of + // recognising `Vec`: one constructor, and the positions read from the kinds + // rather than assumed, so a re-declaration retires the form rather than + // misreading it. + let info = self.data.get(head.as_str())?; + if info.ctors.len() != 1 { + return None; + } + let kinds = info.param_kinds(); + let elem_i = kinds.iter().position(|k| *k == Kind::Type)?; + let nat_i = kinds.iter().position(|k| *k == Kind::Nat)?; + Some((elem_i, nat_i, Sym::from(info.ctors[0].as_str()))) + } + fn check(&mut self, env: &Env, e: &S>, ty: &Type) -> Result<(), TypeError> { self.with_tooltip_row(e.id, e.span, |tc| tc.check_node(env, e, ty)) } @@ -313,6 +337,34 @@ impl Tc<'_> { ) -> Result<(), TypeError> { let span = e.span; let id = e.id; + // A list literal against `Vec` takes its length from the literal's own element + // count, so `[1, 2, 3]` fills a `Vec(Int, 3)` position with no construction + // function in sight. Decided here rather than in an arm below, because the + // expected type is what decides it and a guard cannot bind what an arm needs. + if let (Expr::List(elems), Type::Con(_, args), Some((elem_i, nat_i, ctor))) = + (&e.node, ty, self.shape_indexed_ctor(ty)) + { + let elem_ty = self.apply(&args[elem_i]); + for elem in elems { + self.check(env, elem, &elem_ty)?; + } + // The dimension is unified rather than merely compared, so a literal against + // a variable length solves it, a clash names both lengths, and a rigid length + // is refused rather than forced. + let want = self.apply(&args[nat_i]); + let got = Type::Nat(u64::try_from(elems.len()).unwrap_or(u64::MAX)); + self.subtype(&got, &want).map_err(|e| { + e.or(TypeError::TypeMismatch { + span, + expected: want.show(), + found: got.show(), + }) + })?; + // Elaboration cannot see the expected type, so the constructor it wraps the + // element chain in is recorded against this node. + self.shape_indexed.insert(id, ctor); + return Ok(()); + } match (&e.node, ty) { (Expr::Hole(name), _) => { self.record_hole(env, name, span, ty.clone()); diff --git a/src/tc/mod.rs b/src/tc/mod.rs index 58427375..e733b6d1 100644 --- a/src/tc/mod.rs +++ b/src/tc/mod.rs @@ -365,6 +365,7 @@ fn check_seeded_mode( } let field_res; let unboxed_field; + let shape_indexed; let path_res; let fixed; let span_types; @@ -386,6 +387,7 @@ fn check_seeded_mode( eff_ops: &eff_ops, field_res: BTreeMap::new(), unboxed_field: BTreeMap::new(), + shape_indexed: BTreeMap::new(), path_res: PathRes::new(), fixed: BTreeMap::new(), span_types: BTreeMap::new(), @@ -508,6 +510,7 @@ fn check_seeded_mode( tc.check_or_null_sites()?; field_res = tc.field_res; unboxed_field = tc.unboxed_field; + shape_indexed = tc.shape_indexed; path_res = tc.path_res; fixed = tc.fixed; span_types = tc.span_types; @@ -543,6 +546,7 @@ fn check_seeded_mode( facts: NodeFacts::from_tables( field_res, unboxed_field, + shape_indexed, path_res, fixed, span_types, @@ -704,6 +708,7 @@ fn infer_expr_full( eff_ops: &checked.defs.eff_ops, field_res: BTreeMap::new(), unboxed_field: BTreeMap::new(), + shape_indexed: BTreeMap::new(), path_res: PathRes::new(), fixed: BTreeMap::new(), span_types: BTreeMap::new(), @@ -757,6 +762,7 @@ fn infer_expr_full( let facts = NodeFacts::from_tables( tc.field_res, tc.unboxed_field, + tc.shape_indexed, tc.path_res, tc.fixed, tc.span_types, @@ -791,6 +797,7 @@ fn query_tc(seed: &TypecheckSeed) -> Tc<'_> { eff_ops: seed.effect_operations(), field_res: BTreeMap::new(), unboxed_field: BTreeMap::new(), + shape_indexed: BTreeMap::new(), path_res: PathRes::new(), fixed: BTreeMap::new(), span_types: BTreeMap::new(), diff --git a/src/tc/session.rs b/src/tc/session.rs index b85413f3..df15a7df 100644 --- a/src/tc/session.rs +++ b/src/tc/session.rs @@ -134,6 +134,9 @@ pub(super) struct Tc<'a> { pub(super) eff_ops: &'a BTreeMap, pub(super) field_res: BTreeMap, pub(super) unboxed_field: BTreeMap, + /// A list literal checked against a shape-indexed expected type, keyed by the + /// literal's node id: the constructor elaboration wraps its element chain in. + pub(super) shape_indexed: BTreeMap, pub(super) path_res: PathRes, pub(super) fixed: BTreeMap, pub(super) span_types: BTreeMap, diff --git a/src/tc/subsume.rs b/src/tc/subsume.rs index dfcd3bc8..28807a15 100644 --- a/src/tc/subsume.rs +++ b/src/tc/subsume.rs @@ -892,6 +892,7 @@ mod tests { field_res: BTreeMap::new(), body_witness: BTreeMap::new(), unboxed_field: BTreeMap::new(), + shape_indexed: BTreeMap::new(), path_res: PathRes::new(), fixed: BTreeMap::new(), span_types: BTreeMap::new(), diff --git a/src/wired.rs b/src/wired.rs index fbc92ab2..db2f8496 100644 --- a/src/wired.rs +++ b/src/wired.rs @@ -19,6 +19,14 @@ use crate::types::Type; const TY_HASHMAP: &str = "HashMap"; const TY_TENSOR: &str = "Tensor"; +/// The standard library's fixed-length vector, `Data.Vec.Vec`. +/// +/// Matched on its qualified name where the containers above use a bare one: a user +/// may declare a `Vec` of their own, and the list-literal rule must not catch it. +/// Naming it here is a stepping stone — the intent is a conformance a type opts +/// into, with `Vec` as its first instance. +pub(crate) const TY_VEC: &str = "Data.Vec.Vec"; + /// A container the `e[k]` / `e[k] := v` index sugar supports. /// /// Classifying a receiver type once, here, is what lets the typing rule diff --git a/tests/frontend.rs b/tests/frontend.rs index 1ffd0321..4a7bcbdb 100644 --- a/tests/frontend.rs +++ b/tests/frontend.rs @@ -81,6 +81,8 @@ mod query; mod reflect; #[path = "language/rigid_sig_vars.rs"] mod rigid_sig_vars; +#[path = "language/shape_indexed_literal.rs"] +mod shape_indexed_literal; #[path = "language/skolem_escape.rs"] mod skolem_escape; #[path = "language/soundness.rs"] diff --git a/tests/language/shape_indexed_literal.rs b/tests/language/shape_indexed_literal.rs new file mode 100644 index 00000000..7a284a10 --- /dev/null +++ b/tests/language/shape_indexed_literal.rs @@ -0,0 +1,231 @@ +// A list literal constructs a shape-indexed type: its length comes from the +// literal's own element count, so `[1, 2, 3]` fills a `Vec(Int, 3)` position and a +// count that disagrees is refused naming both lengths. The runtime case below is a +// test rather than a probe because the property it exercises — that the literal +// builds the constructor the type declares — is what a checking-only change would +// get wrong. + +use prism::{check, interpret, with_prelude}; +use rstest::rstest; + +fn accepts(src: &str) { + let full = with_prelude(src); + check(&full).unwrap_or_else(|e| panic!("should type-check, got: {e}\n---\n{src}")); +} + +fn rejection(src: &str) -> String { + let full = with_prelude(src); + check(&full).expect_err("should be rejected").to_string() +} + +fn output(src: &str) -> String { + let full = with_prelude(src); + interpret(&full).expect("should run").term +} + +/// The literal spelling `n` elements, `[0, 1, ...]`. +fn literal_of(n: usize) -> String { + let elems: Vec = (0..n).map(|i| i.to_string()).collect(); + format!("[{}]", elems.join(", ")) +} + +/// A program that passes a literal of `n` elements where a length-`n` vector is +/// wanted, so the expected type is what gives the literal its length. +fn literal_at(n: usize) -> String { + format!( + r"import Data.Vec (..) + +fn takes(v : Vec(Int, {n})) : Int = 0 +fn use() : Int = takes({}) +", + literal_of(n) + ) +} + +// Every length is reached the same way, including the two the module's own +// constructors pin and the ones nothing could build before. +#[rstest] +fn a_literal_constructs_the_length_it_spells(#[values(0, 1, 2, 3, 12)] n: usize) { + accepts(&literal_at(n)); +} + +// The count is checked against the dimension, and the refusal names both so the +// reader is not left comparing two whole shape types. +#[test] +fn a_literal_of_the_wrong_length_is_refused_naming_both() { + let msg = rejection( + r"import Data.Vec (..) + +fn takes3(v : Vec(Int, 3)) : Int = 0 +fn use() : Int = takes3([1, 2]) +", + ); + assert!( + msg.contains("expected length 3") && msg.contains("got length 2"), + "a length clash should name both lengths, got: {msg}" + ); +} + +// A literal against a variable length is not a clash: the count solves the +// variable, which is what lets a caller pass a literal to a polymorphic +// function. +#[test] +fn a_variable_length_is_solved_from_the_count() { + accepts( + r"import Data.Vec (..) + +fn takes(v : Vec(Int, n)) : Int = 0 +fn use() : Int = takes([1, 2, 3]) +", + ); +} + +// A length the caller's own signature fixed is rigid, so a literal cannot decide +// it: the count is evidence about the literal, not about `n`. +#[test] +fn a_rigid_length_cannot_be_satisfied_by_a_literal() { + let msg = rejection( + r"import Data.Vec (..) + +fn f(v : Vec(Int, n)) : Vec(Int, n) = [1, 2, 3] +", + ); + assert!( + msg.contains("mismatch"), + "a literal against a rigid length should be refused, got: {msg}" + ); +} + +// The rule needs the expected type at the literal's own site, so a literal bound +// first is a `List` and stays one: inference gives `v` its type, not the position +// `v` later reaches. Pinned as a test so the limitation cannot drift unnoticed. +#[test] +fn a_literal_bound_before_its_position_is_inferred_as_a_list() { + let msg = rejection( + r"import Data.Vec (..) + +fn takes3(v : Vec(Int, 3)) : Int = 0 +fn use() : Int = + let v = [1, 2, 3] + takes3(v) +", + ); + assert!( + msg.contains("mismatch"), + "a let-bound literal should be inferred as a list, got: {msg}" + ); +} + +// The element lane is adopted through the rule exactly as it is through +// `List(T)`, so a vector of a fixed-width lane needs no per-element suffix. +#[test] +fn the_element_lane_is_adopted_through_the_rule() { + accepts( + r"import Data.Vec (..) + +fn takes(v : Vec(I64, 3)) : Int = 0 +fn use() : Int = takes([1, 2, 3]) +", + ); +} + +// The literal form admits a shape-indexed type where it is wanted and nowhere +// else: a list is still not a vector, and a vector is still not a list. +#[test] +fn a_list_is_still_refused_where_a_shape_indexed_type_is_wanted() { + let msg = rejection( + r"import Data.Vec (..) + +fn takes3(v : Vec(Int, 3)) : Int = 0 +fn use(xs : List(Int)) : Int = takes3(xs) +", + ); + assert!( + msg.contains("mismatch"), + "a list should not pass for a vector, got: {msg}" + ); +} + +#[test] +fn a_shape_indexed_value_is_still_refused_where_a_list_is_wanted() { + let msg = rejection( + r"import Data.Vec (..) + +fn wants(xs : List(Int)) : Int = 0 +fn use(v : Vec(Int, 3)) : Int = wants(v) +", + ); + assert!( + msg.contains("mismatch"), + "a vector should not pass for a list, got: {msg}" + ); +} + +// The runtime half, and the reason it is worth keeping. `vto_list` destructures +// the vector's own constructor to reach the list underneath, so it returns one +// only if the literal really built that constructor; a bare list would fail to +// match instead of quietly looking like the same value. +#[test] +fn a_literal_builds_the_constructor_the_type_declares() { + let prog = r"import Data.Vec (..) + +fn main() = + println(show(vto_list(([1, 2, 3] : Vec(Int, 3))))) + println(show(vto_list(([] : Vec(Int, 0))))) +"; + assert_eq!(output(prog), "[1, 2, 3]\n[]\n"); +} + +// The same at a named position, so the constructor is built for a value that +// travels through a declaration rather than only at the literal's own site. +#[test] +fn a_named_vector_carries_its_constructor() { + let prog = r"import Data.Vec (..) + +fn three() : Vec(Int, 3) = [1, 2, 3] + +fn main() = println(show(vto_list(three()))) +"; + assert_eq!(output(prog), "[1, 2, 3]\n"); +} + +// But the rule is about `Vec` and nothing else. A user's own `Grid(a, n : Nat)` has +// exactly the same shape, and its `Nat` is equally untied to the list — so offering +// it the form would promise a check that does not exist: `MkGrid` stays visible, so +// `MkGrid([1])` passes for a `Grid(Int, 3)` with or without the rule. `Vec` is the +// one type where the offer is worth making, because sealing its constructor is what +// makes the literal the only route and the count the only check. +#[test] +fn a_user_declared_type_is_not_offered_the_form() { + let msg = rejection( + r"type Grid(a, n : Nat) = MkGrid(List(a)) + +fn takes(v : Grid(Int, 3)) : Int = 0 +fn use() : Int = takes([1, 2, 3]) +", + ); + assert!( + msg.contains("mismatch"), + "a user's own type should not be offered the form, got: {msg}" + ); +} + +// But the field has to be a list of the element parameter itself, not a list of +// anything. Otherwise a declaration whose lone field is `List(Int)` under a phantom +// element parameter would let a literal of booleans check in a `Foo(Bool, n)` +// position, and elaboration would then build a value whose field holds integers — +// a representation the type does not describe. +#[test] +fn a_field_listing_something_other_than_the_element_is_not_shape_indexed() { + let msg = rejection( + r"type Foo(a, n : Nat) = MkFoo(List(Int)) + +fn takes(v : Foo(Bool, 3)) : Int = 0 +fn use() : Int = takes([true, false, true]) +", + ); + assert!( + msg.contains("mismatch"), + "a field listing another type should not make a type shape-indexed, got: {msg}" + ); +}