类型、名称与模块

本篇描述前端接受边界。独立实现不要默认采用 HM、一般依赖类型或自动柯里化系统；它们会接受本基线拒绝的程序，且可能改变运行时参数分组。

类一：类型结构与形成

记环境 Γ 为有序绑定及文件接口表。使用类型形状：内建(b)、刚性变量 a、名义构造器 C(P,N,c,K)、类型构造应用、箭头[A1,…,An,R]（n≥1）、全称[a1,…,am].B（m≥1）、元组[A1,…,An]。P 是声明文件身份，N 是声明名，c 是类型内编号，K 是声明的类型。

类型形成 Γ ⊢ A type：

• 七种内建类型均合法；元类型 本身也被接受为类型，不引入宇宙层级。
• 环境中其类型被认定为元类型的名称可作类型。透明别名展开，普通值不因名字像类型就合法。
• 箭头的各定义域和结果分别须为类型，右嵌套箭头在构造时展平；定义域中的箭头保留嵌套。
• 全称参数在环境中绑定为元类型，检查其体；其绑定只能表示类型参数。
• 元组各项须为类型。
• 类型应用的头须解析到名义构造器（直接名或文件引用）；沿 K 消费参数。显式箭头定义域须是元类型，每实参经过类型形成；隐式全称位置只能用隐式实参。最后 K 须为元类型，否则是未完全应用。运行时值、普通 λ 和未解析投影不可作为任意类型计算头。
• 待定/空缺节点不能进入正式类型形成。不得用“任意未知都当类型变量”绕过失败。

立 可以声明元类型的元素（名义类型），也可声明返回某个类型的值构造器。静态身份不可由运行时标签反推；两个不同名义声明即使形状相同也不相等。

类二：类相等及约束匹配

比较前使用检查后接口展开透明类型引用，不展开普通值函数体进行求值。基本比较规则：内建标签相等；刚性变量相同；箭头/元组数量相同且逐项相等；应用头及参数形式和实参逐项相等；全称的参数数量相同，并在同一批新鲜刚性变量下比较其体；名义构造器仅按文件身份 P 与声明名 N 比较；本基线该比较分支忽略 c 和 K，不能把运行编号或完整声明类型额外加进名义相等条件。

结构比较对带类型抽象有共同换名及局部 η 扩展处理：抽象与非抽象比较时，按抽象参数形式将非抽象项施于同一新鲜变量，再比较。它不等于任意 β 规约求正规形。接口类型应先规范化为上述有限形状；普通对象的“子类型检查”仅调用类相等，不存在普遍宽度子类型、协变自动提升或动态类型兜底。

隐参匹配另带有限映射 U:局部待求名→未解或类型：左侧待求变量未解时记录右项；已解时与旧解比较；非待求名是刚性名。按相同结构递归比较。尝试匹配失败时保留进入该次尝试前的映射，不以局部失败的残留更新继续推导；最终每项实参还要按求得类型正式检查。

类三：合成与检查

合成 Γ ⊢ e ⇒ A 返回类型与补全后的表达式；检查 Γ ⊢ e ⇐ A 返回补全后的表达式。对“类型无法合成”不能退化成动态值执行。

上述列出可实现算法，而非只列类型推理结论。例如首模式分支无法合成时，不能任意换一支推断然后称完全兼容；条件的双向尝试与模式的首支策略不同。

类四：完整调用算法

输入为已合成的调用头 (T,h)、有序显隐实参脊 S、可选期望 E：

1. 打开 T 最前的连续全称参数，替换为与环境、实参、期望中名字都不冲突的待求变量，依声明顺序记录 a1…am。拆其后显式箭头为 A1…An→R；不是箭头则 n=0。
2. 从 S 最前读取至多 m 个 授以。一旦开始显参，必须顺序消费当前 n 个显参；显参之间出现隐参则拒绝。S 原本非空时要求饱和，显参不足则拒绝；S 原本为空时允许把整个函数值拿来实例化。消费完的剩余脊留待下一轮应用结果。
3. 已给的隐参依序填入 U；每个都必须形成合法类型，不能把整数 1 作为隐式类型实参。若头既无隐参又无显参而仍有调用，拒绝非函数应用。
4. 收集可直接读取的显式实参类型：本基线这个预读入口只直接读取局部自由变量或文件定义引用（及其位置包装）。字面量、复杂调用、无标注函数不能在这一轮凭猜测提供 ground 类型；不得“改进”为总是递归合成所有实参。源码先前若已把表达式绑定成变量，则可读取该变量类型。
5. 按显参顺序尝试将 Ai 与对应已知实参类型匹配，再将 R 与 E 匹配。若还存在后续调用脊，此轮不使用最终 E。裸函数实例化时以完整显式函数类型代替 R 来匹配 E。读到的实参类型若仍是全称多态，不作 ground 信息。
6. 映射中还有未解名则拒绝。这个算法是有序匹配，不是任意反复求解的全局搜索。不能因后续某个 lambda 看似给出线索就静默增加推断能力。
7. 应用所有已给及自动合成的类型实参，逐个检查显参对替换后的 Ai；检查能发现预读匹配时跳过/失败的约束冲突。形成补全后的调用节点。
8. 剩余脊非空则以当前结果类型和已形成对象继续；否则返回结果。检查模式最终必须与 E 相等。

