依值类型

这是提案 00002 第五步的依值规则：类型可以依赖整数、爻、字符串及其列表的值。本文与文言稿同步。索引式的形状与闭合比较见整数类型索引、爻类型索引、字符串类型索引、列表类型索引。

依一：写法

「定长表」立化「整数」而化「元类型」而「元类型」也。
「新定长表」乃承「甲」而化「甲」而化「整数」者「长」而（「定长表」于「长」于「甲」）也。
「读定长表」乃承「整数」者「长」而承「甲」而
  化（「定长表」于「长」于「甲」）而化（「下标」于「长」）而「甲」
也。

• 化 A 者「x」而 B：A 是可依赖的内建值类型（整数、爻、字符串，或元素仍为这些类型的列表）时造依值箭头，B 里可以提到 x；B 不提 x 时就是普通箭头。A 是元类型时报“化〇者□而〇 的定义域不能是元类型”，类型参数写成 承「甲」而 …。
• 承 A 者「x」而 B：A 是元类型时是隐式类型参数，与 承「x」而 B 相同；否则是隐式值参数，编译后擦除。
• 带标签的依值箭头写成 化「签」为 A 者「x」而 B，标签按位核对，绑定名按换名比较。隐式值参数不带标签。
• 化 A 者「x」而化 B 而 C 仍是一组二参数箭头，饱和规则不变。

依二：类型形成

依值箭头与隐式值参数的定义域先按参数定义域检查（保留标签），去掉标签后须是可依赖的内建值类型，否则报“依值参数的定义域须为整数、爻、字符串或它们的列表”。绑定名以该类型加入环境，再检查值域。值域里类型构造器的索引实参照各索引篇检查为索引式。

依三：调用

• 显式组含依值箭头时，依值位的实参先核对标签、按定义域检查，并须是索引式，否则报“类型中的整数参数须为索引式；其他实参先用虑绑定”一类诊断。去掉源码标注后的检查结果代入后面各位的定义域与结果类型；随后的推定、实参检查与结果类型都用代入后的类型。
• 类型与模块类四第 4 步读取单态函数满参调用的返回类型时，同样先代入依值实参。
• 隐式类型参数与隐式值参数可以交替出现，逐个实例化为待求名；授以 给出的隐式值实参按定义域做对象检查。
• 推定仍是有序匹配：待求的索引变量只在单独出现时求解（向量 于 维 对 向量 于 三 得 维＝三）；含未解待求变量的复合索引式（如 加 左 右）暂不比较，留到代入隐式参数后的最终检查。只在复合式里出现的隐式参数推不出来，要用 授以 给出。
• 隐式参数未能确定时，先不吞错地重放各次接地比较，遇到类型不符就报该不符。

依四：拉姆达

• 会「x」而 e 对依值箭头检查：x 以定义域类型加入环境，按代入 x 后的值域检查 e。
• 对隐式值参数检查：受「x」而 e 绑定 x；会 开头的拉姆达先以不重名的新名打开隐式值参数，再检查整个拉姆达。两者都包成隐式拉姆达，随隐式参数擦除。
• 遇 A 者「x」而 e 合成时，体的类型提到 x 就合成依值箭头，否则合成普通箭头。
• 隐式值参数只能用在类型里。项层引用由隐式参数擦除报“隐式参数擦除后绑定变量仍然存在”。待办事项：在类型检查阶段提前拦截。

依五：相等

• 整数索引：两侧至少一侧是整数加、减、乘或列表投影（长度、乘积）的调用时，两侧规范成数学整数多项式再比较。变量与不透明项作原子；长度、乘积 作用在列表变量段上的结果也作原子。比较前先规整标准库总集重导出的别名。
• 列表投影：长度 按字面段累计元素个数，乘积 按元素的整数多项式相乘，空列的乘积为一。乘积 由标准库 数据结构/多态列。豫 提供。
• 结构比较时左侧已解的待求变量先代入。
• 待办事项：含变量的列表、字符串、爻索引仍只按结构比较；第N个 尚未接入整数规范化。

依六：模式

• 分支细化时，外层环境里类型为可依赖内建值的局部名与类型变量一样可解：空列 的结果 定长列 于 零 匹配 定长列 于 n 时，该分支里 n＝0。
• 整数索引的合一先按结构进行；冲突时把两侧规范成多项式：相等则不细化，两侧都是常量而不同则判为不可达，其余报“无法细化”。覆盖检查遇到“无法细化”按可达处理，只给缺例警告。
• 期望类型确定不了的隐式值参数成为分支内的存在名，按其定义域声明。
• 依值模式匹配：被匹配的是变量、且它出现在期望类型里时，各分支的期望类型里把它代换成该分支的模式，索引随之规约，如 长度 于（缀 头 尾） 规约成一加 尾 的长度。
• 已解析成文件定义引用的裸构造器模式与按名找到的构造器同样处理：带隐式参数的走模式施函，否则做广义合一。
• 待办事项：环境里其他变量类型中的被匹配变量尚未代换；构造器的依值字段在模式里尚未把字段名代入后面字段的类型；规范后一侧是单独待求变量时尚未据此绑定。

依七：擦除与边界

隐式值参数与隐式类型参数一样擦除，显式依值参数照常传递。签名元数与签名类别剥去交替出现的隐式前缀，依值位按普通显式参数计数。无体声明的元数同样计入依值位。宿主边界：带索引的类型按去掉索引之后的形处理，构造器的隐式值参数与类型参数一样由类型实参代换；依值箭头与隐式值参数函数同普通函数、全称函数一样不能过边界。待办事项：结果类型带复合索引（如 加 n 一）的构造器仍按结果类型特化处理而被拒。

依八：验收样例

应用/豫言编译器/测试/语法/依值类型/ 收第八节例一（局部寄配的两张表，及只开一格、次序颠倒两个反例）、例二（向量拼接与点积，及维数不同反例）、例五（张量改形，及漏维反例），另有依值箭头、标签、旧式写法报错、索引细化、无法细化与依值模式匹配各例。