AI 中文总结
研究动态语言类型推断中函数参数的四个证据来源,提出广义约束投影框架GCP,用零注释方式存储并检查调用,利用相关技术和协议,证明了诸多性质,还在Outline语言中实例化并应用于Python源恢复注释。
AI 中文摘要
动态类型语言的类型推断必须协调函数参数的四个不同证据来源:内部赋值、显式声明、上下文要求和结构操作。现有系统常将这些来源合并为一个约束集,导致虚假冲突或需要冗余注释。我们提出广义约束投影(GCP),一个零注释推断框架,它将四个来源存储在稳定定义时模板的单独单调槽中,并在新的投影会话中检查每个调用。普通调用验证具体参数并专门化返回类型而不修改模板,而柯里化产生剩余投影函数。GCP使用大纲等式匹配(OEM)和未来this。在有限高度类型预序的严格成功片段上,我们证明了单调性、局部和全局收敛等性质。对于纯的、无递归的核心Outline0,我们还证明了大步评估定义性、类型保留等。我们在Outline动态语言中实例化GCP,并将其应用于无注释的Python源以恢复PEP 484注释用于下游编译。
英文摘要
Type inference for dynamically typed languages must reconcile four qualitatively different sources of evidence: assigned values, explicit declarations, contextual requirements, and structural operations. Existing approaches often combine them into one constraint set, causing spurious conflicts or requiring annotations. We present Generic Constraints Projection (GCP), a zero-annotation inference framework that stores these sources in four monotone slots on a stable definition-time template and evaluates each call in a fresh projection session, preventing cross-call contamination while specializing return types. GCP uses Outline Equational Matching, an open structural preorder, and a future-this projection rule that preserves concrete receiver types across fluent chains and subtype extensions. On the success-state fragment of a bounded type domain, we prove monotonicity, local and global fixed-point convergence, conditional projection soundness, termination, multi-module convergence, and order independence. For an immutable core language, we also prove big-step evaluation existence, type preservation, runtime receiver retention, and projection-evaluation coherence. We instantiate GCP in Outline for typed ontology worlds and in a Python annotation-recovery pipeline. On 513 manually adapted, fact-paired Outline ports of TypeEvalPy cases, GCP obtains 513/513 exact matches, compared with 485/513 for the published Codestral Q&A baseline on the same fact IDs (two-sided exact McNemar p = 7.45e-9). This is a carrier-port evaluation in TypeEvalPy's closed-world Python vocabulary, not a run on unmodified Python sources.
Comments62 pages, 5 figures, 4 tables