类型、名称与模块

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

类一：类型结构与形成

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

类型形成 Γ ⊢ A type：

• 七种内建类型均合法；类 本身也被接受为类型，不引入宇宙层级。
• 环境中其类型被认定为元类型的名称可作类型。透明别名展开，普通值不因名字像类型就合法。
• 箭头的各定义域和结果分别须为类型，右嵌套箭头在构造时展平；定义域中的箭头保留嵌套。
• 全称参数在环境中绑定为元类型，检查其体；其绑定只能表示类型参数。
• 依值箭头（化 A 者「x」而 B，A 为可依赖的内建值类型）与隐式值参数（承 A 者「x」而 B）的形成见依值类型依二。
• 元组各项须为类型；命名元组的字段名按源顺序随项保留。
• 类型应用的头须解析到名义构造器（直接名或文件引用）；沿 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. 收集可直接读取的显式实参类型。预读入口只读取六种实参形式（及其位置包装）：局部自由变量取环境中的类型；文件定义引用取该定义的类型；带类型标注的式子 A 也 e 取 A 经类型形成后的类型，e 留到第 7 步正式检查；第四种是单态函数的满参调用 g 于 x1 … 于 xk，须同时满足三个条件：g 剥去位置包装后是局部变量或文件定义引用；g 的类型是单态函数（不是全称多态）；各实参都是显式参数，k 正好等于 g 的函数类型的显式参数个数。满足时取 g 的返回类型；各 xi 照样不在这一轮合成，推定仍是一遍有序匹配（「坐待」于（宿主导入 于 …） 靠这一条推出类型参数）。第五种是构造写法 「头」【…】（标签函数类型签七）：头剥去位置包装后是局部变量或文件定义引用、类型是单态函数时，取头的返回类型（构造写法按签名补齐参数，结果总是头的返回类型）；各项同样不在这一轮合成（数据文件里 「列」【「软件」【…】，…】 靠这一条推出列的元素类型，提案 00028）。第六种是组值 「组值」【「字段」者 值 也，…】（元组构造节点，议四一八）：按各项合成组类，与正式检查的作用域合成同法，得到形如 「组类」【「名」乃 文 也，…】 的类型；合成不出时照旧不提供 ground 类型（普通代码与数据文件里 「列」【「组值」【…】，…】 没有期望类型时，靠这一条从第一个元素推出列的元素类型，后面的元素再按它检查）。只对组值字面量本身合成，不扩及其余式子。头是多态函数、带 以、部分应用、头是匿名函数或别的式子的调用，照旧不提供 ground 类型。字面量、投影、其余复杂调用、无标注函数不能在这一轮凭猜测提供 ground 类型；不得“改进”为总是递归合成所有实参。源码先前若已把表达式绑定成变量，则可读取该变量类型；也可就地写成 （类型 也 实参）。
5. 按显参顺序尝试将 Ai 与对应已知实参类型匹配，再将 R 与 E 匹配。若还存在后续调用脊，此轮不使用最终 E。裸函数实例化时以完整显式函数类型代替 R 来匹配 E。读到的实参类型若仍是全称多态，不作 ground 信息。
6. 映射中还有未解名则拒绝。报错列出未能确定的隐式参数、函数的隐式参数名与各显式形参类型，并提示可给实参加类型标注 （类型 也 实参） 或用 以 依次给出隐式参数；完整的匹配映射只在详细调试输出中打印。这个算法是有序匹配，不是任意反复求解的全局搜索。不能因后续某个 lambda 看似给出线索就静默增加推断能力。
7. 应用所有已给及自动合成的类型实参，逐个检查显参对替换后的 Ai；检查能发现预读匹配时跳过/失败的约束冲突。形成补全后的调用节点。
8. 剩余脊非空则以当前结果类型和已形成对象继续；否则返回结果。检查模式最终必须与 E 相等。