因此多态函数带数字字面量的调用，可能需要显式 授以 或期望结果类型；把字面量先局部绑定也可能改变可推断性。连续 化 A 而化 B 而 C 是一组二参数箭头，f 于 a 不因表面左结合而合法。函数参数本身可以是函数类型，调用回调与函数偏应用不是一回事。

类五：模式算法

先将分析对象合成为类型 T。对每个分支独立建立绑定环境：

• 对已解析的构造器常量，实例化隐参并使构造器最终结果匹配 T；显式载荷模式依次按其参数类型检查。
• 新名称模式引入类型 T 的局部绑定；已被识别为构造器的名字不作新变量。数字/字符串/爻常量模式必须与 T 相符。
• 元组模式要求明确的元组 T，数量相同，逐项处理。列字面模式已展开为标准库构造器模式。
• 应用模式必须以构造器为头，不能以任意函数作反向运算。
• 各分支的局部绑定只在本分支结果可见；重复绑定、重复默认等限制应按失败用例处理，不把同名绑定默认实现成相等性守卫。

运行时判别经擦除后按构造器标签、数/串/爻值及元组字段进行。缺少分支会生成运行时报错路径；并非全都在类型阶段做穷尽证明。实现者可以采用不同决策树，但应保持源顺序可达分支的行为和默认分支限制，不执行未选分支。

名一：作用域与查找

局部绑定最新者优先。顶层处理按声明次序推进：先解析定义体（自递归的局部绑定另加），再把新定义加入后续可见绑定；普通前向名称不会因为文件后面存在定义就自动合法。当前绑定优于命名空间，命名空间优于打开文件。

命名空间解析有一条特殊规则：解析名字 N 先查名为 N 的空间；若该空间中有同名定义 N，则返回该定义，否则返回纯空间引用。模块投影在名称解析时消除，不作为运行时结构查找。

打开文件按环境中的列表顺序查询，先命中的定义生效；每次打开都前插，因此后打开的文件优先。顶层定义则附加到已有绑定列表末尾，查找先命中此前同名项；它与局部最新绑定优先的规则不同。模块内部重复名与投影的行为不能通过“一律最新者优先”概括：本地绑定链和文件定义列投影分别查找，文件投影取有序列表中第一个匹配名称。本基线没有全面同名冲突拒绝保证，独立实现须保留相应顺序信息。

名二：导入与包定位

路径由包名和包内模块名构成。包根是 名字。包。豫 所在目录；直接依赖由包说明声明。单段导入查包 总集。豫，不自动聚合整个目录；多段模块在包根下逐段定位。子包是边界，不许经父包路径越过。源码扩展名为 。豫，兼容输入路径处理另接受 .yuyan。

寻 建立以路径末段命名的空间；观 将目标接口纳入未限定名称查找；诵 将目标接口内容重导出。组合按“寻、观、诵”效果执行，不能把 观 自动等同于 寻。依赖图包括这些需要接口的文件；自身导入和循环依赖不得靠加载部分接口绕过。

包解析本身不属于值 ABI，但其输出 P 进入符号身份。互链时必须使用相同 P，不得以另一工作目录的物理路径擅自替换。可把依赖解析器做成单独层，向编译器提供已解析绝对身份、源码及有序依赖，避免类型检查隐式访问不确定搜索路径。

名三：构造器与接口定序

类型内构造器序数从 1 开始。扫描此前环境中“同一文件且构造器最终返回类型头相同”的构造声明，计数加一；比较返回类型头时剥离全称和箭头，再取构造应用头。不能让别的数据类型插入声明影响该类型的序号。

文件接口保留类型、空间、普通值、构造器各项；重导出项保持原文件及定义身份，不能改成重导出文件的虚构源码定义。透明类型直接保存展开体；值保存类型及引用；构造器保存类型和名义身份。没有类型的 .o 只能供链接，不能供新的源码类型检查。

模块计算按最终定义表建立全局存储。一般参数多态在运行时擦除，类型构造器和透明类型可成空占位，但不能因此随意压缩定序。匿名顶层表达式的名字使用编译器内部序号；与旧对象逐项替换时应携带基线接口清单，不要求他方猜出这个名字。