Compile-time typechecking - #209
Open
rTreutlein wants to merge 137 commits into
Open
Conversation
Collaborator
Author
|
Added since opening: Under it a plain The bundled libraries load clean under the flag (the genuinely Without the flag nothing changes; |
Collaborator
Author
|
Two additions since the last update: Erased nominal newtypes ( (: KB (Newtype Expression))
(: Proof (Newtype Expression))
(: rule-ev (-> KB Proof Evidence))declares distinct compile-time brands that are fully erased: no wrappers, no Soundness fixes from an external review ( The branch also merged current main (import overhaul, overapplication 🤖 Generated with Claude Code |
Collaborator
Author
|
Since the last update the branch went through a full line-by-line review plus Soundness. Eleven holes closed, found by new self-audit instruments: Determinism model. PeTTaChainer results. The typed chainer runs 15% faster than the Late knowledge. Several Suite is at 307 examples (87 expected-fail) plus the oracle matrices, ~2 🤖 Generated with Claude Code |
Imports used to resolve against a single global working_dir set once at startup, so a file imported from another directory could not find its own relative dependencies. load_metta_file now maintains a stack of working directories (pushed on entry, popped via setup_call_cleanup), making both MeTTa and Python imports resolve relative to the file that declares them. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
import! previously swallowed every failure via catch(_, fail), so a missing file, a syntax error in a dependency, or a failing Python module import all passed silently. Imports now resolve their target to a canonical path and throw existence_error when it is missing; errors from loading a dependency propagate wrapped with the offending filename. Since a throwing import! no longer fails into backtracking, library/2 now prefers the candidate whose source file actually exists instead of relying on backtracking across registered library paths. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Importing the same file twice into the same space re-asserted all of its clauses, and two files importing each other recursed until the stack blew. import! now tracks per-space load state keyed by the canonical file path: a loaded entry turns repeated imports into no-ops, a loading entry breaks cycles, and failed loads clear their entry so the source can be repaired and the import retried within the same session. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
git-import! piped clone and build output into discarded strings and never checked the exit status, so a failed clone or build step passed silently and left the import broken. Both steps now inherit the caller's stdio and throw process_error on a nonzero exit. The repository path is registered canonicalized and only once, also removing a stray debug print. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Definitions compile expression heads that are not registered functions into plain symbols, so a function imported or defined after its first use is silently never called by the already-compiled expressions. The translator now records atoms it compiles as symbol heads, and registering a function whose name was already compiled that way prints a warning telling the user to move the import or definition above the first use. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…cking attempt Salvaged from the abandoned compile-time-typechecking branch (a0e0746 + uncommitted fixes): 39 spec examples, the dispatch-matrix assertions, and the error-message catalog. AGENTS.md records the phase plan and the design rules learned from the failed attempt. test_typecheck.sh runs the spec as a progress meter (starts red by design); test.sh is untouched and stays green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… overloads, strict mode Phase 1 - type store: (: f ...) declarations are canonicalized into a dynamic declared_fn_type/4 / declared_value_type/2 store when atoms enter &self (add_sexp), removed with them, and forgotten by forget_symbol. Builtin operator types are seeded from lib/lib_builtin_types.metta at startup; caching is idempotent so imports do not duplicate. Phase 2 - monomorphic checking: call sites of declared functions check literal and known-typed arguments during translation and throw literal_type_mismatch / type_conflict at compile time. Clause bodies are checked against the declared output type. Fully resolved calls compile to plain direct calls with no runtime type goals. Phase 3 - polymorphism and partial application: one compatibility relation (type_unify/2) resolves type variables by unification on fresh copies from the store; (List T) element checking works on literals; partial(F, Bound) values get the remaining-arrow type. lib_roman.metta adopts the precise polymorphic annotations from a0e0746 (fold-nested uses the stronger (-> Expression $a Expression $a)). Phase 4 - overloads: if exactly one declaration statically survives, a direct call is compiled; otherwise a guarded disjunction that throws no_matching_overload when no branch applies. Overloaded functions filter on the output type at the call site since their clauses are not output-checked. Phase 5 - strict mode: --strict requires a declared type for every compiled function and rejects any residual runtime type goal at the point of emission. Design (per AGENTS.md): one type channel via attributed variables (tknown / treq at translation time, mreq for runtime constraints), every subexpression translated exactly once, and static failures thrown during translation. Residual runtime guards check bound values through the user-extensible get-type reflection, so runtime refinement types (examples/types_dependent.metta) keep working; guards emitted inside get-type extensions do not recurse. Expression- typed arguments stay unevaluated data unless they form a goal-free closure. Specialization still serves wildcard-typed higher-order args; arrow-typed ones compile to typed direct calls. Spec suite: 37/39 (remaining two are the phase-6 determinism specs). test.sh: green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Parse infix determinism arrows (A -[det]-> B, -[nondet]->, and their long forms) into the same canonical store with a det flag. Functions declared deterministic are validated at translation time: the clause body must be a provably deterministic expression (superpose/match/hyperpose and calls to nondet functions are rejected unless wrapped in once/collapse) and clause heads must not overlap. Conflicting determinism declarations across overloads throw conflicting_determinism_declarations. Spec suite: 39/39. test.sh: green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The feature is complete, so per the plan the examples_typecheck/ spec files move into examples/ and test_typecheck.sh is retired. test.sh gains the expected-fail harness (fail_*.metta must be rejected at compile time with a type/determinism error), --strict handling for strict_*/fail_strict_* files, and runs examples/type_dispatch_matrix.sh at the end. AGENTS.md now documents the implemented feature instead of the plan. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Benchmarking against the pre-typechecking baseline showed large runtime regressions in guard-dense code (fib 0.7s -> 13s): every guard paid for a setup_call_cleanup plus get-type reflection even when the value was a plain number, and eval-heavy interpreters (he_minimalmetta) paid full dispatch bookkeeping per runtime translation. - runtime_type_ok/2 and check_value/3 get primitive fast paths (Number/String/ Bool) ahead of the reflective and store-based checks. - type_guard/output_guard inline the primitive test into the compiled goal: (number(V) -> true ; typecheck_or_error(V, 'Number')), so hot loops only pay a native type test and the reflective path runs on failure only. - expression_arg_value only attempts the closure translation for underapplied calls to known functions, instead of speculatively translating (and discarding) every Expression-typed argument. - Single-declaration calls derive Expression-arg modes directly from the declaration instead of the positional nth0 scan; should_try_specialize walks the args pairwise. Best-of-3 vs baseline after this: fib +5%, tilepuzzle +1%, matespacefast +3%, he_minimalmetta ~+4%, holbenchmark +17% (synthetic guard-per-iteration loops); compile time itself is slightly faster than the old match-based typed dispatch. test.sh: green (184 OK incl. spec tests and dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The arrow-typed-argument exception to specialization was pinned by a matrix assertion inherited from the abandoned attempt, not by semantics. Typed resolved calls now go through the specializer like everything else, so typed HOFs get direct-dispatch bodies again; the matrix asserts the specialized call. To keep specialized instances guard-free and safe: - specialized clause copies bind their (more specific) parameter types for guard elimination but skip determinism/strict/output checks - they are instances of already-validated clauses, - bind_param_type descends into list patterns, typing element variables against the declared (List T) element type, - a typecheck error while re-translating a specialized instance aborts the specialization (falls back to the direct call) instead of aborting the load. test.sh: green (184 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…rict mode) While an undeclared function's clause is translated, its variable parameters carry fresh assumption type variables and the clause exposes a provisional (-> Assumed... Out) arrow to self-recursive calls; typed call sites in the body bind the assumptions by unification. Harvested types go into an internal inferred_fn_type/3 store (never into &self) and are used only to ADD knowledge: - guards on inferred-typed values disappear (untyped fib now compiles to the same guard-free clause as a fully annotated one; holbenchmark's loop guards are gone, returning it to baseline speed), - call sites of inferred functions get output-type knowledge and never throw at compile time - a static mismatch degrades to the runtime guard that the call would have had anyway, - strict mode accepts "declared or inferable", matching its error message. A parameter whose assumption sees conflicting uses is tainted and recorded as %Undefined%; clause joins widen position-wise; declarations supersede and forget_symbol clears inference. Also replaces the cross-call requirement store (treq) with per-call conflict detection: the old accumulation could mark a later branch's call dead based on a requirement from a sibling branch. Same-call conflicts (num-str $x $x) still compile to fail, preserving the collapse-to-() semantics. test.sh: green (184 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two codegen optimizations enabled by the type information: - Calls to the builtin arithmetic operators (+ - * / % min max) whose declaration resolves compile to native `Out is Expr` instead of a predicate call, constant-folded when both operands are literals (a fold that cannot evaluate, e.g. (/ 1 0), stays a runtime goal so the error surfaces at run time as before). - A reified comparison (< <= > >= == !=) whose result only feeds an if-condition compiles to the native comparison inside the if-then-else, skipping the true/false round-trip. Both apply only while the builtin's definition is untouched (guarded by a clause-count check), so MeTTa-level redefinitions of the operators keep working. Semantics are unchanged: the replaced predicates are themselves thin is/2 wrappers with identical error behavior. Untyped fib now compiles to the hand-written-Prolog form via inference + fusion. Best-of-3 wall time vs the pre-typechecking baseline: fib 0.73s -> 0.42s, fibadd 0.79s -> 0.40s, holbenchmark 2.27s -> 1.57s; tilepuzzle and matespacefast slightly faster. test.sh: green (184 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A call ($f ...) whose head variable has a known arrow type of matching arity now compiles to apply_fn1/2/3/N instead of reduce/2: call/N dispatch for function atoms and a direct construction for partial closures, skipping reduce's per-call fun/arity/operator bookkeeping. The last clause of each helper falls back to reduce, preserving its symbolic-data semantics for values that are not callable - including unbound heads used relationally (examples/invertfunction.metta runs functions backwards through such terms). Inference also learns arrow types from head use: applying an assumed parameter to N arguments binds its assumption to an N-ary arrow, so untyped higher-order functions get the fast path and arrow-typed closure knowledge too. Singleton expressions ($x) are excluded - they are data, not zero-arg applications. Argument values are checked against the arrow's argument types (same guard rules as declared calls) and the output type propagates to the call result. Best-of-3 wall vs pre-typechecking baseline: hyperpose_primes 2.41s -> 1.30s, holbenchmark 2.27s -> 1.60s. test.sh: green (184 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Functions declared -[det]-> (whose non-overlapping clauses and deterministic bodies are already validated) now compile with a cut after head matching. This guarantees choicepoint-free execution independent of what the clause indexer manages, which enables last-call optimization: deep deterministic recursion runs in constant memory. The new examples/determinism_lco.metta exercises a clause partition that no single-argument index can discriminate (pairwise non-overlapping on different positions). At 3M recursion depth: 0.28s / 22MB with the det declaration vs 0.60s / 285MB without - 2.1x faster and constant instead of linear stack. Also supports the juxtaposed infix arrow form (: f (A B -[det]-> C)) in addition to the chained form (A -[det]-> B -[det]-> C); previously the juxtaposed spelling silently parsed as a value declaration. test.sh: green (185 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Static type/determinism errors now print the file, line, and offending MeTTa
form before the error itself:
Type error at examples/foo.metta:6 in:
(sid 7)
ERROR: ... Type mismatch: got 7 but expected 'String'
The form reader already tracked line numbers; they now travel with each parsed
form, and load_metta_file keeps the current filename (nested imports restore
the outer one).
A type declaration that arrives after its function's clauses were compiled was
previously a silent no-op (declarations only affect later forms); it now emits
a warning saying exactly that.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ed closures - (let $x Val In) / chain: the bound variable now carries the value's known type, so guards on later uses of $x disappear. - map-atom / filter-atom / foldl-atom type their element variable from the list argument (known (List T) or a homogeneous literal list), eliminating guards inside the lambda body. - Closures over inferred (undeclared) functions count as positive evidence at arrow-typed call sites: a partial over an inferred function resolves the polymorphic arrow instead of staying unknown. Inferred candidates can only confirm, never produce a mismatch. - same_call_var_conflict now also applies to variables with known types: one value can never satisfy two incompatible types in the same call, so such calls still compile to fail (preserving the collapse-to-() semantics even now that HOF element variables are typed). test.sh: green (185 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
examples/type_inference.metta exercises the inference contract end to end: a fully inferable function, a tainted (heterogeneously used) parameter that still compiles and checks at runtime, arrow inference from head use, and a statically mismatching call against an inferred type that fails at run time rather than compile time. The dispatch matrix now asserts the flagship codegen claims so review churn cannot silently regress them: untyped fib compiles with no typecheck goals, a fused native comparison (A<2) and native arithmetic (B is D+F); the inference example compiles fi to fused arithmetic and dispatches the untyped higher-order body through apply_fn1. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Annotate the builtins with polymorphic arguments and concrete outputs: reflection predicates (is-var/is-ground/is-expr/is-space, is-member, =alpha/=@=/=?) as Bool, size-atom/length as Number, repr/repra as String, println! as Bool, and the 3-argument random generators as Number. Since these are seeded at startup, every program gets the output knowledge (and the guard elimination that follows) for free. test.sh: green (185 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
User-facing documentation for compile-time typechecking: annotations and error reporting, the performance story (types make code faster via fused codegen), inference semantics (knowledge only, never rejects), strict mode's no-runtime-checks guarantee, determinism arrows, and the known caveats (declaration order, Expression argument semantics, eval-per-iteration). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Space reads were the remaining place where types went unknown: a match pattern's variables are bound from space atoms, which the checker cannot see. But when the pattern's head has a declared type - (: age (-> String Number Atom)) - atoms of that relation conform to the schema, so the pattern variables of (match &self (age $who $n) ...) acquire String and Number, the match body compiles guard-free (including fused arithmetic), and the result type flows onward through collapse/let/calls. Direct type queries (match &self (: $x Fruit) $x) bind $x : Fruit from the pattern itself; conjunctive comma patterns type each conjunct. Nested constructor patterns recurse. This derives space-read types from the producer-side schema instead of assuming them from consumer-side requirements, keeping runtime checking intact where no schema exists. examples/strict_match_schema.metta runs under --strict, so any residual guard in the generated code fails the suite. test.sh: green (187 OK incl. dispatch matrix). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…mption Cherry-picked from typecheck-v2-pettachainer-strict (f182cc4) with one change dropped: Kept: - check_value/3 clauses reunited (fixes a discontiguous-clause load warning) - lib_roman set-operation declarations un-parenthesized: (: (/?\) ...) parsed as a list-named declaration and was silently ignored; the twelve declarations are now active - () types as (List $t) - the empty list inhabits every list type - collapse always produces a known (List ...) type (element falls back to a wildcard), and add-atom/remove-atom outputs are Bool - add_known_type unifies an unbound single candidate instead of accumulating - set_out_type accepts nonground types, letting polymorphic list outputs flow - copy_term_nat for specialization keys (keeps type attributes out of names) - examples/strict_type_flow.metta (runs under --strict; passes without the dropped change) Dropped: the local_type_var mechanism, which assumed consumer-side required types for clause-local variables without emitting guards - a Number could flow through a String-typed function silently in non-strict mode. Dynamic boundaries get an explicit ascription form instead (next commit). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
expression_typed/1 was deliberately newtype-transparent: an argument position declared (Newtype Expression) kept its argument unevaluated, exactly as a literal Expression position does. That reading made a brand-typed position unable to receive a COMPUTED value at all - (expected-role? (holder-role $h)) compiled the inner call as the literal ['holder-role', H] and answered wrongly in every mode, PeTTaChainer's nested_nominal_call_argument_not_reduced repro. The reversal follows the branch's own brand doctrine: the representation is an upper bound on the payload's shape, never a licence - and never a quoting instruction. Only the LITERAL Expression type now invokes the convention, which is what a code-taking function asks for. Nothing is lost for constructor-built payloads (evaluating data is identity), and a genuinely raw fun-headed payload still has quote. All five brand/newtype examples keep their verdicts. Suite: 229 example greens + 94 expected-fail, both matrices. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018hetjCktvza2Xa7nCopnJx
import_prolog_functions_from_file/2 and _from_module/2 had no declared or inferable type, so a --strict program could not load PeTTa's own import library (PeTTaChainer's strict_lib_import_missing_types repro). Both are (-[nondet]-> Expression (List %Undefined%) %Undefined%) now: nondet is the honest arrow for one-solution-per-imported-name (superpose), and the list type on the name-list parameter is what discharges superpose's residual guard under --strict. Pinned as strict_lib_import. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018hetjCktvza2Xa7nCopnJx
Follow-up to ee7a35a, which was pushed on a red suite - my error, caught by the harness on the next run. Declaring the previously-undeclared importers changed their first parameter's argument convention: undeclared, the call site EVALUATED (library lib_import.pl) and the resolved path reached consult; declared Expression, the raw form was passed instead and the import failed silently, breaking git_import and test_datetime. The path parameter is %Undefined% now - a wildcard carries no convention, so the argument evaluates exactly as before the declaration existed. The strict_lib_import pin also asserted with assertEqual, which prints no verdict line, so the harness scored its clean exit as a failure; it uses test/2 like every other positive example. Suite verified before this commit: exit 0, 229 example greens + 94 expected-fail, both matrices. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018hetjCktvza2Xa7nCopnJx
… match A feature batch driven by downstream PeTTaChainer needs, all opt-in: - Generalize the fold-flat special case into declaration-driven contextual typing: a declared product or (List T) result flows top-down through if/case/let/let*/chain/match bodies, closure-resolved call arguments, and staged let* initializers. Explicit constructors (data ...) and (make-list ...) receive the expectation element-wise. Syntax-form dispatch guards against var-headed compounds: ($proof) is data whose head is unbound, never a syntax form. - Structural aliases (: Name (Alias Rep)), expanded once in normalize_type; late declarations re-normalize every store and recompile affected functions. - Opaque foreign types (: Name (Foreign Arity)) for FFI values such as library(heaps) heaps: trusted at check_value, never structurally inspected. - Typed spaces (: &s (SpaceOf Row)): add-atom/remove-atom values are prevalidated against the row, match patterns are bound with the row type including union narrowing; definite contradictions reject at compile time. - Newtype-transparent pattern binding: a structural pattern at a brand-typed position binds through the brand's representation, so raw destructuring of Newtype fields carries no residual strict checks. Each feature ships strict_/fail_strict_ examples; suite 845/0, chainer suite 52/0. Ignore git-import!'s repos/ clone target. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…t-det arrows Fixes from an external soundness review, each verified by repro, plus two design decisions settled with the downstream PeTTaChainer agent: - soundness_matrix.sh Phase B reports failures through the worker-safe channel; the no-det-cut phase can actually fail the suite now. - foldall no longer certifies an unknown initializer as the accumulator output type; absence of evidence leaves the residual check in place. - Determinism case coverage types scrutinee literals through the ordinary value-typing relation, so a statically impossible case is rejected. - map/foldl/filter-atom determinism proofs require a bound proper list; an open or partial list rejects at the boundary instead of enumerating. - Declaration removal is the inverse of addition: it recompiles the function, uncaches every declaration kind, recomputes explicit effect metadata from the remaining overloads, and Newtype/cross-kind conflicts are order-independent. - A runtime clause change recompiles transitive callers whose compiled form consumed the old determinism proof (visited-set cascade), so stale det commitments are re-validated instead of silently violated. - Deferred type requirements are as strong as immediate ones: nested list/tuple variables are constrained, and an mreq-attributed variable validates its eventual binding with the same error policy. The checker attributes no longer leak into program-visible identity: =alpha and =@= compare attribute-free (copy_term_nat), and mreq lists merge by variant-union. - --strict-det requires an explicit -[det]->, -[semidet]->, or -[nondet]-> in every arrow position of a declaration, higher-order parameters included; the mode-dependent reinterpretation of plain -> is gone. Plain arrows keep their uncommitted meaning in default and --strict modes. Chosen over plain-as-semidet by the downstream chainer project, which migrates its declarations next. Suite 860/0 including the genuine soundness matrix; PeTTaChainer verified 52/52 through the deferred-guard change and now awaits its arrow migration. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two rounds, verified together (suite 912/0; downstream PeTTaChainer integrated and green): Library-origin trust: declarations loaded through the curated (library ...) import path are verified promises - full compile-time checking, but in non-strict modes they emit no runtime residual guards and no variable constraints at call sites. Untyped projects importing typed libraries pay nothing at runtime; a user redeclaration restores guards; strict obligations are unchanged (suppressing them there would be unsound). git-import! and plain file imports stay user-origin. Enforced by examples/lib_trust_matrix.sh. Typed libraries: every lib/*.metta plain arrow migrated to an explicit effect arrow chosen from clause behavior, and public functions of the previously untyped libraries declared where type and cardinality are verifiable; reflective helpers deliberately stay undeclared rather than receive guessed signatures. Effect polymorphism: -[$v]-> declares an effect variable ranging over det < semidet < nondet. One variable per declaration, allowed in closure-parameter arrows and the top-level arrow; a call's effect is the join of the body's intrinsic level (closures assumed det) and the closure arguments' actual levels. Effect functions compile without commitment cuts - cardinality is analytic and carried to call sites; --oracle-det audits instantiations against actual arguments. The form counts as explicit under --strict-det. Conduit library functions (map/fold-flat family, composition operators, iterate, for-each-in-atom) are now polymorphic instead of fixed-level. Also: soundness-matrix Phase B result comparison canonicalizes SWI's allocator-dependent variable numbering while preserving sharing, so it compares answers rather than allocation artifacts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Builtin behavior lived in six places that had drifted (implies was implemented and classified but missing from the Boolean signatures). builtin_registry.pl now holds one builtin_spec record per builtin - implementation origin, typing, evaluation, cardinality, and lowering. det_builtins' fixed-effect table is a thin view over the registry; argument-sensitive and contextual rules stay procedural but are SELECTED by registry name, so a dangling rule reference is a load-time error. Startup validation plus examples/builtin_registry_matrix.sh check the registry against implementations and lib_builtin_types.metta signatures in both directions; an unregistered builtin now fails the suite instead of drifting silently. Behavior is unchanged: suite 912/0, downstream PeTTaChainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
One fn_decl(F, Arity, scheme(Args, Out), effect_model(Top, Vars), Origin, provenance(Loc, syntax(Orig))) record replaces the fragmented declared_fn_type/4 + explicit_det_decl/2 + explicit_committed_decl/3 stores, absorbs the library-origin side table, and carries the effect-variable metadata. All mutation flows through one writer pair, so the removal-inverts-addition and order-independent-conflict rules hold by construction. The old predicates remain as fresh-copy views so consumers migrate incrementally; effective-overload determinism, effect-variable lookup, trust decisions, and lifecycle code use the canonical record directly. Stored provenance now enriches determinism conflicts and redeclaration warnings. Consolidation surfaced and reconciled four fragment inconsistencies: first-overload-only committed-decl retention, symbol-level origin clearing, separate erase/reconstruct removal paths, and triple-store alias rebuilds. Behavior unchanged: suite 912/0, chainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Determinism, exhaustiveness, output-certificate, and conditional-effect analyses now return one closed record - analysis_proof(Subject, Verdict, requirements(...), certificates(...), dependencies(...)) - instead of publishing through asserted facts and b_setval scopes. Core walkers emit observations via delimited continuations; analysis_collect/2 turns them into returned data, so a top-level proof carries the transitive evidence it consumed. Boundary requirements are published only by the validation path; constructor snapshots and exhaustiveness verdicts are boundary stores the cores no longer mutate. The four det/effect/certificate memo stores collapse into one analysis_memo behind a four-predicate cache API that preserves the old broad invalidation policy - the single boundary Phase 4 will refine using the dependency lists every proof now carries. Read-only recursion scopes remain and are documented in place. Two conversion hazards were found and fixed: forall/negation probes backtracked over returned proof events, and nested Boolean certificate checks re-entered the public wrapper, losing the recursion stack. Behavior unchanged: suite 912/0 with all matrices, chainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Compiled clauses, specializations, and generated lambdas now persist the dependency lists their Phase 3 proofs consumed - compiled_deps keyed by clause ref with an indexed compiled_dep_edge view - and every mutation (clause change, declaration add/remove, constructor-set change, alias change) enters one notify_mutation/1 entry point that invalidates exactly the matching memos and recompiles exactly the affected functions, transitively. Revalidation failures throw what a fresh compile would. Deleted as subsumed: late_symbol_use tracking, constructor snapshots and their recompile scan, the alias-specific recompile loop, the source-walking caller cascade, and global output-certificate flushing. The graph also covers what those mechanisms only acknowledged in comments: late clauses breaking consumed output certificates and invalidated effect-polymorphism conditional verdicts now recompile or reject their consumers (fail_late_output_cert_consumer, fail_late_effect_conditional). Suite 912/0 with all matrices, chainer 52/0; chainer load time roughly halved (indexed edges replace source walking). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
translate_expr/4 takes none | expected(T); translate_expected_product and its duplicated construct clauses (match, if, case, let, let*, chain, list and data construction, branch merging) are deleted. The dispatch invariants survive - variable-headed compounds never unify syntax clauses, atomics and partials bypass them, [] keeps its list-expectation meaning - and expectation propagation is exactly as selective as before: contextual products and (List T) only, flowing through the same result positions. Each place the two paths had drifted for the same construct was reconciled to observable-identical behavior; case now shares one recursion while keeping Prior-based narrowing and first-match semantics. The 5b half (det analyzer consuming the same traversal) was assessed and deliberately NOT done: the analyzer's walk is entangled with clause-set fixpoints, assumption stacks, flow-sensitive narrowing, and cardinality-specific handling where analysis intentionally differs from codegen. Sharing it would need a semantic expression IR, not traversal events; a partial merge would create a third path. Recorded here as the starting point for any future unification. Suite 912/0 with all matrices, chainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The checker is now separately loaded ownership units: predicates are never interleaved across files, every persistent store's dynamic or thread_local declaration lives in its owning file, and typecheck.pl uses ensure_loaded in an order that is organizational, not semantic. examples/typecheck_boundary_matrix.sh enforces both properties - it loads the units in a permuted order and rejects predicates defined in more than one file. Drifted code moved to its owners: ctor_snapshots.pl is deleted (constructor mutation keys to decl_store, certification to clause_checks/oracles, exhaustiveness storage to det_analysis, file context to filereader); parametric declaration checks moved from oracles to inference; det_args.pl renamed det_proofs.pl to match what it owns. builtin_registry.pl became a real SWI module; the remaining units are documented user-module boundaries - forcing modules onto files sharing translator stores and attribute hooks would be a broad call-site migration for no behavioral gain. Suite 912/0 with all five matrices, chainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The Phase 3 proof machinery cost a 6.7x load-time regression on the downstream chainer (bisected per phase commit; Phase 4 recovered part). Profile-guided fixes, behavior and API identical: - Memo invalidation follows indexed analysis_memo_dep edges instead of scanning every memo clause and reconstructing its dependencies (clause/3 was 19.7% of self-time). - Nested analyses return one proof record whose lists the parent merges once, replacing per-observation replay through the collection machinery (this was quadratic in nesting depth). - Per-observation reset/shift replaced by a backtrackable scoped event stack internal to analysis_collect/2. - The dependency graph keeps an exact owner-maintained set of consumed constructor types and reverse validation edges, instead of rewalking compiled clauses per constructor declaration. - Proof lists are sorted and deduplicated before caching; ground proofs, declarations, and dependency lists skip copy_term. Benchmark (chainer test_inheritance_query_proof, min of 3): 8.84s to 1.95s, matching the pre-architecture checker on the same host control (2.31s). Chainer full suite: ~288s to ~156s. Suite 912/0 with all five matrices, chainer 52/0. Memo behavior unchanged - same lookups, hits, and invalidation policy, cheaper mechanics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Raw =@= success already implies attribute-free variance - identical attributes still correspond after stripping - so =alpha and =@= accept at C speed without copying. A raw failure is final unless checker attributes are present on either side; only that rare case pays for the attribute-stripping copies. Ground proof-key comparisons, the hot case in downstream proof dedup, no longer copy at all. Same semantics as the round-4 fix (the identity regression examples all hold); no separate unsafe fast variant needed. Chainer suite wall time: ~156s to 63s. Suite 912/0, chainer 52/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Six verified findings from the second external review, each with a pinned regression example: - A clause body's determinism is not the cardinality of calling the relation. An inferred (uncommitted) callee now certifies det only when the call's arguments prove unique, applicable clause selection and coverage - degrading to semidet/nondet otherwise - with boundness provisos where the proof consumed a parameter, and proper-list evidence propagated through recursive traversals. The effect-polymorphism intrinsic consumes the same call-effect relation. No existing example needed loosening. - Determinism recursion guards key by F/N, not F: a recursive call to another arity of the same symbol is no longer assumed coinductively det. - A runtime arrow check requires positive callable evidence (registered function or partial application at the required arity); a value that would take the reduce data fallback cannot satisfy an arrow type. - A trusted-library call records its declared result type only when every argument obligation was statically discharged; trust waives guards, never manufactures certificates. Untyped importers keep zero runtime cost. - Non-function declarations (SpaceOf, Alias, Newtype, Foreign, value) are first-class in the dependency graph via declaration(Kind, Name) keys and declaration_changed events; removing a space schema now recompiles its readers instead of leaving stale certifications. - Recompilation stages and validates every replacement clause before erasing the old ones, so a failed revalidation keeps the previous consistent state. The remaining runtime add-atom source window is documented in place. - Repeated-variable dead-call elimination is restricted to primitive/nominal non-union pairs where assignability failure implies disjointness; overlapping unions compile normally. Suite 916/0 with all five matrices, chainer 54/0 (their suite gained two tests since the last baseline). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Eight verified findings from the third external review, all fixed: - The repeated-variable dead-call optimization is DELETED, not restricted again: open user atom types are not closed disjoint sets (a value may legally carry several type declarations), so no assignability shortcut can prove an empty intersection. - Library trust keys on the CALLER: a declared function always emits its lib-boundary guards (killing the det hole - det callers are declared by definition); only undeclared callers keep zero-cost imports, and a call whose guards were waived contributes at most semidet so inferred effects cannot launder unverified inputs. Origin flips recompile compiled guard-free callers via the graph. - Closure values, the fresh-variable fallback, and effect-polymorphic calls consume the same selection/coverage machinery as direct calls. A partial single clause yields a semidet closure, never det; an effect-poly call joins body, closure, and actual-argument selection effects. The complete selection evidence set: manifest structure, output certificates of the producing expression (inline collapse and certified functions, with output_cert dependency edges), and declared types backed by boundary provisos. Each form existed in some pre-unification path; the unified proof now holds all of them. - Selection claims only what survives translation: clauses with head goal prefixes support no selection proof, compiler forms such as data contribute no structural evidence, and cons patterns compare in one normalized representation. - body_commits accepts only a direct body (cut): a cut as a let value runs after pattern unification and is no unconditional entry commit. - Declaration dependencies are recorded negatively (every consultation point, whether or not a declaration exists yet) and alias rebuilds emit events for each rebuilt dependent declaration. Typed-space updates stay definite-mismatch-only by design - partial rows and removal patterns are legitimate - now also enforced at the runtime space boundary for wrappers compilation cannot see through. - A failed declaration revalidation retracts the staged declaration and origin instead of leaving them active over old executable code. Suite 925/0 with all five matrices, chainer 54/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Six findings, conservative-downgrade direction throughout: - Selection proofs: one possible clause is at most one (semidet); call-site coverage requires covering keys (pinned constructor and cons fields cover nothing); a declared local type is not shape evidence - producers need output certificates, parameters use boundary provisos. - Generated failure paths: a clause whose head elaboration emitted goals cannot commit det; let/chain patterns contribute may_fail unless entailed by the value's known, declared, or closure-RESOLVED instantiated type (fresh-variable product patterns over resolved parametric fold results stay det; literal and unentailed constructor patterns do not). - Strict modes reject unresolved nominal intersections on repeated variables (the hidden guard violated strict's no-implicit-residual guarantee); default mode holds conjunctive mreq requirements correctly instead of failing on the second. - SpaceOf is a checked schema: declaring it validates existing rows (definite mismatches throw, naming the row); README documents the full contract. - Bounded mutation cleanup: failed runtime function addition retracts everything it staged (no ghost callables); declaration transactions restore on failure as well as throw; all declaration kinds share the transaction helper. - Quoted compounds type STRUCTURALLY: (quote (+ 1 2)) is a tuple, not a Number; (quote ($v $w)) with typed variables IS its product type, so literal term construction stays expressible. Quoted atomics keep literal types. Calibrations against the downstream chainer restored three typing facts the checker already knew: quoted structural products, sole-constructor nominal destructuring (with ctor_set dependency), and closure-resolved instantiated product types for let entailment. Suite 932/0 with all five matrices. The chainer gate intentionally reports its next genuine finding: inheritance-lift-parts destructures an Expression-typed value with a constructor pattern inside -[det]->, an invariant the type system cannot see; the chainer encodes it honestly next (case-with-error, semidet, or precise premise types). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
examples/fuzz_matrix.sh (sixth matrix in test.sh) plus a seeded generator: small random programs over nominal types with random constructors, random clause-head shapes (variable, literal, pinned constructor, cons/nil, overlapping), random effect annotations including effect variables, and random call modes from bound literals to unbound variables. Each program's embedded test forms encode the cardinality its DECLARED effects promise - adversarial programs whose promise the runtime cannot honor are generated on purpose, and the checker must reject them. Conservative rejection is never a failure; only accepted-then- misbehaves is: a failing test in an accepted program, an --oracle or --oracle-det throw on a discharged certification, a --no-det-cut result difference, or the new MUTATION CONVERGENCE property - an incremental add/remove/late-declaration sequence must end observably identical to a fresh load of the equivalent final program, the executable statement of "removal is the inverse of addition". A test failure outranks the exit code (a canary caught that a failing test also exits nonzero and would otherwise count as a rejection). Failures shrink by form deletion and are saved with their seed. Fixed seed and 45 programs in CI; four seeds x 45 programs ran clean: 145 accepted, 35 rejected, zero misbehaviors. Suite 932/0 with all six matrices. (The generator was started by the implementation agent but its session was cut off mid-task by a provider content filter; the runner, detection ordering, mutation variants, and validation are hand-finished.) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(@ Whole Inner) now works in typed-space match patterns - top-level and nested - through the SAME mechanism clause heads always used: a registered function application in a pattern position elaborates into a fresh runtime-pattern variable plus its translated call, emitted after the match goal. @'s as-pattern behavior (bind the exact stored row while destructuring it) is derived from its ordinary lib_patrick definition, works only when that library is loaded, and works identically for any other det function in a pattern position. Boundary: only uniquely-declared det functions elaborate - a det application has unambiguous value semantics in a pattern, while registered nondet names (the downstream chainer's cpu-call) are legitimately used as data tags and stay literal structure. The @-specific clauses that had accreted are gone: pattern_value_shape, bind_param_type, bind_pattern_typed, quoted-pattern tracking, inference constructor-field typing, and both det_analysis destructuring cases now resolve function signatures generically - @'s observed type transparency falls out of its ($a $b -> $a) arrow, with a clause_set dependency recorded so redefinition invalidates consumers. The only remaining '@' literals in src/ are unrelated Python bool normalizers. Suite 935/0 with all six matrices; downstream chainer 54/0 (their side fixed inheritance-lift-parts, so both projects are green together). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
case is first-match and committed, so a union member whose constructors were ALL consumed by earlier branches cannot reach a later branch. A VARIABLE fallthrough pattern now subtracts such members from its bound union - (case $v (((mk-ref $n) ...) ($rest ...))) over (| Wrapped Ref) types $rest as Wrapped alone - removing the downstream idiom of re-branding the fallthrough by hand. Exclusion is positive-proof-only: a nominal member subtracts only when its nonempty constructor set is completely consumed by prior patterns; primitives, lists, wildcards, arrows, and newtypes are never subtracted (their values are not exhausted by constructor coverage). Each nominal exclusion records its ctor_set dependency, so a constructor declared later invalidates the narrowing and recompiles the consumer. Suite 940/0 with all six matrices; downstream chainer 54/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four improvements from the downstream chainer's post-cleanup audit: - (if (= $v (Ctor ...)) Then Else) with a union-typed variable and literal constructor structure lowers through the existing case translation: Then gets constructor narrowing and typed fields, Else gets subtraction narrowing - no new analysis. Deliberately narrow: plain = only (== does not bind), literal patterns only - broad case elaboration changed eager equality behavior downstream. - brand over a control construct or construction translates its payload under expected(Representation) through the existing expectation spine, then applies the brand once: per-branch ascriptions inside (brand N (if/case ...)) are no longer needed, and a contradicting field fails against the representation directly. - Parametric foreign products already instantiated correctly through destructuring ((Heap $v) -> (Number $v (Heap $v)) with $v := Goal); verified and pinned with a native pop adapter example rather than fixed. - bind_param_type expands concrete Newtype representations for structural clause-HEAD parameters, mirroring the binder used by match patterns since round 2: (= (kb-context-kbid ($kbid $_ctx $_vars)) $kbid) against (: KBContext (Newtype (KB Expression Expression))) types $kbid as KB, transitively. Suite 951/0 with all six matrices; downstream chainer 54/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four edges found by the downstream chainer's standalone repros: - A case scrutinee CONSTRUCTED from typed values (a positional pair of parameters) now derives its product type, so deep patterns bind through positional fields, constructor fields, and newtype representations. - The equality-test desugar accepts variable-headed PURE-STRUCTURE patterns (variables, literals, constructor applications) when the scrutinee's known type is a union or a matching-width product; evaluable subterms stay excluded - the eager-equality hazard was about evaluation, not shape. - The known-type constraint path acquires brands the way check_value always did: a value whose merged candidates all fit the brand's representation takes the brand as its canonical nominal type; a DIFFERENT brand or a concrete representation conflict still rejects. - That canonical recording alone fixes brand-through-let: the branded output carries its singleton nominal type through any binding, with no let-specific logic. The four downstream repros load clean under --strict --strict-det and are ported as pinned examples. Suite 958/0 with all six matrices; chainer 54/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
rTreutlein
force-pushed
the
typecheck-v2
branch
from
August 2, 2026 08:26
e1bd9e3 to
e7938dc
Compare
Contributor
|
I wonder if we could adopt more compact notations such as
You may notice the new arrow type I understand that it breaks backward compatibility, cause the regular arrow type What do you think? |
Collaborator
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Compile-time typechecking
Adds an optional type system to PeTTa. Declarations are checked during
translation, most checks resolve at compile time, and the type information
feeds code generation.
What you get:
(: f (-> Number Number Number))is checked at every call site anddefinition. Mismatches are compile errors with file and line.
parameters bound inside destructuring patterns. Inference only adds
knowledge: it eliminates guards and types call outputs, but never demands
anything of a caller and never rejects a program that would otherwise run.
(
number(V) -> true ; ...) instead of reflection per call.--strict: every function needs a declared or inferable type and noimplicit runtime checks may remain. Dynamic values are handled visibly,
either with
(the Type Expr)(a single checked cast) or by declaring%Undefined%outputs.(STV Number Number), nominal constructor declarations, union types(| A B)with pattern narrowing, erased nominal newtypes(
(: Proof (Newtype Expression))— compile-time brands with zero runtimerepresentation), and match patterns typed from declared relation schemas.
Heterogeneous lists widen to the union of their element types instead of
losing their type. Several
.mettafiles can be loaded in order, andknowledge arriving late — a declaration or constructor in a later file —
recompiles exactly the clauses whose verdicts it invalidates.
Determinism is part of the type. Three arrows:
-[det]->(exactly oneresult),
-[semidet]->(zero or one, committed identically),-[nondet]->.A written commitment is validated in every mode — body analysis with
positive evidence about callees, non-overlapping heads, a provable-only
exhaustiveness check — and compiles to a commit after head match, so deep
deterministic recursion runs in constant memory (22MB instead of 285MB at
depth 3M in the included example). The builtin determinism table was derived
by reading every predicate's source, and call sites with manifest argument
shapes get sharper verdicts than the (name, arity) worst case. A committed
arrow also enforces bound arguments at the boundary — exactly where the
determinism proof relied on boundness, and nowhere else: a
(and $l $r)wrapper gets a
nonvarcheck per consumed parameter and throws a clear erroron an unbound argument instead of silently enumerating, while a pure data
constructor, det with any arguments, gets none. A parameter the body tests
with
is-varis exempt — the author handled the unbound case. "Typed impliesbound" holding at the consumed positions is what lets Bool-typed parameters
use the boolean builtins, typed parameters reach
remove-atom, andfixed-width tuple parameters count as manifest lists — all deterministically.
The analysis is also flow-sensitive where it pays: behind a
(== $xs ())test a semidet head accessor is det, and a function whose everyclause provably yields a proper list (a
collapse, say) certifies its outputso list builtins are det through the wrapper.
--strict-detremains thestrictest level: every arrow position of a declaration must state its
cardinality explicitly (
-[det]->,-[semidet]->,-[nondet]->), higher-order parameters included — a plain
->is rejected there rather thansilently reinterpreted. Higher-order conduits declare an effect variable
instead of overloading:
(: map (-[$v]-> (-[$v]-> $a $b) (List $a) (List $b)))is det with a det closure and nondet with a nondet one, and a nondet
instantiation consumed in a det context is a compile error.
The checker audits itself.
--oraclere-emits every staticallydischarged certification — clause outputs and call-site arguments — as a
runtime check;
--oracle-detcounts the solutions of every committed calland throws on a cardinality violation;
--no-det-cutsuppresses the commititself. The test suite runs all three over every example, plus a manifest of
known-counterexample programs (some multi-file — several holes exist only
across a load-order boundary) that must fail for exactly the stated reason.
Three adversarial audit rounds against these oracles closed eleven soundness
holes; the recurring defect shape — "unknown" read as "compatible with
everything" — is now a design rule: unknown is not evidence, anywhere.
On real code: we converted the PeTTaChainer inference engine to full strict
typing (including the
--strict-detexplicit-arrow migration), and theconversion surfaced and fixed real bugs in the chainer itself. It also drove
the checker: dozens of reported gaps (union narrowing through
case, brandsafter control flow, accessor element types, space-op determinism, and more)
are fixed and pinned as examples in this branch.
On the ConceptNet own-pet benchmark, the type-directed execution path
reduced chainer query CPU time by ~23% against master in a controlled
comparison (identical proof and TV, paired runs). The end-to-end branches
are ~4% apart because two effects unrelated to the checker mask the gain on
this particular query: the typed export's corrected conjunction-introduction
semantics adds 5,545 rules to an And-heavy candidate set, and the two
exports fall on opposite sides of SWI-Prolog's 2^20 clause-index boundary
(~2.8%). The interesting part is where the win comes from: the typed
query performs 97.2% fewer
reducecalls (640 vs 22,769) — staticallytyped calls compile to direct predicate calls instead of interpretation —
while runtime type validation is negligible: 84 shallow guards and zero
slow-path value checks in the hot path. Strict typing pays through
compilation, not checking. This is a controlled result for one
conjunction-heavy workload, not a universal speedup claim.
Microbenchmarks, from the individually benchmarked codegen commits:
The gains show up where typed values run through arithmetic, closures or
deterministic recursion in inner loops, and wash out in match/search-dominated
code. The he_minimalmetta row is the honest cost: translation got roughly
20-40% more expensive, which you notice as load time and in code that
re-translates its expressions at runtime. Memoizing runtime translations
would remove that whole class of cost (it would help untyped code just as
much); planned as a follow-up.
Implementation notes: there is
one type store, one compatibility relation (
type_unify/2), and types travelon attributed variables — no second bookkeeping path. Errors are thrown
during translation; generated code is never re-scanned, and no subexpression
is translated twice.
cons,appendand friends deliberately have no global(List $a)signatures (that would reject legal heterogeneous expressions) —they are typed contextually instead, constructors and accessors both. Runtime
guards go through
get-type, so user-defined refinement types keep working.Testing: the example suite went from 152 to 383 files — 117 of them
fail_*cases that must be rejected with the exact expected error, the rest running
green, many under
--strict/--strict-det— plus five matrix scripts(oracle soundness, type dispatch, library trust, builtin-registry
consistency, and load-order independence of the checker units) asserting
properties of the generated code and of the checker itself.
test.shisgreen after every commit, and the history is granular on purpose: each
codegen optimization is its own commit and was benchmarked individually.
Size: the checker is 14 ownership units under
src/typecheck/(~5300lines: one declarative builtin registry, one canonical declaration store,
analyses that return proof records, and one dependency graph that
recompiles exactly the clauses a late declaration or clause change
invalidates);
src/translator.plgrew to ~1400. The rest of the diff istests and README documentation.
🤖 Generated with Claude Code
https://claude.ai/code/session_018hetjCktvza2Xa7nCopnJx