因此多态函数带数字字面量的调用，可能需要显式 以 或期望结果类型；把字面量先局部绑定也可能改变可推断性。综上，隐式参数由变量、定义引用、带类型标注的式子、单态函数的饱和调用与组值字面量这五种显式实参的类型，以及期望的结果类型推定；其余实参要提供类型，就写成 （类型 也 实参）。连续 化 A 而化 B 而 C 是一组二参数箭头，f 于 a 不因表面左结合而合法。函数参数本身可以是函数类型，调用回调与函数偏应用不是一回事。

依值箭头的实参检查与代入、隐式值参数的实例化与推定见依值类型依三。

类五：模式算法

提案 00002 第四步：标准库 数据结构/多态列。豫 的「列」「罄」「缀」是内建列（《《内建类型：列》》、《《内建列：罄》》、《《内建列：缀》》）的别名。普通结构比较和分支合一仍把旧列类型头（所有者“豫言”、包名“标准库”、包内该模块）规整为内建列身份，供旧缓存与旧接口使用；元素类型逐项比较。内建罄、缀沿用原来的构造器标签及字段表示。

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

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

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

整数索引的细化、“无法细化”与依值模式匹配见依值类型依六。

提案 00002 的分支细化开发规则

宿主边界暂拒绝结果类型特化的构造器：最终结果的类型参数必须是互不相同的全称变量，不能包含常量、复合类型或重复变量。检查该类型的全部构造器，拒绝消息为“结果类型特化的构造器不能过宿主边界”。待办事项：实现特化构造器的宿主边界转换。

模式约束的确定合一冲突使该分支不可达，编译器在分支源码位置发出“不可达的匹配分支”警告并跳过分支体的类型检查。模式里构造器所属的类型与被鉴值的类型不是同一个类型时，编译器在模式处报错“模式的构造器「名」不属于被鉴值的类型「类」”（带文件与行列），分支体照常检查，本次鉴式检查完再一起报出。合成匹配结果类型时采用首个可达分支；没有可达分支且没有期望类型时不能合成。--no-warnings 关闭警告输出，仍跳过不可达分支。模式里的裸名（构造器除外）一律作新的局部绑定、遮蔽外层（议题 212、222）；全局函数、本文件的类型名、外层局部绑定与模式变量都照此，内建构造器名与常值仍按表达式检查。模式里的应用以函数为头、重复模式绑定、非法显式存在参数等普通错误继续报错：以函数为头的应用在可达性筛选时即报出。模式位置出现名称解析从别的模块展开出来的类型表达式时，编译器报定稿诊断，带文件、行列与源码行：那里的源码是裸名时，消息为“模式变量「名」与类型「名」同名，换个名字”；源码里写着 以（…）时，消息为“模式里不能写类型实参，去掉 以（…）”；源码文字不是可用的裸名、模式项又是元组、箭头或隐式前缀类型时，消息为“模式里不能写类型表达式：…”；其余情形照旧报“不是支持的模式匹配项：…”。前两种消息末尾提示模式只能由构造器、字面量与新名组成（议题 #419）。

有明确期望类型且所有分支均不可达时，仍先求被匹配式，再抛出可捕获的“模式匹配错误，缺少分支”异常。

本段记录正在验收的开发规则，实施状态及证据见实施记录。完整 GADT、存在类型及不可达分支验收尚未完成。

构造器结果类型与分析对象类型做双向一阶合一；外层环境里类型为元类型的局部变量可在该分支内求解，求解带出现检查。得到的代换作用于分支的期望返回类型、局部绑定的类型以及分支体中的类型参数和标注。每支单独建立状态，正常返回及异常退出均恢复原状态，其他分支沿用原环境。

有明确期望类型的匹配可作这种细化。合成匹配仍从首支合成结果、检查后继支；若任一支细化了外层类型变量，则报“需类型标注”。后继支从首支得来的类型属于合成算法的内部结果，不能据此放行细化。局部匹配可以用类型判断给出期望类型，例如 （「文」也（鉴……））。

存在类型开发路径先以构造器结果推定隐式参数。结果不能确定的参数成为分支内的新刚性类型，字段和随包函数按该类型检查；合成分支的结果类型不能包含这些新名称，否则报“存在类型逃出模式匹配分支”。显式模式类型参数只能核对结果已确定的类型，不能强指定存在参数，也不能凭此指定把泛型构造器的外层索引细化。跨参数组的未定存在参数仍在实现和验收范围内。

存在类型在隐式模式参数中绑定一次，使检查后分支语法树闭合；其后重复引用使用同一类型名称。模式转换擦除该隐式绑定，运行时构造器字段保持原次序。

跨参数组的构造器模式由最终构造结果求解隐参；读取后继全称时使用新名字，将最终结果中有用的后继索引纳入推定，每次只给当前调用组补足隐参。后组实际绑定继续服从同一最终索引约束，隐藏类型的绑定和逃逸限制覆盖整个分支。

类六：无体声明与宿主边界

无体声明是签名之后没有同名定义的 乃 声明，只许出现在词法与语法语四所列的文件里。语法分析给它合成函数体：逐个接收参数的嵌套函数，最内层是一次内部原语调用，实参依次是各层参数。类型检查按声明类型检查这个函数体，并按声明类别改写最内层的调用：

• 宿主导入（。接口。豫）：按各参数的类型与期望的结果类型算出边界签名（形与 Wasm 类型的对应见网页汇编接口网五），附在内部名末尾，去掉类型为“有”的实参。算边界形时先展开透明类型；整数、小数、爻、字符串、有直接对应；元组与命名元组按项；列 于 T 为列；字节串、字节缓冲为串；有构造器的类型按构造器在类型声明里的次序列出各支，用类型实参代换构造器的类型参数；接口文件里没有构造器的类型为资源；结果类型 异步返回 于 T（标准库 语言核心/异步原语。豫）记作异〔T 的形〕，只许作结果的最外层。函数类型、全称类型、类型变量、除列以外的递归类型、动态分类值，以及非接口文件里没有构造器的类型（如引用类），都报“不能过宿主边界”。
• 内建声明（。内建。豫）：声明名须在编译器的原语表里，否则报“不在原语表里的内建名”。签名按粗形核对：整数、小数、爻、字符串（字节串、字节缓冲同属串）、有分别记为整、小、爻、串、元，其余类型记为任；去掉元参数后，参数个数与原语表相同，原语表写“任”的位置配任何粗形，其余位置须相同，否则报“内建签名不符”。核对通过后改成原语的内部名（豫言_ 加声明名），由代码生成就地生成指令或运行时调用。参数次序照内部原语。
• 底层内建声明（。底层内建。豫）：内部名是 底层_ 加声明名（声明名以“声明”开头的改成 声明： 加其余部分，如「声明存」改成 声明：内存），须在底层后端的原语表（底层定型。豫）、车道原语表或特殊处理名单里，否则报“不在底层原语表里的内建名”。签名按粗形核对：整数与爻记为整，小数记为双，底层库数值类型的长整数、单精度、向量记为长、单、向，字符串记为串，有记为元，其余类型（类型变量等）记为任；去掉元参数后，原语表里的原语须参数个数相同，地址参数配整或长，任配任何类型，结果的元配整，其余位置须相同，否则报“内建签名与底层原语表不符”。特殊处理的原语只核对名字。
• 底层导入（。底层接口。豫）：模块名是接口文件名（去掉后缀），字段名是声明名，改写为 导入：模块：字段：参数：结果；参数与结果写类型字串（整数与爻为整，长整数、单精度、小数、向量为长、单、双、向；没有就写 0），去掉类型为“有”的实参，结果为“有”时没有结果；其他类型报“底层导入的参数与结果只能是整数、爻、长整数、单精度、小数、向量或有”。语义见《底层模式》七。

• 应用接口（。应用接口。豫）：改写为“应用接口：包名：函数名：全签名”，全签名连类型为“有”的参数也写出（代码生成据此知道实现的哪几个参数是“有”），实参照样只留非“有”的。入口定义了同名顶层函数时编成导出，入口没有实现却被调用时抛出可捕获的异常，见网页汇编接口网五。待办事项：尚未核对入口定义的类型与应用接口声明的类型是否相同，目前靠接口检查器在实现文件模式下核对。

标准库的语言原语都声明在 库/豫章/本原/本术。内建。豫，宿主服务声明在 库/豫章/东道。接口。豫 与 宿主带列。接口。豫（导入模块“标准库”）；标准库的公开函数改调它们，公开名与参数次序不变。底层库的原语声明在 库/底层库/本术。底层内建。豫，底层库各模块的公开函数改调它们。

名一：作用域与查找

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

鉴 的模式里，裸名与构造器（含构造器的值别名）同名时作构造器模式；其余裸名一律作新的局部绑定、遮蔽外层，与本文件的类型名、顶层函数、常量同名时亦然（议题 212、222）。遮蔽后分支体里同名的引用归内层这个绑定，递归调用随之取内层的值（议题 434）。从别的模块展开出来的类型名在模式位置按“模式项是类型表达式”报定稿诊断，模式变量取另一个名字即可（议题 #419）。

命名空间是由 寻 建立的静态名字作用域，只出现在 之 投影的左侧，不能作为参数、返回值、类型或数据。命名空间之名 在名称解析时消除成对应文件里的定义引用，不作为运行时结构查找。

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

名二：导入与包定位

路径由包名、登记的子包名与包内模块名构成。包根是 名字。包。豫 所在目录；直接依赖与子包登记（「包含在」「包含包」）由包说明声明。首段必须是当前包自身或其直接依赖的包名，指定起始包；自第二段起，若某段是当前所指包登记的子包，则下钻到该子包并继续，否则其余各段是所指包内的模块路径，即子包优先于模块。路径止于某个包（单段，或止于子包）时按该包的默认导入展开（见下文），不自动聚合整个目录；多段模块在所指包的包根下逐段定位。模块路径末段对应文件 模块名。豫；该文件不存在时依次查接口文件 模块名。接口。豫、模块名。应用接口。豫 与内建声明 模块名。内建。豫，再查着色源 模块名。着色器。豫（导入它得到构建时生成的模块）。着色文件（。着色器。豫、。着色器。接口。豫）里的导入只查 模块名。着色器。豫 与 模块名。着色器。接口。豫，见着色语言着二。底层文件（文件名带「。底层」）里的导入只查 模块名。底层。豫、模块名。底层接口。豫 与 模块名。底层内建。豫，高级文件导入这三种底层模块时报错，全部后缀见文件后缀。未登记的嵌套包仍是边界，不许经父包路径越过；登记的子包可经父包路径引用。源码扩展名为 。豫，兼容输入路径处理另接受 .yuyan。

导入操作有三种：寻 加载目标文件，并建立以路径末段命名的静态命名空间；观 将已导入文件的名字纳入未限定名称查找，所观的文件须已由 寻 或 寻观 导入；寻观 兼具二者。依赖图包括这些需要接口的文件；自身导入和循环依赖不得靠加载部分接口绕过。

默认导入是库包描述里「类型」必填的「默认导入」字段，值是列表，可以为空列表（空列表表示这个包的导入必须写明模块路径）。条目是包内模块路径（用 / 分段，不含扩展名）或登记的子包名；子包优先于模块，子包条目递归展开该子包自己的默认导入；各条目展开出的叶子模块之间不许导出同名定义。展开成多个叶子模块时，寻 把路径末段绑成对应全部叶子模块的命名空间（包名之名 逐个叶子模块查找），观 按条目次序依次打开各叶子模块，寻观 兼具二者；绑定的命名空间只有路径末段这一个，需要某个条目自己的命名空间时，显式 寻 该模块。字段的写法与检查见豫构包系统“默认导入”。

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

名三：构造器与接口定序

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

文件接口保留类型、普通值、构造器各项；透明类型直接保存展开体；值保存类型及引用；构造器保存类型和名义身份。没有类型的编译产物只能供装配，不能供新的源码类型检查。

全局存储按最终定义表建立：普通源文件的顶层是写成常量初值的数据，测试、脚本与黄金样例另有程序体（见执行与编译行一）。一般参数多态在运行时擦除，类型构造器和透明类型可成空占位，但不能因此随意压缩定序。匿名顶层表达式的名字使用编译器内部序号；与旧对象逐项替换时应携带基线接口清单，不要求他方猜出这个名字。